nyuuzyou/wikis huggingface dataset:
Categorical Variable/Examples/Time to Failure

== Example of Categorical Variable ==
Let $X$ be a random variable whose values take on various classifications of time to failure of a machine part:
:$\set {< 100 \, \mathrm {hr}, 100 - 199 \, \mathrm {hr}, 200 - 299 \, \mathrm {hr}, > 300 \, \mathrm {hr} }$
Then $X$ is classed as a categorical variable.
== Sources ==
* 
Category:Examples of Categorical Variables
Categories of Elements of Ring

== Theorem ==
Let $\left({R, +, \circ}\right)$ be a ring.
The elements of $R$ are partitioned into three classes:
:$(1): \quad$ the zero
:$(2): \quad$ the units
:$(3): \quad$ the proper elements.
== Proof ==
By definition, a proper element is a non-zero element which has no product inverse.
Also by definition, a unit is an element which does have a product inverse.
Because $0 \circ x = 0$ there can be no $x \in R$ such that $0 \times x = 1$, and so $0$ is not a unit.
Hence the result.
Category:Ring Theory
Categories of Elements under Well-Ordering

== Theorem ==
Let $A$ be a class.
Let $\preccurlyeq$ be a well-ordering on $A$.
Let $x \in A$ be an element of $A$.
Then $x$ falls into one of the following $3$ categories:
:$(1): \quad x$ is the smallest element of $A$ $\preccurlyeq$
:$(2): \quad x$ is the immediate successor of another element $y \in A$ $\preccurlyeq$
:$(3): \quad x$ is a limit element of $A$ under $\preccurlyeq$.
== Proof ==
Let $x \in A$.
;$(1): \quad x$ is the smallest element of $A$ $\preccurlyeq$:
We note that $\preccurlyeq$ is a well-ordering on $A$.
Hence as $A \subseteq A$ we have that $A$ has a smallest element.
Hence there exists one element of $A$ which is that smallest element of $A$.
Let $x$ be that smallest element of $A$.
By definition of smallest element:
:$\forall y \in A: x \preccurlyeq y$
Hence $x$ cannot be the immediate successor of another element $y \in A$ $\preccurlyeq$.
;$(2): \quad x$ is the immediate successor of another element $y \in A$ $\preccurlyeq$:
Let $y \in A$ such that $y$ is not the greatest element of $A$ $\preccurlyeq$.
Then:
:$\forall y \in A: \exists x \in A: y \preccurlyeq x$
such that $x$ is an immediate successor of $y$.
By definition of immediate successor, it follows that $x$ is not the smallest element of $A$ $\preccurlyeq$.
;$(3): \quad x$ is a limit element of $A$ under $\preccurlyeq$:
Suppose there exists $x$ such that:
:$x$ is not the smallest element of $A$ $\preccurlyeq$
and:
:$x$ is not the immediate successor of another element $y \in A$ $\preccurlyeq$.
Then by definition $x$ is a limit element of $A$ under $\preccurlyeq$.
The result follows.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text I$ -- Superinduction and Well Ordering: $\S 1$ Introduction to well ordering
Category:Well-Orderings
Category Axioms are Self-Dual/Morphisms-Only Category Theory

== Theorem ==
Let $\mathrm{MOCT}$ be the collection of axioms for morphisms-only category theory.
Then:
:$\mathrm{MOCT} = \mathrm{MOCT}^*$
where $\mathrm{MOCT}^*$ consists of the dual statements of those in $\mathrm{MOCT}$.
== Proof ==
== Sources ==
* : $\S 3.1$
Category:Category Axioms are Self-Dual
Category Axioms are Self-Dual/Object Category Theory

== Theorem ==
Let $\mathrm {CT}$ be the collection of seven axioms on Characterization of Metacategory via Equations.
Then:
:$\mathrm {CT} = \mathrm {CT}^*$
where $\mathrm {CT}^*$ consists of the dual statements of those in $\mathrm{CT}$.
== Proof ==
The seven axioms are:
Their duals are:
It is seen that only names of the bound variables $f, g$ and $h$ have been changed at some places.
Therefore, we conclude:
:$\mathrm {CT}^* = \mathrm {CT}$
== Sources ==
* : $\S 3.1$
Category:Category Axioms are Self-Dual
Category Induces Preorder

== Theorem ==
Let $\mathbf S$ be a category with set of objects $S$.
Then the binary relation $\precsim$ defined by:
:$\forall a, b \in S: a \precsim b \iff \exists f: a \to b$
is a preorder on $S$.
== Proof ==
It suffices to establish $\precsim$ is reflexive and transitive.
=== Reflexivity ===
For any $a \in S$, we have the identity morphism $\operatorname{id}_a : a \to a$.
Hence $a \precsim a$.
=== Transitivity ===
For $a, b, c \in S$, let $a \precsim b$ and $b \precsim c$.
Then we have:
:$f: a \to b$ and $g: b \to c$
Therefore, we have the composite morphism $g \circ f: a \to c$ as well.
Hence $a \precsim c$.
It follows that $\precsim$ is a preorder.
Category:Category Theory
Category:Preorder Theory
Category has Finite Limits iff Finite Products and Equalizers

== Theorem ==
Let $\mathbf C$ be a metacategory.
Then:
:$\mathbf C$ has all finite limits
:
:$\mathbf C$ has all finite products and equalizers.
== Proof ==
=== Necessary Condition ===
By definition, finite products are instances of finite limits.
So are equalizers, by Equalizer as Limit.
=== Sufficient Condition ===
Let $C: \mathbf J \to \mathbf C$ be a diagram, with $\mathbf J$ finite.
The objective is to construct the limit $D = \varprojlim_j C_j$.
That is:
:an object $D$
:morphisms $p_j: D \to C_j$
such that:
:$C_\alpha p_i = p_j$ for each $\mathbf J$-morphism $\alpha: i \to j$
:for each $E$ and $q_j: E \to C_j$ such that $C_\alpha q_i = q_j$ for each $\alpha$, there is a unique $f: E \to D$ such that $q_j = p_j f$ for each $j$
To this end, consider the finite products:
:$\ds \prod_{j \mathop \in \operatorname{ob} \mathbf J} C_j$ and $\ds \prod_{\alpha \mathop \in \operatorname{mor} \mathbf J} C_{\operatorname{cod} \alpha}$
of the objects of the diagram and the codomains of its morphisms.
Next, define the morphisms $\pi, \varepsilon: \ds \prod_{j \mathop \in \operatorname{ob} \mathbf J} C_j \to \prod_{\alpha \mathop \in \operatorname{mor} \mathbf J} C_{\operatorname{cod} \alpha}$ by:
:$\pi_\alpha = \pr_{C_{\operatorname{cod} \alpha}}$
:$\varepsilon_\alpha = C_\alpha \pr_{C_{\operatorname{dom} \alpha}}$
Now let $e: D \to \ds \prod_{j \mathop \in \operatorname{ob} \mathbf J} C_j$ be the equalizer of $\pi$ and $\varepsilon$.
Also, define $p_j: D \to C_j$ by $p_j = \pr_{C_j} e$ for each $j$.
Now, for every $\alpha: i \to j$:
Lastly, suppose that $E$ and $q_j$ have the properties stated.
By definition of the product $\ds \prod_{j \mathop \in \operatorname{ob} \mathbf J} C_j$, there is a morphism:
:$\ds q: E \to \prod_{j \mathop \in \operatorname{ob} \mathbf J} C_j$
Now, for every $\alpha: i \to j$:
Hence, since $e$ equalizes $\pi$ and $\varepsilon$, it follows that there exists a unique $f: E \to D$, such that:
:$q = ef$
Thus, for each $j$:
:$\pr_j q = \pr_j e f$
which, by the definitions of $q_j$ and $p_j$, amounts to:
:$q_j = p_j f$
Hence $D$ and the $q_j$ form the desired limit.
== Sources ==
* : $\S 5.4$: Proposition $5.21$
Category:Category Theory
Category has Products and Equalizers iff Pullbacks and Terminal Object

== Theorem ==
Let $\mathbf C$ be a metacategory.
Then the following are equivalent:
:$(1): \mathbf C$ has all finite products and equalizers.
:$(2): \mathbf C$ has all pullbacks and a terminal object.
== Proof ==
=== $(1)$ implies $(2)$ ===
Suppose $\mathbf C$ has all finite products and equalizers.
That $\mathbf C$ has pullbacks follows from Pullback as Equalizer.
That $\mathbf C$ has a terminal object follows by Empty Product is Terminal Object.
=== $(2)$ implies $(1)$ ===
Suppose $\mathbf C$ has all pullbacks and a terminal object.
From Category has Finite Products iff Terminal Object and Binary Products, it suffices to check that $\mathbf C$ has binary products.
That this is the case follows from Product as Pullback.
That $\mathbf C$ has equalizers follows from Equalizer as Pullback, as it is established that $\mathbf C$ has finite products.
== Sources ==
* : $\S 5.4$: Proposition $5.14$
Category:Pullbacks
Category:Category Theory
Category of Categories is Category

== Theorem ==
Let $\mathbf{Cat}$ be the category of categories.
Then $\mathbf{Cat}$ is a metacategory.
== Proof ==
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two functors their composition is again a functor by Composite Functor is Functor.
For any small category $\mathbf C$, we have the identity functor $\operatorname {id}_{\mathbf C}$.
By Identity Functor is Left Identity and Identity Functor is Right Identity this is the identity morphism for $\mathbf C$.
Finally by Composition of Functors is Associative, the associative property is satisfied.
Hence $\mathbf{Cat}$ is a metacategory.
Category:Category of Categories
Category of Frames is Category

== Theorem ==
Let $\mathbf{Frm}$ denote the category of frames.
Then:
:$\mathbf{Frm}$ is a metacategory
== Proof ==
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two frame homomorphisms their composition (in the usual set theoretic sense) is again a frame homomorphism by Composite Frame Homomorphism is Frame Homomorphism.
For any frame $L = \struct{S, \preceq}$, we have the identity mapping $\operatorname{id}_S$.
From Identity Mapping is Frame Homomorphism we have $\operatorname{id}_S$ is a frame homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $L$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Frm}$ is a metacategory.
== Sources ==
* : Chapter $\text {II}$: Introduction to Locales, $\S 1.1$ Definition (a)
Category:Category of Frames (Lattice Theory)
Category of Lattices is Category

== Theorem ==
Let $\mathbf{Lat}$ denote the category of lattices.
Then:
:$\mathbf{Lat}$ is a metacategory
== Proof ==
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two lattice homomorphisms their composition (in the usual set theoretic sense) is again a lattice homomorphism by Composite Lattice Homomorphisms is Lattice Homomorphism.
For any lattice $\struct{L, \vee, \wedge, \preceq}$, we have the identity mapping $\operatorname{id}_L$.
From Identity Mapping is Lattice Homomorphism we have $\operatorname{id}_L$ is a lattice homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $\struct{L, \vee, \wedge, \preceq}$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Lat}$ is a metacategory.
== Sources ==
* : Chapter $\text I$: Preliminaries, $\S 3.2$ Definition
Category:Category of Lattices
Category of Locales is Category

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Then:
:$\mathbf{Loc}$ is a category
== Proof ==
By definition, the category of locales is:
:the dual category of the category of frames
From Category of Frames is Category:
:the category of frames is a category
From Dual Category is Category:
:the category of locales is a category
== Sources ==
* : Chapter $\text {II}$: Introduction to Locales, $\S 1.1$ Definition (b)
Category:Category of Locales
Category of Locales with Localic Mappings is Category

== Theorem ==
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Then:
:$\mathbf{Loc_*}$ is a metacategory
== Proof ==
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two localic mappings their composition (in the usual set theoretic sense) is again a localic mapping by Composite Localic Mapping is Localic Mapping.
For any locale $L = \struct{S, \preceq}$, we have the identity mapping $\operatorname{id}_S$.
From Identity Mapping is Localic Mapping we have $\operatorname{id}_S$ is a localic mapping.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $L$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Loc_*}$ is a metacategory.
== Sources ==
* : Chapter II: Frames and Locales. Spectra, $\S 2.2$
Category:Locales
Category of Locales with Localic Mappings is Isomorphic to Category of Locales

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Then:
:$\mathbf{Loc_*}$ is isomorphic to $\mathbf{Loc}$.
== Proof ==
By definitions of category of locales and category of locales with localic mappings:
:the objects of $\mathbf{Loc}$ and $\mathbf{Loc_*}$ are locales
:the morphisms of $\mathbf{Loc}$ are continuous maps
:the morphisms of $\mathbf{Loc_*}$ are localic mappings
By definition of continuous maps:
:$f : L_1 \to L_2$ is a continuous map there exists a frame homomorphism $f^* : L_2 \to L_1 :$
::$f = \paren{f^*}^{\operatorname{op}}$
By definition of localic mapping:
:$g : L_1 \to L_2$ is a localic mapping there exists a frame homomorphism $g^* : L_2 \to L_1 :$
::$\tuple{g, g^*}$ is a Galois connection
Let $F : \mathbf{Loc} \to \mathbf{Loc_*}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map F L = L$
:for each continuous map $f : L_1 \to L_2$ of $\mathbf{Loc} : \map F f = f_*$
where:
:$f_* : L_1 \to L_2$ denotes the upper adjoint of the frame homomorphism $f^* : L_2 \to L_1$
:$f = \paren{f^*}^{\operatorname{op}}$
=== Lemma 1 ===
Let $G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
:for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{g^*}^{\operatorname{op}}$
where:
:$g^* : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
:$\paren{g^*}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism
=== Lemma 2 ===
=== Lemma 3 ===
=== Lemma 4 ===
It follows that $F$ is an isomorphism of categories by definition.
Hence $\mathbf{Loc_*}$ is isomorphic to $\mathbf{Loc}$.
== Sources ==
* : Chapter II: Frames and Locales. Spectra, $\S 2.2$
Category:Category of Locales
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales
Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 3

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $F : \mathbf{Loc} \to \mathbf{Loc_*}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map F L = L$
:for each continuous map $f : L_1 \to L_2$ of $\mathbf{Loc} : \map F f = \upperadjoint f$
where:
:$\upperadjoint f: L_1 \to L_2$ denotes the upper adjoint of the frame homomorphism $\loweradjoint f : L_2 \to L_1$
:$f = \paren{\loweradjoint f}^{\operatorname{op}}$
Let $G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
:for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{\loweradjoint g}^{\operatorname{op}}$
where:
:$\loweradjoint g : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
:$\paren{\loweradjoint g}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism
Then:
:$GF = \operatorname{id}_{\mathbf {Loc}}$
== Proof ==
By definition of $\mathbf{Loc}$ and $\mathbf {Loc_*}$ the objects of $\mathbf{Loc}$ are the objects of $\mathbf{Loc_*}$.
The object functors of $F$ and $G$ are the identity object functor and so $GF$ is the identity object functor.
Let $f : L_1 \to L_2$ be a continuous map of $\mathbf{Loc}$.
By definition of continuous map:
:there exists a frame homomorphism $\loweradjoint f : L_2 \to L_1$ such that $f = \paren{\loweradjoint f}^{\operatorname{op}}$.
From Frame Homomorphism is Lower Adjoint of Galois Connection:
:there exists an upper adjoint $\upperadjoint f$ such that $\tuple{\upperadjoint f, \loweradjoint f}$ is a Galois connection.
We have:
Hence $GF$ is the identity morphism functor.
The result follows.
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales
Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 4

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $F : \mathbf{Loc} \to \mathbf{Loc_*}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map F L = L$
:for each continuous map $f : L_1 \to L_2$ of $\mathbf{Loc} : \map G f = f_*$
where:
:$f_* : L_1 \to L_2$ denotes the upper adjoint of the frame homomorphism $f^* : L_2 \to L_1$
:$f = \paren{f^*}^{\operatorname{op}}$
Let $G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
:for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{g^*}^{\operatorname{op}}$
where:
:$g^* : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
:$\paren{g^*}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism
Then:
:$FG = \operatorname{id}_{\mathbf {Loc_*}}$
== Proof ==
By definition of $\mathbf{Loc_*}$ and $\mathbf {Loc}$ the objects of $\mathbf{Loc_*}$ are the objects of $\mathbf{Loc}$.
The object functors of $G$ and $F$ are the identity object functor and so $FG$ is the identity object functor.
Let $g : L_1 \to L_2$ be a localic mapping of $\mathbf{Loc_*}$.
By definition of localic mapping:
:there exists a Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ such that $g = \upperadjoint g$ and $\loweradjoint g$ is a frame homomorphism.
We have:
Hence $FG$ is the identity morphism functor.
The result follows.
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales
Category of Modules has Enough Projectives

== Theorem ==
Let $A$ be a ring.
Then the category of left $A$-modules has enough projectives.
== Proof ==
Let $M$ be an $A$-module.
By Surjection by Free Module there is a free $A$-module $F$ and a surjection $f : F \to M$.
By Epimorphism of Modules Iff Surjection $f$ is an epimorphism.
By Free Module is Projective $F$ is projective.
Category:Homological Algebra
Category of Monoids is Category

== Theorem ==
Let $\mathbf{Mon}$ be the category of monoids.
Then $\mathbf{Mon}$ is a metacategory.
== Proof ==
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
We have Composite of Homomorphisms on Algebraic Structure is Homomorphism, verifying $(C1)$.
We have Identity Mapping is Automorphism providing $\operatorname{id}_S$ for every monoid $\left({S, \circ}\right)$.
Now, $(C2)$ follows from Identity Mapping is Left Identity and Identity Mapping is Right Identity.
Finally, $(C3)$ follows from Composition of Mappings is Associative.
Hence $\mathbf{Mon}$ is a metacategory.
Category:Category of Monoids
Category of Ordered Sets has Enough Constants

== Theorem ==
Let $\mathbf{OrdSet}$ be the category of ordered sets.
Then $\mathbf{OrdSet}$ has enough constants.
== Proof ==
By Singleton Ordered Set is Terminal Object, we have that any ordered set with a singleton as underlying set is terminal in $\mathbf{OrdSet}$.
Let $1$ be such a singleton ordered set.
To show that $\mathbf{OrdSet}$ has enough constants, it is to be shown that if:
:$f: P \to Q \ne g: P \to Q$
then there exists an $x: 1 \to P$ such that $f \circ x \ne g \circ x$.
Now by definition of $\mathbf{OrdSet}$, $f$ and $g$ are increasing mappings.
In particular, they are mappings, and by Equality of Mappings, there must be a $p \in P$ such that:
:$\map f p \ne \map g p$
Define $\bar p: 1 \to P$ by $\map {\bar p} * = p$ (where $*$ is the unique element of $1$).
If this is a morphism in $\mathbf{OrdSet}$, we are evidently done.
This follows from Mapping is Constant iff Increasing and Decreasing.
Hence $\mathbf{OrdSet}$ has enough constants.
== Sources ==
* : $\S 2.3$: Example $2.12$: $1$
Category:Category of Ordered Sets
Category of Ordered Sets is Category

== Theorem ==
Let $\mathbf{OrdSet}$ be the category of ordered sets.
Then $\mathbf{OrdSet}$ is a metacategory.
== Proof ==
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
For any two increasing mappings their composition (in the usual set theoretic sense) is again increasing by Composite of Increasing Mappings is Increasing.
For any set $X$, we have the identity mapping $\operatorname{id}_X$.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity that this is the identity morphism for $X$.
That it is increasing follows from Identity Mapping is Increasing.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{OrdSet}$ is a metacategory.
== Sources ==
* : $\S 1.4.3$
Category:Category of Ordered Sets
Category of Pointed Sets as Coslice Category

== Theorem ==
Let $\mathbf{Set}_*$ be the category of pointed sets.
Let $\mathbf{Set}$ be the category of sets.
Let $1 := \left\{{*}\right\}$ be any singleton.
Then:
:$\mathbf{Set}_* \cong 1 \mathbin / \mathbf{Set}$
where $1 \mathbin / \mathbf{Set}$ denotes the coslice of $\mathbf{Set}$ under $1$ and $\cong$ signifies isomorphic categories.
== Proof ==
Define the functor $F: \mathbf{Set}_* \to 1 \mathbin / \mathbf{Set}$ by:
:$\map F {C, c} := \bar c: 1 \to C$
:$F f := f$
where $\bar c: 1 \to C$ is defined by $\bar c (*) = c$.
Further, define $G: 1 \mathbin / \mathbf{Set} \to \mathbf{Set}_*$ by:
:$\map G {x: 1 \to C} := \struct {C, x \paren *}$
:$G f := f$
=== $F$ is a functor ===
The definition of $F$ on morphisms is admissible, since for any pointed mapping $\map f: {C, c} \to \struct {D, d}$:
Thus by Equality of Mappings, $f \circ \bar c = \bar d$.
So indeed $F f = f$ is a morphism $\bar c \to \bar d$, as desired.
The identity morphisms of both $\mathbf{Set}_*$ and $1 \mathbin / \mathbf{Set}$ are the identity mappings, which $F$ thus preserves.
That $F$ preserves composition is also trivial, since $\mathbf{Set}_*$ and $1 \mathbin / \mathbf{Set}$ both have composition of mappings as their $\circ$.
In conclusion, $F$ is a functor.
=== $G$ is a functor ===
Let $x: 1 \to C$ and $y: 1 \to D$ be objects of the coslice $1 \mathbin / \mathbf{Set}$.
Let $f: C \to D$ be a morphism $x \to y$.
That is, let $f \circ x = y$.
Thus, in particular:
:$\map f {\map x *} = \map y *$
showing that $f$ is a pointed mapping $\struct {C, \map x *} \to \struct {D, \map y *}$.
Observe that the composition and the identity morphisms of $1 \mathbin / \mathbf{Set}$ and $\mathbf{Set}_*$ are identical.
Because $G$ is the identity on morphisms, it is thus trivially a functor.
=== $F$ is an isomorphism ===
Because $F$ and $G$ are the identity on morphisms, it will suffice to show that:
:$F \map G x = x$ for all objects $x$ of $1 \mathbin / \mathbf{Set}$
:$G \map F {C, c} = \struct {C, c}$ for all objects $\struct {C, c}$ of $\mathbf{Set}_*$
Explicitly:
Now $\overline {\map x *}: 1 \to C$ is defined by $\map {\overline {\map x *} * = \map x *$.
Hence $\overline {\map x *} = x$ by Equality of Mappings.
For the other equality:
where the last equality follows by definition of $\bar c$.
Thus $F$ is shown to be an isomorphism, and hence:
:$\mathbf{Set}_* \cong 1 \mathbin / \mathbf{Set}$
== Sources ==
* : $\S 1.6$: Example $1.8$
Category:Category of Pointed Sets
Category:Coslice Categories
Category of Pointed Sets is Category

== Theorem ==
Let $\mathbf{Set}_*$ be the category of pointed sets.
Then $\mathbf{Set}_*$ is a metacategory. 
== Proof ==
The axioms $(\text C 1)$ to $(\text C 3)$ are checked for a metacategory.
Pick any two morphisms $f : \struct {A, a} \to \struct {B, b}$ and $g : \struct {B, b} \to \struct {C, c}$ from $\mathbf{Set}_*$.
By the definition of composition in the category of pointed sets:
:$\map {\paren {g \circ f} } a = \map g {\map f a} = \map g b = c$
whence $g \circ f$ is a pointed mapping from $\struct {A, a}$ to $\struct {C, c}$.
That composition of pointed mappings is associative follows from Composition of Mappings is Associative.
For any object $\struct {A, a}$, the identity mapping $\operatorname{id}_A$ induces a pointed map $\operatorname{id}_{\struct {A, a} }: \struct {A, a} \to \struct {A, a}$, as $\map {\operatorname{id}_A} a = a$.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $\struct {A, a}$.
Category:Category Theory