A Lean Companion to Conceptual Mathematics

Article III: Examples of categories

1. The category 𝑺↻ of endomaps of sets

The category 𝑺↻ of endomaps of sets is described on pp. 136–137. We implement this category in Lean in a similar way to the category of algebraic objects that we developed in the solution to Session 4, Exercise 1. Our Lean implementation follows closely the definition of category given on p. 21, so we reproduce that definition here, interspersed with our comments (italicised) and the corresponding Lean code.

Definition: Category (p. 21)

A category consists of the DATA:

(1) OBJECTS

An object in the category 𝑺↻ is a set equipped with an endomap.

structure SetWithEndomap where t : Type carrier : Set t toEnd : t t toEnd_mem {a} : a carrier toEnd a carrier

(2) MAPS

A map in the category 𝑺↻ is one which respects the given structure — i.e., a morphism which commutes. Note that we use a Lean subtype here instead of a Lean structure.

def SetWithEndomapHom (X Y : SetWithEndomap) := { f : X.t Y.t // ( x X.carrier, f x Y.carrier) -- maps to codomain f X.toEnd = Y.toEnd f -- commutes }

(3) For each map f, one object as DOMAIN of f and one object as CODOMAIN of f

As given above, a SetWithEndomapHom is a subtype of morphisms between the underlying types of two SetWithEndomap objects, so the domain and codomain are already specified.

(4) For each object A an IDENTITY MAP, which has domain A and codomain A

We define the identity map within the SetWithEndomapHom namespace to facilitate code re-use in some closely related category instances that follow shortly.

def SetWithEndomapHom.id (X : SetWithEndomap) : SetWithEndomapHom X X := 𝟙 X.t, X:SetWithEndomap(∀ x X.carrier, 𝟙 X.t x X.carrier) 𝟙 X.t X.toEnd = X.toEnd 𝟙 X.t X:SetWithEndomap x X.carrier, 𝟙 X.t x X.carrierX:SetWithEndomap𝟙 X.t X.toEnd = X.toEnd 𝟙 X.t X:SetWithEndomap x X.carrier, 𝟙 X.t x X.carrier intro _ X:SetWithEndomapx✝:X.thx:x✝ X.carrier𝟙 X.t x✝ X.carrier All goals completed! 🐙 X:SetWithEndomap𝟙 X.t X.toEnd = X.toEnd 𝟙 X.t All goals completed! 🐙

(5) For each pair of maps {A \xrightarrow{f} B \xrightarrow{g} C}, a COMPOSITE MAP map {A \xrightarrow{g \;\mathrm{following}\; f} C}

We likewise define composition of maps within the SetWithEndomapHom namespace.

def SetWithEndomapHom.comp {X Y Z : SetWithEndomap} (f : SetWithEndomapHom X Y) (g : SetWithEndomapHom Y Z) : SetWithEndomapHom X Z := g.val f.val, X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Z(∀ x X.carrier, (g f) x Z.carrier) (g f) X.toEnd = Z.toEnd g f X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd f(∀ x X.carrier, (g f) x Z.carrier) (g f) X.toEnd = Z.toEnd g f X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd g(∀ x X.carrier, (g f) x Z.carrier) (g f) X.toEnd = Z.toEnd g f X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd g x X.carrier, (g f) x Z.carrierX:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd g(g f) X.toEnd = Z.toEnd g f X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd g x X.carrier, (g f) x Z.carrier intro x X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd gx:X.thx:x X.carrier(g f) x Z.carrier All goals completed! 🐙 X:SetWithEndomapY:SetWithEndomapZ:SetWithEndomapf:SetWithEndomapHom X Yg:SetWithEndomapHom Y Zhf_mtc: x X.carrier, f x Y.carrierhf_comm:f X.toEnd = Y.toEnd fhg_mtc: x Y.carrier, g x Z.carrierhg_comm:g Y.toEnd = Z.toEnd g(g f) X.toEnd = Z.toEnd g f All goals completed! 🐙

We can now instantiate the category 𝑺↻.

instance instCatSetWithEndomap : Category SetWithEndomap where Hom := SetWithEndomapHom id := SetWithEndomapHom.id comp := SetWithEndomapHom.comp

satisfying the following RULES:

(i) IDENTITY LAWS: If {A \xrightarrow{f} B}, then {1_B \circ f = f} and {f \circ 1_A = f}

The identity laws are given by the methods Category.comp_id and Category.id_comp, respectively, which Lean is able to discharge automatically using tactics.

(ii) ASSOCIATIVE LAW: If {A \xrightarrow{f} B \xrightarrow{g} C \xrightarrow{h} D}, then {(h \circ g) \circ f = h \circ (g \circ f)}

The associative law is given by the method Category.assoc, which Lean is likewise able to discharge automatically.

For good measure, we make the category 𝑺↻ a concrete category.

instance {X Y : SetWithEndomap} : FunLike (instCatSetWithEndomap.Hom X Y) X.t Y.t where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory SetWithEndomap instCatSetWithEndomap.Hom where hom f := f ofHom f := f
Exercise 1 (p. 137)

Show that if both X^{↻\alpha} \xrightarrow{f} Y^{↻\beta} ...and also Y^{↻\beta} \xrightarrow{g} Z^{↻\gamma} are maps in 𝑺↻, then the composite {g \circ f} in 𝑺 actually defines another map in 𝑺↻. Hint: What should the domain and the codomain (in the sense of 𝑺↻) of this third map be? Transfer the definition (given for the case f) to the cases g and {g \circ f}; then calculate that the equations satisfied by g and f imply the desired equation for {g \circ f}.

Solution: Exercise 1

Using only the category Type, we have

example {X Y Z : Type} (α : X X) (β : Y Y) (γ : Z Z) (f : X Y) (hf_comm : f α = β f) (g : Y Z) (hg_comm : g β = γ g) : (g f) α = γ (g f) := X:TypeY:TypeZ:Typeα:X Xβ:Y Yγ:Z Zf:X Yhf_comm:f α = β fg:Y Zhg_comm:g β = γ g(g f) α = γ g f -- cf. SetWithEndomapHom.comp above All goals completed! 🐙

Using instead our implementation of the category 𝑺↻ of endomaps of sets gives

example {X Y Z : SetWithEndomap} (f : X Y) (g : Y Z) : X Z := g f

3. Two subcategories of 𝑺↻

We implement the category 𝑺ᵉ of idempotent endomaps of sets, described on p. 138. We re-use code from our earlier implementation of the category 𝑺↻.structure SetWithIdemEndomap extends SetWithEndomap where idem : toEnd toEnd = toEnd instance instCatSetWithIdemEndomap : Category SetWithIdemEndomap where Hom X Y := SetWithEndomapHom X.toSetWithEndomap Y.toSetWithEndomap id X := SetWithEndomapHom.id X.toSetWithEndomap comp := SetWithEndomapHom.comp instance {X Y : SetWithIdemEndomap} : FunLike (instCatSetWithIdemEndomap.Hom X Y) X.t Y.t where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory SetWithIdemEndomap instCatSetWithIdemEndomap.Hom where hom f := f ofHom f := f
We implement the category 𝑺◯ of invertible endomaps of sets (automorphisms of sets, permutations), described on p. 138.structure SetWithInvEndomap extends SetWithEndomap where inv : inv, inv toEnd = 𝟙 t toEnd inv = 𝟙 t instance instCatSetWithInvEndomap : Category SetWithInvEndomap where Hom X Y := SetWithEndomapHom X.toSetWithEndomap Y.toSetWithEndomap id X := SetWithEndomapHom.id X.toSetWithEndomap comp := SetWithEndomapHom.comp instance {X Y : SetWithInvEndomap} : FunLike (instCatSetWithInvEndomap.Hom X Y) X.t Y.t where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory SetWithInvEndomap instCatSetWithInvEndomap.Hom where hom f := f ofHom f := f

4. Categories of endomaps

The category 𝑪↻ of endomaps is described on pp. 138–139. We implement the category 𝑪↻ below (cf. the category 𝑺↻).

Define the objects.

structure Endomap where carrier : Type toEnd : carrier carrier

Define the maps.

def EndomapHom (X Y : Endomap) := { f : X.carrier Y.carrier // f X.toEnd = Y.toEnd f -- commutes }

Define the identity maps and the composite maps.

namespace EndomapHom def id (X : Endomap) : EndomapHom X X := 𝟙 X.carrier, rfl def comp {X Y Z : Endomap} (f : EndomapHom X Y) (g : EndomapHom Y Z) : EndomapHom X Z := g.val f.val, X:EndomapY:EndomapZ:Endomapf:EndomapHom X Yg:EndomapHom Y Z(g f) X.toEnd = Z.toEnd g f X:EndomapY:EndomapZ:Endomapf:EndomapHom X Yg:EndomapHom Y Zhf_comm:f X.toEnd = Y.toEnd f(g f) X.toEnd = Z.toEnd g f X:EndomapY:EndomapZ:Endomapf:EndomapHom X Yg:EndomapHom Y Zhf_comm:f X.toEnd = Y.toEnd fhg_comm:g Y.toEnd = Z.toEnd g(g f) X.toEnd = Z.toEnd g f All goals completed! 🐙 end EndomapHom

Instantiate the category 𝑪↻.

instance instCatEndomap : Category Endomap where Hom := EndomapHom id := EndomapHom.id comp := EndomapHom.comp

Make the category 𝑪↻ a concrete category.

instance {X Y : Endomap} : FunLike (instCatEndomap.Hom X Y) X.carrier Y.carrier where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory Endomap instCatEndomap.Hom where hom f := f ofHom f := f
We implement the category 𝑪ᵉ of idempotents, described on pp. 138–139.structure IdemEndomap extends Endomap where idem : toEnd toEnd = toEnd instance instCatIdemEndomap : Category IdemEndomap where Hom X Y := EndomapHom X.toEndomap Y.toEndomap id X := EndomapHom.id X.toEndomap comp := EndomapHom.comp instance {X Y : IdemEndomap} : FunLike (instCatIdemEndomap.Hom X Y) X.carrier Y.carrier where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory IdemEndomap instCatIdemEndomap.Hom where hom f := f ofHom f := f
We implement the category 𝑪◯ of isomorphic endomaps (automorphisms), described on pp. 138–139.structure InvEndomap extends Endomap where inv : inv, inv toEnd = 𝟙 carrier toEnd inv = 𝟙 carrier instance instCatInvEndomap : Category InvEndomap where Hom X Y := EndomapHom X.toEndomap Y.toEndomap id X := EndomapHom.id X.toEndomap comp := EndomapHom.comp instance {X Y : InvEndomap} : FunLike (instCatInvEndomap.Hom X Y) X.carrier Y.carrier where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory InvEndomap instCatInvEndomap.Hom where hom f := f ofHom f := f
We implement the category 𝑪ᶿ of involutions, described on pp. 138–139.structure InvolEndomap extends InvEndomap where invol : toEnd toEnd = 𝟙 carrier instance instCatInvolEndomap : Category InvolEndomap where Hom X Y := EndomapHom X.toEndomap Y.toEndomap id X := EndomapHom.id X.toEndomap comp := EndomapHom.comp instance {X Y : InvolEndomap} : FunLike (instCatInvolEndomap.Hom X Y) X.carrier Y.carrier where coe f := f.val coe_injective' := fun _ _ h Subtype.ext h instance : ConcreteCategory InvolEndomap instCatInvolEndomap.Hom where hom f := f ofHom f := f
Exercise 2 (p. 139)

What can you prove about an idempotent which has a retraction?

Solution: Exercise 2

We can prove that the only idempotent which has a retraction is the identity.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A : 𝒞} {α β : A A} (h_idem : α α = α) (h_retraction : β α = 𝟙 A) : α = 𝟙 A := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 Aα = 𝟙 A calc α = 𝟙 A α := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 Aα = 𝟙 A α All goals completed! 🐙 _ = (β α) α := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 A𝟙 A α = (β α) α All goals completed! 🐙 _ = β α α := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 A(β α) α = β α α All goals completed! 🐙 _ = β α := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 Aβ α α = β α All goals completed! 🐙 _ = 𝟙 A := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞α:A Aβ:A Ah_idem:α α = αh_retraction:β α = 𝟙 Aβ α = 𝟙 A All goals completed! 🐙
Exercise 3 (p. 140)

A finite set A has an even number of elements iff (i.e. if and only if) there is an involution on A with no fixed points; A has an odd number of elements iff there is an involution on A with just one fixed point. Here we rely on known ideas about numbers — but these properties can be used as a definition of oddness or evenness that can be verified without counting if the structure of a real situation suggests an involution. The map 'mate of' in a group A of socks is an obvious example.

Solution: Exercise 3

TODO Exercise III.3

In Exercises 4–7 that follow, we use the type \mathbb{Z} instead of the set \mathbb{Z} (and hence the concrete category Type instead of the category 𝑺 of sets).

Exercise 4 (p. 140)

If {\alpha(x) = -x} is considered as an endomap of \mathbb{Z}, is \alpha an involution or an idempotent? What are its fixed points?

Solution: Exercise 4

Define the endomap {\alpha(x) = -x} on \mathbb{Z}.

def α : := fun x -x

\alpha is not an idempotent.

example : ¬(IsIdempotent α) := ¬IsIdempotent α h:IsIdempotent αFalse h:IsIdempotent αh_contra:(α α) 1 = α 1 := congrFun IsIdempotent.idem 1False h:IsIdempotent αh_contra:1 = -1 := congrFun IsIdempotent.idem 1False All goals completed! 🐙

\alpha is an involution.

example : IsInvolution α := { invol := α α = 𝟙 x✝:(α α) x✝ = 𝟙 x✝ x✝:- -x✝ = x✝ All goals completed! 🐙 }

The only fixed point of \alpha is 0.

example {x : } : Function.IsFixedPt α x x = 0 := x:Function.IsFixedPt α x x = 0 x:-x = x x = 0 x:-x = x x = 0x:x = 0 -x = x x:-x = x x = 0 All goals completed! 🐙 x:x = 0 -x = x x:hx:x = 0-x = x x:hx:x = 0-0 = 0 All goals completed! 🐙

Note that since the converse of eq_zero_of_neg_eq is true, we can also state the following:

theorem _root_.eq_zero_iff_neg_eq {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : -a = a a = 0 := α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:α-a = a a = 0 α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:α-a = a a = 0α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:αa = 0 -a = a α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:α-a = a a = 0 All goals completed! 🐙 α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:αa = 0 -a = a α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:αh:a = 0-a = a α:Type uinst✝²:AddCommGroup αinst✝¹:LinearOrder αinst✝:IsOrderedAddMonoid αa:αh:a = 0-0 = 0 All goals completed! 🐙

We can then use this new lemma to simplify the proof in the previous example.

example {x : } : Function.IsFixedPt α x x = 0 := eq_zero_iff_neg_eq
Exercise 5 (p. 140)

Same questions as above, if instead {\alpha(x) = |x|}, the absolute value.

Solution: Exercise 5

Define the endomap {\alpha(x) = |x|} on \mathbb{Z}.

def α : := fun x |x|

\alpha is an idempotent.

example : IsIdempotent α := { idem := α α = α x✝:(α α) x✝ = α x✝ x✝:|(|x✝|)| = |x✝| All goals completed! 🐙 }

\alpha is not an involution.

example : ¬(IsInvolution α) := ¬IsInvolution α h:IsInvolution αFalse h:IsInvolution αh_contra:(α α) (-1) = 𝟙 (-1) := congrFun IsInvolution.invol (-1)False h:IsInvolution αh_contra:|(|(-1)|)| = -1 := congrFun IsInvolution.invol (-1)False All goals completed! 🐙

The fixed points of \alpha are all the points greater than or equal to 0.

example {x : } : Function.IsFixedPt α x 0 x := x:Function.IsFixedPt α x 0 x x:|x| = x 0 x x:|x| = x 0 xx:0 x |x| = x x:|x| = x 0 x x:hx:|x| = x0 x x:hx:|x| = x0 |x| All goals completed! 🐙 x:0 x |x| = x All goals completed! 🐙

Note that since the converse of abs_of_nonneg is true with the additional assumption [AddRightMono α], we can state the following:

theorem _root_.abs_iff_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] [AddRightMono α] : 0 a |a| = a := α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono α0 a |a| = a α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono α0 a |a| = aα:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono α|a| = a 0 a α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono α0 a |a| = a All goals completed! 🐙 α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono α|a| = a 0 a α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono αh:|a| = a0 a α:Type u_1inst✝³:Lattice αinst✝²:AddGroup αa:αinst✝¹:AddLeftMono αinst✝:AddRightMono αh:|a| = a0 |a| All goals completed! 🐙

We can then use this new lemma to simplify the proof in the previous example.

example {x : } : Function.IsFixedPt α x 0 x := abs_iff_nonneg.symm
Exercise 6 (p. 140)

If \alpha is the endomap of \mathbb{Z}, defined by the formula {\alpha(x) = x + 3}, is \alpha an automorphism? If so, write the formula for its inverse.

Solution: Exercise 6

Define the endomap {\alpha(x) = x + 3} on \mathbb{Z}.

def α : := fun x x + 3

\alpha is an automorphism, with inverse {\alpha^{-1}(x) = x - 3}.

example : IsIso α := IsIso α αinv: := fun x x - 3IsIso α exact { out := αinv: := fun x x - 3 inv, inv α = 𝟙 α inv = 𝟙 αinv: := fun x x - 3αinv α = 𝟙 α αinv = 𝟙 αinv: := fun x x - 3αinv α = 𝟙 αinv: := fun x x - 3α αinv = 𝟙 all_goals αinv: := fun x x - 3x✝:(α αinv) x✝ = 𝟙 x✝ αinv: := fun x x - 3x✝:x✝ - 3 + 3 = x✝ All goals completed! 🐙 }
Exercise 7 (p. 140)

Same questions for {\alpha(x) = 5x}.

Solution: Exercise 7

Define the endomap {\alpha(x) = 5x} on \mathbb{Z}.

def α : := fun x 5 * x

\alpha is not an automorphism.

example : ¬(IsIso α) := ¬IsIso α h:IsIso αFalse h:IsIso ααinv: left✝:αinv α = 𝟙 h_right_inv:α αinv = 𝟙 False h:IsIso ααinv: left✝:αinv α = 𝟙 h_right_inv:α αinv = 𝟙 h_contra₁:(α αinv) 1 = 𝟙 1 := congrFun h_right_inv 1False have h_contra₂ : (5 : ) 1 := ¬IsIso α h:IsIso ααinv: left✝:αinv α = 𝟙 h_right_inv:α αinv = 𝟙 h_contra₁:(α αinv) 1 = 𝟙 1 := congrFun h_right_inv 11 = 5 * αinv 1 All goals completed! 🐙 All goals completed! 🐙
Exercise 8 (p. 140)

Show that both 𝑪ᵉ, 𝑪ᶿ are subcategories of the category [whose objects are all the endomaps \alpha in 𝑪 which satisfy {\alpha \circ \alpha \circ \alpha = \alpha}], i.e. that either an idempotent or an involution will satisfy {\alpha^3 = \alpha}.

Solution: Exercise 8

We show that the category 𝑪ᵉ of idempotents is a subcategory of the category given in the question.

example {α : IdemEndomap} : α.toEnd α.toEnd α.toEnd = α.toEnd := α:IdemEndomapα.toEnd α.toEnd α.toEnd = α.toEnd repeat All goals completed! 🐙

Or, more generally, that an idempotent will satisfy {\alpha^3 = \alpha}.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A : 𝒞} (α : A A) [IsIdempotent α] : α α α = α := 𝒞:Type uinst✝¹:Category.{v, u} 𝒞A:𝒞α:A Ainst✝:IsIdempotent αα α α = α repeat All goals completed! 🐙

We show that the category 𝑪ᶿ of involutions is a subcategory of the category given in the question.

example {α : InvolEndomap} : α.toEnd α.toEnd α.toEnd = α.toEnd := α:InvolEndomapα.toEnd α.toEnd α.toEnd = α.toEnd All goals completed! 🐙

Or, more generally, that an involution will satisfy {\alpha^3 = \alpha}.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A : 𝒞} (α : A A) [IsInvolution α] : α α α = α := 𝒞:Type uinst✝¹:Category.{v, u} 𝒞A:𝒞α:A Ainst✝:IsInvolution αα α α = α All goals completed! 🐙
Exercise 9 (p. 141)

In [the category Type], consider the endomap \alpha of a three-element [type A] defined by...

inductive A | a₁ | a₂ | a₃ def α : A A | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂

Show that it satisfies {\alpha^3 = \alpha}, but that it is not idempotent and that it is not an involution.

Solution: Exercise 9

We show that \alpha satisfies {\alpha^3 = \alpha}.

example : α α α = α := α α α = α x:A(α α α) x = α x x:A(match match match x with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match x with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ (match match match A.a₁ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₁ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂(match match match A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂(match match match A.a₃ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₃ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ (match match match A.a₁ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₁ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂(match match match A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂(match match match A.a₃ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂) = match A.a₃ with | A.a₁ => A.a₂ | A.a₂ => A.a₃ | A.a₃ => A.a₂ All goals completed! 🐙

But \alpha is not idempotent.

example : ¬(IsIdempotent α) := ¬IsIdempotent α h:IsIdempotent αFalse h:IsIdempotent αh_contra:(α α) A.a₁ = α A.a₁ := congrFun IsIdempotent.idem A.a₁False h:IsIdempotent αh_contra:A.a₃ = A.a₂ := congrFun IsIdempotent.idem A.a₁False All goals completed! 🐙

And \alpha is not an involution.

example : ¬(IsInvolution α) := ¬IsInvolution α h:IsInvolution αFalse h:IsInvolution αh_contra:(α α) A.a₁ = 𝟙 A A.a₁ := congrFun IsInvolution.invol A.a₁False h:IsInvolution αh_contra:A.a₃ = A.a₁ := congrFun IsInvolution.invol A.a₁False All goals completed! 🐙

5. Irreflexive graphs

Exercise 10 (p. 141)

Complete the specification of the two maps X \xrightarrow{s} P \quad\text{and}\quad X \xrightarrow{t} P which express the source and target relations of the [given graph]. Is there any element of X at which s and t take the same value in P? Is there any element to which t assigns the value k?

Solution: Exercise 10

The full specification of the two maps s and t is as follows:

inductive X | a | b | c | d | e inductive P | k | m | n | p | q | r def s : X P | X.a => P.k | X.b => P.m | X.c => P.k | X.d => P.p | X.e => P.m def t : X P | X.a => P.m | X.b => P.m | X.c => P.m | X.d => P.q | X.e => P.r

s and t take the same value in P at the element b of X.

example : s X.b = t X.b := rfl

There is no element to which t assigns the value k.

example : ¬( x : X, t x = P.k) := ¬ x, t x = P.k (x : X), t x P.k x:Xt x P.k t X.a P.kt X.b P.kt X.c P.kt X.d P.kt X.e P.k t X.a P.kt X.b P.kt X.c P.kt X.d P.kt X.e P.k All goals completed! 🐙

The category 𝑺⇊ of (irreflexive directed multi-) graphs is described on pp. 141–142. We implement the category 𝑺⇊ below.

structure IrreflexiveGraph where tA : Type carrierA : Set tA tD : Type carrierD : Set tD toSrc : tA tD toSrc_mem {a} : a carrierA toSrc a carrierD toTgt : tA tD toTgt_mem {a} : a carrierA toTgt a carrierD instance instCategoryIrreflexiveGraph : Category IrreflexiveGraph where Hom X Y := { f : (X.tA Y.tA) × (X.tD Y.tD) // ( x X.carrierA, f.1 x Y.carrierA) -- fA maps to codomain ( x X.carrierD, f.2 x Y.carrierD) -- fD maps to codomain f.2 X.toSrc = Y.toSrc f.1 -- source commutes f.2 X.toTgt = Y.toTgt f.1 -- target commutes } id X := (𝟙 X.tA, 𝟙 X.tD), X:IrreflexiveGraph(∀ x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierA) (∀ x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierD) (𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1 (𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1 X:IrreflexiveGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:IrreflexiveGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:IrreflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1X:IrreflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1 X:IrreflexiveGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:IrreflexiveGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:IrreflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1X:IrreflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1 first | X:IrreflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1 | All goals completed! 🐙 comp := {X Y Z : IrreflexiveGraph} { f // (∀ x X.carrierA, f.1 x Y.carrierA) (∀ x X.carrierD, f.2 x Y.carrierD) f.2 X.toSrc = Y.toSrc f.1 f.2 X.toTgt = Y.toTgt f.1 } { f // (∀ x Y.carrierA, f.1 x Z.carrierA) (∀ x Y.carrierD, f.2 x Z.carrierD) f.2 Y.toSrc = Z.toSrc f.1 f.2 Y.toTgt = Z.toTgt f.1 } { f // (∀ x X.carrierA, f.1 x Z.carrierA) (∀ x X.carrierD, f.2 x Z.carrierD) f.2 X.toSrc = Z.toSrc f.1 f.2 X.toTgt = Z.toTgt f.1 } X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toSrc = Y✝.toSrc f.1 f.2 X✝.toTgt = Y✝.toTgt f.1g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1{ f // (∀ x X✝.carrierA, f.1 x Z✝.carrierA) (∀ x X✝.carrierD, f.2 x Z✝.carrierD) f.2 X✝.toSrc = Z✝.toSrc f.1 f.2 X✝.toTgt = Z✝.toTgt f.1 } exact (g.1 f.1, g.2 f.2), X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toSrc = Y✝.toSrc f.1 f.2 X✝.toTgt = Y✝.toTgt f.1g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierAX✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierDX✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1(g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1(g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA intro x X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1x:X✝.tAhx:x X✝.carrierA(g.1 f.1, g.2 f.2).1 x Z✝.carrierA All goals completed! 🐙 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD intro x X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1x:X✝.tDhx:x X✝.carrierD(g.1 f.1, g.2 f.2).2 x Z✝.carrierD All goals completed! 🐙 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1(g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 All goals completed! 🐙 X✝:IrreflexiveGraphY✝:IrreflexiveGraphZ✝:IrreflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1(g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 All goals completed! 🐙
Exercise 11 (p. 142)

If f is [the map of graphs] X \xrightarrow{f_A} Y,\; P \xrightarrow{f_D} Q and if Y \xrightarrow{g_A} Z,\; Q \xrightarrow{g_D} R is another map of graphs, show that the pair {g_A \circ f_A,\; g_D \circ f_D} of 𝑺-composites is also an 𝑺⇊-map.

Solution: Exercise 11variable (X P Y Q Z R : Type) (s t : X P) (s' t' : Y Q) (s'' t'' : Z R) example (fA : X Y) (fD : P Q) (gA : Y Z) (gD : Q R) (hfSrc_comm : fD s = s' fA) (hfTgt_comm : fD t = t' fA) (hgSrc_comm : gD s' = s'' gA) (hgTgt_comm : gD t' = t'' gA) : (gD fD) s = s'' (gA fA) (gD fD) t = t'' (gA fA) := X:TypeP:TypeY:TypeQ:TypeZ:TypeR:Types:X Pt:X Ps':Y Qt':Y Qs'':Z Rt'':Z RfA:X YfD:P QgA:Y ZgD:Q RhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAhgSrc_comm:gD s' = s'' gAhgTgt_comm:gD t' = t'' gA(gD fD) s = s'' gA fA (gD fD) t = t'' gA fA X:TypeP:TypeY:TypeQ:TypeZ:TypeR:Types:X Pt:X Ps':Y Qt':Y Qs'':Z Rt'':Z RfA:X YfD:P QgA:Y ZgD:Q RhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAhgSrc_comm:gD s' = s'' gAhgTgt_comm:gD t' = t'' gA(gD fD) s = s'' gA fAX:TypeP:TypeY:TypeQ:TypeZ:TypeR:Types:X Pt:X Ps':Y Qt':Y Qs'':Z Rt'':Z RfA:X YfD:P QgA:Y ZgD:Q RhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAhgSrc_comm:gD s' = s'' gAhgTgt_comm:gD t' = t'' gA(gD fD) t = t'' gA fA -- cf. instCategoryIrreflexiveGraph.comp above X:TypeP:TypeY:TypeQ:TypeZ:TypeR:Types:X Pt:X Ps':Y Qt':Y Qs'':Z Rt'':Z RfA:X YfD:P QgA:Y ZgD:Q RhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAhgSrc_comm:gD s' = s'' gAhgTgt_comm:gD t' = t'' gA(gD fD) s = s'' gA fA All goals completed! 🐙 X:TypeP:TypeY:TypeQ:TypeZ:TypeR:Types:X Pt:X Ps':Y Qt':Y Qs'':Z Rt'':Z RfA:X YfD:P QgA:Y ZgD:Q RhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAhgSrc_comm:gD s' = s'' gAhgTgt_comm:gD t' = t'' gA(gD fD) t = t'' gA fA All goals completed! 🐙

Equivalently, we can use our implementation of the category 𝑺⇊ of graphs.

def graph (A D : Type) (src tgt : A D) : IrreflexiveGraph := { tA := A carrierA := Set.univ tD := D carrierD := Set.univ toSrc := src toSrc_mem := fun _ Set.mem_univ _ toTgt := tgt toTgt_mem := fun _ Set.mem_univ _ } example (f : graph X P s t graph Y Q s' t') (g : graph Y Q s' t' graph Z R s'' t'') : graph X P s t graph Z R s'' t'' := g f

6. Endomaps as special graphs

Exercise 12 (p. 143)

If we denote the result of the [insertion] process by I(f), then {I(g \circ f) = I(g) \circ I(f)} so that our insertion I preserves the fundamental operation of categories.

Solution: Exercise 12

The insertion I maps endomaps of sets to irreflexive graphs and maps morphisms between endomaps of sets to morphisms between irreflexive graphs — in other words, I is a functor. We again use our implementation of the category 𝑺⇊ of graphs.

def functorSetWithEndomapToIrreflexiveGraph : Functor SetWithEndomap IrreflexiveGraph := { obj (X : SetWithEndomap) := { tA := X.t carrierA := Set.univ tD := X.t carrierD := Set.univ toSrc := 𝟙 X.t toSrc_mem := fun _ Set.mem_univ _ toTgt := X.toEnd toTgt_mem := fun _ Set.mem_univ _ } map {X Y : SetWithEndomap} (f : X Y) := { val := (f, f) property := X:SetWithEndomapY:SetWithEndomapf:X Y(∀ x { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toSrc := 𝟙 X.t, toSrc_mem := , toTgt := X.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.carrierA) (∀ x { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toSrc := 𝟙 X.t, toSrc_mem := , toTgt := X.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toSrc := 𝟙 X.t, toSrc_mem := , toTgt := X.toEnd, toTgt_mem := }.toSrc = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toSrc := 𝟙 X.t, toSrc_mem := , toTgt := X.toEnd, toTgt_mem := }.toTgt = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 Y:SetWithEndomaptX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝: {a : tX}, a carrierX toEndX a carrierXf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ } Y(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toSrc := 𝟙 Y.t, toSrc_mem := , toTgt := Y.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ } { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toSrc = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toTgt = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.thf_mtc: x { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.carrier, f x { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.carrierhf_comm:f { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd = { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd f(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierD) ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toSrc = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toTgt = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierD) ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toSrc = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toTgt = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierAtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierDtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toSrc = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toTgt = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierAtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.carrierDtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toSrc = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toSrc ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, toSrc_mem := , toTgt := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toTgt_mem := }.toTgt = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toSrc := 𝟙 { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, toSrc_mem := , toTgt := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toTgt_mem := }.toTgt ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 (tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(ConcreteCategory.hom f, ) toEndX = toEndY (ConcreteCategory.hom f, ); tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(ConcreteCategory.hom f, ) toEndX = toEndY (ConcreteCategory.hom f, ); All goals completed! 🐙) } } -- Helper function to align to the notation in the book def I {X Y : SetWithEndomap} (f : X Y) := functorSetWithEndomapToIrreflexiveGraph.map f example {X Y Z : SetWithEndomap} (f : X Y) (g : Y Z) : I (g f) = I g I f := rfl
Exercise 13 (p. 144)

(Fullness) Show that if we are given any 𝑺⇊-morphism X \xrightarrow{f_A} Y,\; X \xrightarrow{f_D} Y between the special graphs that come via I from endomaps of sets, then it follows that {f_A = f_D}, so that the map itself comes via I from a map in 𝑺↻.

Solution: Exercise 13variable (X' Y' : SetWithEndomap)

Using Category IrreflexiveGraph, we have

def graph₁ (S : SetWithEndomap) : IrreflexiveGraph := { tA := S.t carrierA := Set.univ tD := S.t carrierD := Set.univ toSrc := 𝟙 S.t toSrc_mem := fun _ Set.mem_univ _ toTgt := S.toEnd toTgt_mem := fun _ Set.mem_univ _ } variable (f₁ : graph₁ X' graph₁ Y') -- Align to the notation in the book: fA is f₁.val.1, fD is f₁.val.2 set_option quotPrecheck false local notation "fA₁" => f₁.val.1 local notation "fD₁" => f₁.val.2 set_option quotPrecheck true example : fA₁ = fD₁ := X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'(↑f₁).1 = (↑f₁).2 X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'left✝¹: x (graph₁ X').carrierA, (↑f₁).1 x (graph₁ Y').carrierAleft✝: x (graph₁ X').carrierD, (↑f₁).2 x (graph₁ Y').carrierDhfSrc_comm:(↑f₁).2 (graph₁ X').toSrc = (graph₁ Y').toSrc (↑f₁).1right✝:(↑f₁).2 (graph₁ X').toTgt = (graph₁ Y').toTgt (↑f₁).1(↑f₁).1 = (↑f₁).2 X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'left✝¹: x (graph₁ X').carrierA, (↑f₁).1 x (graph₁ Y').carrierAleft✝: x (graph₁ X').carrierD, (↑f₁).2 x (graph₁ Y').carrierDhfSrc_comm:(↑f₁).2 𝟙 X'.t = 𝟙 Y'.t (↑f₁).1right✝:(↑f₁).2 (graph₁ X').toTgt = (graph₁ Y').toTgt (↑f₁).1(↑f₁).1 = (↑f₁).2 All goals completed! 🐙

Alternatively, using functorSetWithEndomapToIrreflexiveGraph, we have

def graph₂ (S : SetWithEndomap) : IrreflexiveGraph := functorSetWithEndomapToIrreflexiveGraph.obj S variable (f₂ : graph₂ X' graph₂ Y') set_option quotPrecheck false local notation "fA₂" => f₂.val.1 local notation "fD₂" => f₂.val.2 set_option quotPrecheck true example : fA₂ = fD₂ := X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'f₂:graph₂ X' graph₂ Y'(↑f₂).1 = (↑f₂).2 X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'f₂:graph₂ X' graph₂ Y'left✝¹: x (graph₂ X').carrierA, (↑f₂).1 x (graph₂ Y').carrierAleft✝: x (graph₂ X').carrierD, (↑f₂).2 x (graph₂ Y').carrierDhfSrc_comm:(↑f₂).2 (graph₂ X').toSrc = (graph₂ Y').toSrc (↑f₂).1right✝:(↑f₂).2 (graph₂ X').toTgt = (graph₂ Y').toTgt (↑f₂).1(↑f₂).1 = (↑f₂).2 X':SetWithEndomapY':SetWithEndomapf₁:graph₁ X' graph₁ Y'f₂:graph₂ X' graph₂ Y'left✝¹: x (graph₂ X').carrierA, (↑f₂).1 x (graph₂ Y').carrierAleft✝: x (graph₂ X').carrierD, (↑f₂).2 x (graph₂ Y').carrierDhfSrc_comm:(↑f₂).2 𝟙 X'.t = 𝟙 Y'.t (↑f₂).1right✝:(↑f₂).2 (graph₂ X').toTgt = (graph₂ Y').toTgt (↑f₂).1(↑f₂).1 = (↑f₂).2 All goals completed! 🐙

7. The simpler category 𝑺↓: Objects are just maps of sets

The category 𝑺↓ of simple directed graphs is described on pp. 144–145. We implement the category 𝑺↓ below.

structure SimpleGraph where tA : Type carrierA : Set tA tD : Type carrierD : Set tD toFun : tA tD toFun_mem {a} : a carrierA toFun a carrierD instance : Category SimpleGraph where Hom X Y := { f : (X.tA Y.tA) × (X.tD Y.tD) // ( x X.carrierA, f.1 x Y.carrierA) -- fA maps to codomain ( x X.carrierD, f.2 x Y.carrierD) -- fD maps to codomain f.2 X.toFun = Y.toFun f.1 -- commutes } id X := (𝟙 X.tA, 𝟙 X.tD), X:SimpleGraph(∀ x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierA) (∀ x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierD) (𝟙 X.tA, 𝟙 X.tD).2 X.toFun = X.toFun (𝟙 X.tA, 𝟙 X.tD).1 X:SimpleGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:SimpleGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:SimpleGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toFun = X.toFun (𝟙 X.tA, 𝟙 X.tD).1 X:SimpleGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:SimpleGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:SimpleGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toFun = X.toFun (𝟙 X.tA, 𝟙 X.tD).1 first | X:SimpleGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toFun = X.toFun (𝟙 X.tA, 𝟙 X.tD).1 | All goals completed! 🐙 comp := {X Y Z : SimpleGraph} { f // (∀ x X.carrierA, f.1 x Y.carrierA) (∀ x X.carrierD, f.2 x Y.carrierD) f.2 X.toFun = Y.toFun f.1 } { f // (∀ x Y.carrierA, f.1 x Z.carrierA) (∀ x Y.carrierD, f.2 x Z.carrierD) f.2 Y.toFun = Z.toFun f.1 } { f // (∀ x X.carrierA, f.1 x Z.carrierA) (∀ x X.carrierD, f.2 x Z.carrierD) f.2 X.toFun = Z.toFun f.1 } X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toFun = Y✝.toFun f.1g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toFun = Z✝.toFun g.1{ f // (∀ x X✝.carrierA, f.1 x Z✝.carrierA) (∀ x X✝.carrierD, f.2 x Z✝.carrierD) f.2 X✝.toFun = Z✝.toFun f.1 } exact (g.1 f.1, g.2 f.2), X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toFun = Y✝.toFun f.1g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toFun = Z✝.toFun g.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toFun = Z✝.toFun (g.1 f.1, g.2 f.2).1 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toFun = Z✝.toFun g.1hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toFun = Z✝.toFun (g.1 f.1, g.2 f.2).1 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toFun = Z✝.toFun (g.1 f.1, g.2 f.2).1 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierAX✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierDX✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1(g.1 f.1, g.2 f.2).2 X✝.toFun = Z✝.toFun (g.1 f.1, g.2 f.2).1 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA intro x X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1x:X✝.tAhx:x X✝.carrierA(g.1 f.1, g.2 f.2).1 x Z✝.carrierA All goals completed! 🐙 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD intro x X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1x:X✝.tDhx:x X✝.carrierD(g.1 f.1, g.2 f.2).2 x Z✝.carrierD All goals completed! 🐙 X✝:SimpleGraphY✝:SimpleGraphZ✝:SimpleGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toFun = Y✝.toFun f.1hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toFun = Z✝.toFun g.1(g.1 f.1, g.2 f.2).2 X✝.toFun = Z✝.toFun (g.1 f.1, g.2 f.2).1 All goals completed! 🐙

The insertion J is a functor from 𝑺↻ to 𝑺↓.

def functorSetWithEndomapToSimpleGraph : Functor SetWithEndomap SimpleGraph := { obj (X : SetWithEndomap) := { tA := X.t carrierA := Set.univ tD := X.t carrierD := Set.univ toFun := X.toEnd toFun_mem := fun _ Set.mem_univ _ } map {X Y : SetWithEndomap} (f : X Y) := { val := (f, f) property := X:SetWithEndomapY:SetWithEndomapf:X Y(∀ x { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toFun := X.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.carrierA) (∀ x { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toFun := X.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := X.t, carrierA := Set.univ, tD := X.t, carrierD := Set.univ, toFun := X.toEnd, toFun_mem := }.toFun = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 Y:SetWithEndomaptX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝: {a : tX}, a carrierX toEndX a carrierXf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ } Y(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun = { tA := Y.t, carrierA := Set.univ, tD := Y.t, carrierD := Set.univ, toFun := Y.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ } { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierD) ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.toFun = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f), (ConcreteCategory.hom f)).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:{ t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.thf_mtc: x { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.carrier, f x { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.carrierhf_comm:f { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd = { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd f(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierD) ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.toFun = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierA) (∀ x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierD) ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.toFun = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierAtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierDtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.toFun = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierA, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierAtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f x { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.carrierD, ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 x { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.carrierDtX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).2 { tA := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierA := Set.univ, tD := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.t, carrierD := Set.univ, toFun := { t := tX, carrier := carrierX, toEnd := toEndX, toEnd_mem := toEnd_mem✝¹ }.toEnd, toFun_mem := }.toFun = { tA := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierA := Set.univ, tD := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.t, carrierD := Set.univ, toFun := { t := tY, carrier := carrierY, toEnd := toEndY, toEnd_mem := toEnd_mem✝ }.toEnd, toFun_mem := }.toFun ((ConcreteCategory.hom f, ), (ConcreteCategory.hom f, )).1 (tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(ConcreteCategory.hom f, ) toEndX = toEndY (ConcreteCategory.hom f, ); tX:TypecarrierX:Set tXtoEndX:tX tXtoEnd_mem✝¹: {a : tX}, a carrierX toEndX a carrierXtY:TypecarrierY:Set tYtoEndY:tY tYtoEnd_mem✝: {a : tY}, a carrierY toEndY a carrierYf:tX tYhf_mtc: x carrierX, f x carrierYhf_comm:f toEndX = toEndY f(ConcreteCategory.hom f, ) toEndX = toEndY (ConcreteCategory.hom f, ); All goals completed! 🐙) } } -- Helper function to align to the notation in the book def J {X Y : SetWithEndomap} (f : X Y) := functorSetWithEndomapToSimpleGraph.map f example {X Y Z : SetWithEndomap} (f : X Y) (g : Y Z) : J (g f) = J g J f := rfl
Exercise 14 (p. 144)

Give an example of 𝑺 of two endomaps and two maps as in X \xrightarrow{f_A} Y,\; X \xrightarrow{f_D} Y,\; X \xrightarrow{\alpha} X,\; Y \xrightarrow{\beta} Y which satisfy the equation {f_D \circ \alpha = \beta \circ f_A}, but for which {f_A \ne f_D}.

Solution: Exercise 14

We give X, Y, \alpha, \beta, f_A, f_D as follows:

inductive X | x₁ | x₂ inductive Y | y₁ | y₂ def α : X X | X.x₁ => X.x₁ | X.x₂ => X.x₁ def β : Y Y | Y.y₁ => Y.y₁ | Y.y₂ => Y.y₁ def fA : X Y | X.x₁ => Y.y₁ | X.x₂ => Y.y₂ def fD : X Y | X.x₁ => Y.y₁ | X.x₂ => Y.y₁

We show that our example satisfies the required properties.

example : fD α = β fA fA fD := fD α = β fA fA fD fD α = β fAfA fD fD α = β fA x:X(fD α) x = (β fA) x (fD α) X.x₁ = (β fA) X.x₁(fD α) X.x₂ = (β fA) X.x₂ (fD α) X.x₁ = (β fA) X.x₁(fD α) X.x₂ = (β fA) X.x₂ All goals completed! 🐙 fA fD h:fA = fDFalse h:fA = fDh_contra:fA X.x₂ = fD X.x₂ := congrFun h X.x₂False h:fA = fDh_contra:Y.y₂ = Y.y₁ := congrFun h X.x₂False All goals completed! 🐙

8. Reflexive graphs

The category of reflexive graphs is described on p. 145. We implement this category below.

structure ReflexiveGraph extends IrreflexiveGraph where toCommonSection : tD tA toCommonSection_mem {d} : d carrierD toCommonSection d carrierA section_src : toSrc toCommonSection = 𝟙 tD section_tgt : toTgt toCommonSection = 𝟙 tD instance : Category ReflexiveGraph where Hom X Y := { f : (X.tA Y.tA) × (X.tD Y.tD) // ( x X.carrierA, f.1 x Y.carrierA) -- fA maps to codomain ( x X.carrierD, f.2 x Y.carrierD) -- fD maps to codomain f.2 X.toSrc = Y.toSrc f.1 -- source commutes f.2 X.toTgt = Y.toTgt f.1 -- target commutes f.1 X.toCommonSection = Y.toCommonSection f.2 } id X := (𝟙 X.tA, 𝟙 X.tD), X:ReflexiveGraph(∀ x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierA) (∀ x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierD) (𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1 (𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1 (𝟙 X.tA, 𝟙 X.tD).1 X.toCommonSection = X.toCommonSection (𝟙 X.tA, 𝟙 X.tD).2 X:ReflexiveGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:ReflexiveGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1X:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1X:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).1 X.toCommonSection = X.toCommonSection (𝟙 X.tA, 𝟙 X.tD).2 X:ReflexiveGraph x X.carrierA, (𝟙 X.tA, 𝟙 X.tD).1 x X.carrierAX:ReflexiveGraph x X.carrierD, (𝟙 X.tA, 𝟙 X.tD).2 x X.carrierDX:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toSrc = X.toSrc (𝟙 X.tA, 𝟙 X.tD).1X:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).2 X.toTgt = X.toTgt (𝟙 X.tA, 𝟙 X.tD).1X:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).1 X.toCommonSection = X.toCommonSection (𝟙 X.tA, 𝟙 X.tD).2 first | X:ReflexiveGraph(𝟙 X.tA, 𝟙 X.tD).1 X.toCommonSection = X.toCommonSection (𝟙 X.tA, 𝟙 X.tD).2 | All goals completed! 🐙 comp := {X Y Z : ReflexiveGraph} { f // (∀ x X.carrierA, f.1 x Y.carrierA) (∀ x X.carrierD, f.2 x Y.carrierD) f.2 X.toSrc = Y.toSrc f.1 f.2 X.toTgt = Y.toTgt f.1 f.1 X.toCommonSection = Y.toCommonSection f.2 } { f // (∀ x Y.carrierA, f.1 x Z.carrierA) (∀ x Y.carrierD, f.2 x Z.carrierD) f.2 Y.toSrc = Z.toSrc f.1 f.2 Y.toTgt = Z.toTgt f.1 f.1 Y.toCommonSection = Z.toCommonSection f.2 } { f // (∀ x X.carrierA, f.1 x Z.carrierA) (∀ x X.carrierD, f.2 x Z.carrierD) f.2 X.toSrc = Z.toSrc f.1 f.2 X.toTgt = Z.toTgt f.1 f.1 X.toCommonSection = Z.toCommonSection f.2 } X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toSrc = Y✝.toSrc f.1 f.2 X✝.toTgt = Y✝.toTgt f.1 f.1 X✝.toCommonSection = Y✝.toCommonSection f.2g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1 g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2{ f // (∀ x X✝.carrierA, f.1 x Z✝.carrierA) (∀ x X✝.carrierD, f.2 x Z✝.carrierD) f.2 X✝.toSrc = Z✝.toSrc f.1 f.2 X✝.toTgt = Z✝.toTgt f.1 f.1 X✝.toCommonSection = Z✝.toCommonSection f.2 } exact (g.1 f.1, g.2 f.2), X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)hf:(∀ x X✝.carrierA, f.1 x Y✝.carrierA) (∀ x X✝.carrierD, f.2 x Y✝.carrierD) f.2 X✝.toSrc = Y✝.toSrc f.1 f.2 X✝.toTgt = Y✝.toTgt f.1 f.1 X✝.toCommonSection = Y✝.toCommonSection f.2g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1 g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.toCommonSection = Z✝.toCommonSection (g.1 f.1, g.2 f.2).2 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hg:(∀ x Y✝.carrierA, g.1 x Z✝.carrierA) (∀ x Y✝.carrierD, g.2 x Z✝.carrierD) g.2 Y✝.toSrc = Z✝.toSrc g.1 g.2 Y✝.toTgt = Z✝.toTgt g.1 g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.toCommonSection = Z✝.toCommonSection (g.1 f.1, g.2 f.2).2 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(∀ x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA) (∀ x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD) (g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.toCommonSection = Z✝.toCommonSection (g.1 f.1, g.2 f.2).2 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierAX✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierDX✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).1 X✝.toCommonSection = Z✝.toCommonSection (g.1 f.1, g.2 f.2).2 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2 x X✝.carrierA, (g.1 f.1, g.2 f.2).1 x Z✝.carrierA intro x X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2x:X✝.tAhx:x X✝.carrierA(g.1 f.1, g.2 f.2).1 x Z✝.carrierA All goals completed! 🐙 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2 x X✝.carrierD, (g.1 f.1, g.2 f.2).2 x Z✝.carrierD intro x X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2x:X✝.tDhx:x X✝.carrierD(g.1 f.1, g.2 f.2).2 x Z✝.carrierD All goals completed! 🐙 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).2 X✝.toSrc = Z✝.toSrc (g.1 f.1, g.2 f.2).1 All goals completed! 🐙 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).2 X✝.toTgt = Z✝.toTgt (g.1 f.1, g.2 f.2).1 All goals completed! 🐙 X✝:ReflexiveGraphY✝:ReflexiveGraphZ✝:ReflexiveGraphf:(X✝.tA Y✝.tA) × (X✝.tD Y✝.tD)g:(Y✝.tA Z✝.tA) × (Y✝.tD Z✝.tD)hfA_mtc: x X✝.carrierA, f.1 x Y✝.carrierAhfD_mtc: x X✝.carrierD, f.2 x Y✝.carrierDhfSrc_comm:f.2 X✝.toSrc = Y✝.toSrc f.1hfTgt_comm:f.2 X✝.toTgt = Y✝.toTgt f.1hfCommonSection_comm:f.1 X✝.toCommonSection = Y✝.toCommonSection f.2hgA_mtc: x Y✝.carrierA, g.1 x Z✝.carrierAhgD_mtc: x Y✝.carrierD, g.2 x Z✝.carrierDhgSrc_comm:g.2 Y✝.toSrc = Z✝.toSrc g.1hgTgt_comm:g.2 Y✝.toTgt = Z✝.toTgt g.1hgCommonSection_comm:g.1 Y✝.toCommonSection = Z✝.toCommonSection g.2(g.1 f.1, g.2 f.2).1 X✝.toCommonSection = Z✝.toCommonSection (g.1 f.1, g.2 f.2).2 All goals completed! 🐙
Exercise 15 (p. 145)

In a reflexive graph, the two endomaps {e_1 = is}, {e_0 = it} of the set of arrows are not only idempotent, but even satisfy four equations: e_k e_j = e_j \quad\text{for}\quad k, j = 0, 1.

Solution: Exercise 15

We use our implementation of the category of reflexive graphs.

variable (X : ReflexiveGraph)

Define the two endomaps {e_1 = is}, {e_0 = it}.

variable (e₁ e₀ : X.tA X.tA) (h₁ : e₁ = X.toCommonSection X.toSrc) (h₀ : e₀ = X.toCommonSection X.toTgt)

e_0 e_0 = e_0

example : e₀ e₀ = e₀ := X:ReflexiveGraphe₁:X.tA X.tAe₀:X.tA X.tAh₁:e₁ = X.toCommonSection X.toSrch₀:e₀ = X.toCommonSection X.toTgte₀ e₀ = e₀ All goals completed! 🐙

e_0 e_1 = e_1

example : e₀ e₁ = e₁ := X:ReflexiveGraphe₁:X.tA X.tAe₀:X.tA X.tAh₁:e₁ = X.toCommonSection X.toSrch₀:e₀ = X.toCommonSection X.toTgte₀ e₁ = e₁ All goals completed! 🐙

e_1 e_0 = e_0

example : e₁ e₀ = e₀ := X:ReflexiveGraphe₁:X.tA X.tAe₀:X.tA X.tAh₁:e₁ = X.toCommonSection X.toSrch₀:e₀ = X.toCommonSection X.toTgte₁ e₀ = e₀ All goals completed! 🐙

e_1 e_1 = e_1

example : e₁ e₁ = e₁ := X:ReflexiveGraphe₁:X.tA X.tAe₀:X.tA X.tAh₁:e₁ = X.toCommonSection X.toSrch₀:e₀ = X.toCommonSection X.toTgte₁ e₁ = e₁ All goals completed! 🐙
Exercise 16 (p. 145)

Show that if f_A, f_D in 𝑺 constitute a map of reflexive graphs, then f_D is determined by f_A and the internal structure of the two graphs.

Solution: Exercise 16

f is a morphism in our category of reflexive graphs.

variable (X Y : ReflexiveGraph) (f : X Y) -- Align to the notation in the book set_option quotPrecheck false local notation "fA" => f.val.1 local notation "fD" => f.val.2 set_option quotPrecheck true local notation "s" => X.toSrc local notation "s'" => Y.toSrc local notation "t" => X.toTgt local notation "t'" => Y.toTgt local notation "i" => X.toCommonSection local notation "i'" => Y.toCommonSection

Then f_D is determined by f_A and the internal structure of the two graphs.

example : fD = s' fA i := X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 = Y.toSrc (↑f).1 X.toCommonSection X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 X.toSrc X.toCommonSection = Y.toSrc (↑f).1 X.toCommonSection repeat X:ReflexiveGraphY:ReflexiveGraphf:X Y((↑f).2 X.toSrc) X.toCommonSection = (Y.toSrc (↑f).1) X.toCommonSection X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 X.toSrc = Y.toSrc (↑f).1 All goals completed! 🐙

Or, alternatively,

example : fD = t' fA i := X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 = Y.toTgt (↑f).1 X.toCommonSection X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 X.toTgt X.toCommonSection = Y.toTgt (↑f).1 X.toCommonSection repeat X:ReflexiveGraphY:ReflexiveGraphf:X Y((↑f).2 X.toTgt) X.toCommonSection = (Y.toTgt (↑f).1) X.toCommonSection X:ReflexiveGraphY:ReflexiveGraphf:X Y(↑f).2 X.toTgt = Y.toTgt (↑f).1 All goals completed! 🐙
Exercise 17 (p. 145)

Consider a structure involving two sets and four maps as in M \xrightarrow{\varphi} M,\; F \xrightarrow{\varphi'} M,\; F \xrightarrow{\mu} F,\; M \xrightarrow{\mu'} F \quad\text{(no equations required)} (for example {M = \mathit{males}}, {F = \mathit{females}}, \varphi and \varphi' are \mathit{father}, and \mu and \mu' are \mathit{mother}). Devise a rational definition of map between such structures in order to make them into a category.

Solution: Exercise 17

Define the structure.

structure ParentLike where tM : Type carrierM : Set tM tF : Type carrierF : Set tF φ : tM tM φ_mem {m} : m carrierM φ m carrierM φ' : tF tM φ'_mem {f} : f carrierF φ' f carrierM μ : tF tF μ_mem {f} : f carrierF μ f carrierF μ' : tM tF μ'_mem {m} : m carrierM μ' m carrierF

Define a map between such structures.

def ParentLikeHom (X Y : ParentLike) := { f : (X.tM Y.tM) × (X.tF Y.tF) // ( x X.carrierM, f.1 x Y.carrierM) -- f.1 maps to codomain ( x X.carrierF, f.2 x Y.carrierF) -- f.2 maps to codomain f.1 X.φ = Y.φ f.1 -- φ commutes f.1 X.φ' = Y.φ' f.2 -- φ' commutes f.2 X.μ = Y.μ f.2 -- μ commutes f.2 X.μ' = Y.μ' f.1 -- μ' commutes }

This map between structures makes them into a category.

instance : Category ParentLike where Hom := ParentLikeHom -- our map between ParentLike structures id X := (𝟙 X.tM, 𝟙 X.tF), X:ParentLike(∀ x X.carrierM, (𝟙 X.tM, 𝟙 X.tF).1 x X.carrierM) (∀ x X.carrierF, (𝟙 X.tM, 𝟙 X.tF).2 x X.carrierF) (𝟙 X.tM, 𝟙 X.tF).1 X.φ = X.φ (𝟙 X.tM, 𝟙 X.tF).1 (𝟙 X.tM, 𝟙 X.tF).1 X.φ' = X.φ' (𝟙 X.tM, 𝟙 X.tF).2 (𝟙 X.tM, 𝟙 X.tF).2 X.μ = X.μ (𝟙 X.tM, 𝟙 X.tF).2 (𝟙 X.tM, 𝟙 X.tF).2 X.μ' = X.μ' (𝟙 X.tM, 𝟙 X.tF).1 X:ParentLike x X.carrierM, (𝟙 X.tM, 𝟙 X.tF).1 x X.carrierMX:ParentLike x X.carrierF, (𝟙 X.tM, 𝟙 X.tF).2 x X.carrierFX:ParentLike(𝟙 X.tM, 𝟙 X.tF).1 X.φ = X.φ (𝟙 X.tM, 𝟙 X.tF).1X:ParentLike(𝟙 X.tM, 𝟙 X.tF).1 X.φ' = X.φ' (𝟙 X.tM, 𝟙 X.tF).2X:ParentLike(𝟙 X.tM, 𝟙 X.tF).2 X.μ = X.μ (𝟙 X.tM, 𝟙 X.tF).2X:ParentLike(𝟙 X.tM, 𝟙 X.tF).2 X.μ' = X.μ' (𝟙 X.tM, 𝟙 X.tF).1 X:ParentLike x X.carrierM, (𝟙 X.tM, 𝟙 X.tF).1 x X.carrierMX:ParentLike x X.carrierF, (𝟙 X.tM, 𝟙 X.tF).2 x X.carrierFX:ParentLike(𝟙 X.tM, 𝟙 X.tF).1 X.φ = X.φ (𝟙 X.tM, 𝟙 X.tF).1X:ParentLike(𝟙 X.tM, 𝟙 X.tF).1 X.φ' = X.φ' (𝟙 X.tM, 𝟙 X.tF).2X:ParentLike(𝟙 X.tM, 𝟙 X.tF).2 X.μ = X.μ (𝟙 X.tM, 𝟙 X.tF).2X:ParentLike(𝟙 X.tM, 𝟙 X.tF).2 X.μ' = X.μ' (𝟙 X.tM, 𝟙 X.tF).1 first | X:ParentLike(𝟙 X.tM, 𝟙 X.tF).2 X.μ' = X.μ' (𝟙 X.tM, 𝟙 X.tF).1 | All goals completed! 🐙 comp := {X Y Z : ParentLike} ParentLikeHom X Y ParentLikeHom Y Z ParentLikeHom X Z X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)hf:(∀ x X✝.carrierM, f.1 x Y✝.carrierM) (∀ x X✝.carrierF, f.2 x Y✝.carrierF) f.1 X✝.φ = Y✝.φ f.1 f.1 X✝.φ' = Y✝.φ' f.2 f.2 X✝.μ = Y✝.μ f.2 f.2 X✝.μ' = Y✝.μ' f.1g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hg:(∀ x Y✝.carrierM, g.1 x Z✝.carrierM) (∀ x Y✝.carrierF, g.2 x Z✝.carrierF) g.1 Y✝.φ = Z✝.φ g.1 g.1 Y✝.φ' = Z✝.φ' g.2 g.2 Y✝.μ = Z✝.μ g.2 g.2 Y✝.μ' = Z✝.μ' g.1ParentLikeHom X✝ Z✝ exact (g.1 f.1, g.2 f.2), X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)hf:(∀ x X✝.carrierM, f.1 x Y✝.carrierM) (∀ x X✝.carrierF, f.2 x Y✝.carrierF) f.1 X✝.φ = Y✝.φ f.1 f.1 X✝.φ' = Y✝.φ' f.2 f.2 X✝.μ = Y✝.μ f.2 f.2 X✝.μ' = Y✝.μ' f.1g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hg:(∀ x Y✝.carrierM, g.1 x Z✝.carrierM) (∀ x Y✝.carrierF, g.2 x Z✝.carrierF) g.1 Y✝.φ = Z✝.φ g.1 g.1 Y✝.φ' = Z✝.φ' g.2 g.2 Y✝.μ = Z✝.μ g.2 g.2 Y✝.μ' = Z✝.μ' g.1(∀ x X✝.carrierM, (g.1 f.1, g.2 f.2).1 x Z✝.carrierM) (∀ x X✝.carrierF, (g.1 f.1, g.2 f.2).2 x Z✝.carrierF) (g.1 f.1, g.2 f.2).1 X✝.φ = Z✝.φ (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.φ' = Z✝.φ' (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ = Z✝.μ (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ' = Z✝.μ' (g.1 f.1, g.2 f.2).1 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hg:(∀ x Y✝.carrierM, g.1 x Z✝.carrierM) (∀ x Y✝.carrierF, g.2 x Z✝.carrierF) g.1 Y✝.φ = Z✝.φ g.1 g.1 Y✝.φ' = Z✝.φ' g.2 g.2 Y✝.μ = Z✝.μ g.2 g.2 Y✝.μ' = Z✝.μ' g.1hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1(∀ x X✝.carrierM, (g.1 f.1, g.2 f.2).1 x Z✝.carrierM) (∀ x X✝.carrierF, (g.1 f.1, g.2 f.2).2 x Z✝.carrierF) (g.1 f.1, g.2 f.2).1 X✝.φ = Z✝.φ (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.φ' = Z✝.φ' (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ = Z✝.μ (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ' = Z✝.μ' (g.1 f.1, g.2 f.2).1 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(∀ x X✝.carrierM, (g.1 f.1, g.2 f.2).1 x Z✝.carrierM) (∀ x X✝.carrierF, (g.1 f.1, g.2 f.2).2 x Z✝.carrierF) (g.1 f.1, g.2 f.2).1 X✝.φ = Z✝.φ (g.1 f.1, g.2 f.2).1 (g.1 f.1, g.2 f.2).1 X✝.φ' = Z✝.φ' (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ = Z✝.μ (g.1 f.1, g.2 f.2).2 (g.1 f.1, g.2 f.2).2 X✝.μ' = Z✝.μ' (g.1 f.1, g.2 f.2).1 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1 x X✝.carrierM, (g.1 f.1, g.2 f.2).1 x Z✝.carrierMX✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1 x X✝.carrierF, (g.1 f.1, g.2 f.2).2 x Z✝.carrierFX✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).1 X✝.φ = Z✝.φ (g.1 f.1, g.2 f.2).1X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).1 X✝.φ' = Z✝.φ' (g.1 f.1, g.2 f.2).2X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).2 X✝.μ = Z✝.μ (g.1 f.1, g.2 f.2).2X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).2 X✝.μ' = Z✝.μ' (g.1 f.1, g.2 f.2).1 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1 x X✝.carrierM, (g.1 f.1, g.2 f.2).1 x Z✝.carrierM intro x X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1x:X✝.tMhx:x X✝.carrierM(g.1 f.1, g.2 f.2).1 x Z✝.carrierM All goals completed! 🐙 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1 x X✝.carrierF, (g.1 f.1, g.2 f.2).2 x Z✝.carrierF intro x X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1x:X✝.tFhx:x X✝.carrierF(g.1 f.1, g.2 f.2).2 x Z✝.carrierF All goals completed! 🐙 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).1 X✝.φ = Z✝.φ (g.1 f.1, g.2 f.2).1 All goals completed! 🐙 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).1 X✝.φ' = Z✝.φ' (g.1 f.1, g.2 f.2).2 All goals completed! 🐙 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).2 X✝.μ = Z✝.μ (g.1 f.1, g.2 f.2).2 All goals completed! 🐙 X✝:ParentLikeY✝:ParentLikeZ✝:ParentLikef:(X✝.tM Y✝.tM) × (X✝.tF Y✝.tF)g:(Y✝.tM Z✝.tM) × (Y✝.tF Z✝.tF)hfM_mtc: x X✝.carrierM, f.1 x Y✝.carrierMhfF_mtc: x X✝.carrierF, f.2 x Y✝.carrierFhfφ_comm:f.1 X✝.φ = Y✝.φ f.1hfφ'_comm:f.1 X✝.φ' = Y✝.φ' f.2hfμ_comm:f.2 X✝.μ = Y✝.μ f.2hfμ'_comm:f.2 X✝.μ' = Y✝.μ' f.1hgM_mtc: x Y✝.carrierM, g.1 x Z✝.carrierMhgF_mtc: x Y✝.carrierF, g.2 x Z✝.carrierFhgφ_comm:g.1 Y✝.φ = Z✝.φ g.1hgφ'_comm:g.1 Y✝.φ' = Z✝.φ' g.2hgμ_comm:g.2 Y✝.μ = Z✝.μ g.2hgμ'_comm:g.2 Y✝.μ' = Z✝.μ' g.1(g.1 f.1, g.2 f.2).2 X✝.μ' = Z✝.μ' (g.1 f.1, g.2 f.2).1 All goals completed! 🐙

10. Retractions and injectivity

Definition: Injective (p. 146)

We say that a map {X \xrightarrow{a} Y} is injective iff for any maps {T \xrightarrow{x_1} X} and {T \xrightarrow{x_2} X} (in the same category) if {ax_1 = ax_2} then {x_1 = x_2} (or, in contrapositive form, 'the map a does not destroy distinctions', i.e. if {x_1 \ne x_2}..., then {ax_1 \ne ax_2} as well).

cf. the earlier definition of injective on p. 52.

Exercise 18 (p. 146)

If a has a retraction, then a is injective. (Assume {pa = 1_X} and {ax_1 = ax_2}; then try to show by calculation that {x_1 = x_2}.)

Solution: Exercise 18

cf. mono_iff_injective.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {X Y T : 𝒞} {a : X Y} {p : Y X} {x₁ x₂ : T X} (h₁ : p a = 𝟙 X) (h₂ : a x₁ = a x₂) : x₁ = x₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂x₁ = x₂ calc x₁ _ = 𝟙 X x₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂x₁ = 𝟙 X x₁ All goals completed! 🐙 _ = (p a) x₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂𝟙 X x₁ = (p a) x₁ All goals completed! 🐙 _ = p a x₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂(p a) x₁ = p a x₁ All goals completed! 🐙 _ = p a x₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂p a x₁ = p a x₂ All goals completed! 🐙 _ = (p a) x₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂p a x₂ = (p a) x₂ All goals completed! 🐙 _ = 𝟙 X x₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂(p a) x₂ = 𝟙 X x₂ All goals completed! 🐙 _ = x₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞X:𝒞Y:𝒞T:𝒞a:X Yp:Y Xx₁:T Xx₂:T Xh₁:p a = 𝟙 Xh₂:a x₁ = a x₂𝟙 X x₂ = x₂ All goals completed! 🐙

Exercises 19–24 that follow relate to the sets X and Y, the endomaps \alpha and \beta, and the map a as defined below. (Note that we in fact define X and Y as finite types rather than finite sets.)

inductive X | x₀ | x₁ deriving Fintype inductive Y | y₀ | y₁ | y₂ deriving Fintype def α : X X | X.x₀ => X.x₀ | X.x₁ => X.x₀ def β : Y Y | Y.y₀ => Y.y₀ | Y.y₁ => Y.y₀ | Y.y₂ => Y.y₁ def a : X Y | X.x₀ => Y.y₀ | X.x₁ => Y.y₁
Exercise 19 (p. 147)

Show that a is a map {X^{↻\alpha} \xrightarrow{a} Y^{↻\beta}} in 𝑺↻.

Solution: Exercise 19

a is a map in 𝑺↻ if it satisfies the condition {a \alpha = \beta a}.

example : a α = β a := a α = β a x:X(a α) x = (β a) x (a α) X.x₀ = (β a) X.x₀(a α) X.x₁ = (β a) X.x₁ (a α) X.x₀ = (β a) X.x₀(a α) X.x₁ = (β a) X.x₁ All goals completed! 🐙

Or, alternatively, using the categorical framework we defined earlier, a is a map in 𝑺↻ if it is a morphism in our category of endomaps of sets.

def : SetWithEndomap := { t := X carrier := Set.univ toEnd := α toEnd_mem := fun _ Set.mem_univ _ } def : SetWithEndomap := { t := Y carrier := Set.univ toEnd := β toEnd_mem := fun _ Set.mem_univ _ } def a' : := a, (∀ x .carrier, ExIII_19_24.a x .carrier) a .toEnd = .toEnd a x .carrier, ExIII_19_24.a x .carriera .toEnd = .toEnd a x .carrier, ExIII_19_24.a x .carrier All goals completed! 🐙 a .toEnd = .toEnd a x:.t(a .toEnd) x = (.toEnd a) x (a .toEnd) X.x₀ = (.toEnd a) X.x₀(a .toEnd) X.x₁ = (.toEnd a) X.x₁ (a .toEnd) X.x₀ = (.toEnd a) X.x₀(a .toEnd) X.x₁ = (.toEnd a) X.x₁ All goals completed! 🐙
Exercise 20 (p. 147)

Show that a is injective.

Solution: Exercise 20

cf. Exercise 18 above.

example : {T : Type} (x₁ x₂ : T X), a x₁ = a x₂ x₁ = x₂ := {T : Type} (x₁ x₂ : T X), a x₁ = a x₂ x₁ = x₂ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁ {T : Type} (x₁ x₂ : T X), a x₁ = a x₂ x₁ = x₂ have h₁ : p a = 𝟙 X := {T : Type} (x₁ x₂ : T X), a x₁ = a x₂ x₁ = x₂ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁x:X(p a) x = 𝟙 X x p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁(p a) X.x₀ = 𝟙 X X.x₀p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁(p a) X.x₁ = 𝟙 X X.x₁ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁(p a) X.x₀ = 𝟙 X X.x₀p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁(p a) X.x₁ = 𝟙 X X.x₁ All goals completed! 🐙 intro _ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ X (x₂ : T✝ X), a x₁ = a x₂ x₁ = x₂ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xa x₁ = a x₂ x₁ = x₂ p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂x₁ = x₂ calc x₁ _ = 𝟙 X x₁ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂x₁ = 𝟙 X x₁ All goals completed! 🐙 _ = (p a) x₁ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂𝟙 X x₁ = (p a) x₁ All goals completed! 🐙 _ = p a x₁ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂(p a) x₁ = p a x₁ All goals completed! 🐙 _ = p a x₂ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂p a x₁ = p a x₂ All goals completed! 🐙 _ = (p a) x₂ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂p a x₂ = (p a) x₂ All goals completed! 🐙 _ = 𝟙 X x₂ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂(p a) x₂ = 𝟙 X x₂ All goals completed! 🐙 _ = x₂ := p:Y X := fun x match x with | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁h₁:p a = 𝟙 X := funext fun x X.casesOn (motive := fun t x = t (p a) x = 𝟙 X x) x (fun h Eq.symm h Eq.refl ((p a) X.x₀)) (fun h Eq.symm h Eq.refl ((p a) X.x₁)) (Eq.refl x)T✝:Typex₁:T✝ Xx₂:T✝ Xh₂:a x₁ = a x₂𝟙 X x₂ = x₂ All goals completed! 🐙
Exercise 21 (p. 147)

Show that, as a map {X \xrightarrow{a} Y} in 𝑺, a has exactly two retractions p.

Solution: Exercise 21

We found one retraction p_1 in Exercise 20.

def p₁ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁ example : p₁ a = 𝟙 X := p₁ a = 𝟙 X x:X(p₁ a) x = 𝟙 X x (p₁ a) X.x₀ = 𝟙 X X.x₀(p₁ a) X.x₁ = 𝟙 X X.x₁ (p₁ a) X.x₀ = 𝟙 X X.x₀(p₁ a) X.x₁ = 𝟙 X X.x₁ All goals completed! 🐙

Using p_1 with Danilo's formula, we find that a has exactly two retractions.

2#eval Danilo's_formula (Finset.univ) (Finset.univ) a p₁ (p₁ a = id x:X(p₁ a) x = id x (p₁ a) X.x₀ = id X.x₀(p₁ a) X.x₁ = id X.x₁ (p₁ a) X.x₀ = id X.x₀(p₁ a) X.x₁ = id X.x₁ All goals completed! 🐙) (Function.Injective a intro x x:Xy:Xa x = a y x = y x:Xy:Xa✝:a x = a yx = y y:Xa✝:a X.x₀ = a yX.x₀ = yy:Xa✝:a X.x₁ = a yX.x₁ = y y:Xa✝:a X.x₀ = a yX.x₀ = yy:Xa✝:a X.x₁ = a yX.x₁ = y a✝:a X.x₁ = a X.x₀X.x₁ = X.x₀a✝:a X.x₁ = a X.x₁X.x₁ = X.x₁ all_goals first | All goals completed! 🐙 | a✝:a X.x₁ = a X.x₀False; All goals completed! 🐙)
2

The other retraction p_2 is

def p₂ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₀ example : p₂ a = 𝟙 X := p₂ a = 𝟙 X x:X(p₂ a) x = 𝟙 X x (p₂ a) X.x₀ = 𝟙 X X.x₀(p₂ a) X.x₁ = 𝟙 X X.x₁ (p₂ a) X.x₀ = 𝟙 X X.x₀(p₂ a) X.x₁ = 𝟙 X X.x₁ All goals completed! 🐙
Exercise 22 (p. 147)

Show that neither of the maps p found in the preceding exercise is a map {Y^{↻\beta} \rightarrow X^{↻\alpha}} in 𝑺↻. Hence a has no retractions in 𝑺↻.

Solution: Exercise 22

p_1 is not a map {Y^{↻\beta} \rightarrow X^{↻\alpha}} in 𝑺↻.

example : ¬(p₁ β = α p₁) := ¬p₁ β = α p₁ h:p₁ β = α p₁False h:p₁ β = α p₁h_contra:(p₁ β) Y.y₂ = (α p₁) Y.y₂ := congrFun h Y.y₂False h:p₁ β = α p₁h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙

p_2 is not a map {Y^{↻\beta} \rightarrow X^{↻\alpha}} in 𝑺↻.

example : ¬(p₂ β = α p₂) := ¬p₂ β = α p₂ h:p₂ β = α p₂False h:p₂ β = α p₂h_contra:(p₂ β) Y.y₂ = (α p₂) Y.y₂ := congrFun h Y.y₂False h:p₂ β = α p₂h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙

Since, by Exercise 21, p_1 and p_2 are the only retractions of a in 𝑺, they are the only candidates for retractions of a in 𝑺↻; hence a has no retractions in 𝑺↻.

Exercise 23 (p. 147)

How many of the eight 𝑺-maps {Y \rightarrow X} (if any) are actually 𝑺↻-maps? Y^{↻\beta} \rightarrow X^{↻\alpha}

Solution: Exercise 23

For an 𝑺-map b to be an 𝑺↻-map, we require that {b \beta = \alpha b}. Since {\alpha b = x_0}, it follows that we require {b \beta = x_0}. That is, we require {b(y_0) = x_0} and {b(y_1) = x_0}, which leaves b(y_2) as the only degree of freedom. Hence just two of the eight 𝑺-maps {Y \rightarrow X} are actually 𝑺↻-maps {Y^{↻\beta} \rightarrow X^{↻\alpha}}, as given below.

The 𝑺-maps b_1 and b_2 are 𝑺↻-maps.

def b₁ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₀ | Y.y₂ => X.x₀ example : b₁ β = α b₁ := b₁ β = α b₁ y:Y(b₁ β) y = (α b₁) y (b₁ β) Y.y₀ = (α b₁) Y.y₀(b₁ β) Y.y₁ = (α b₁) Y.y₁(b₁ β) Y.y₂ = (α b₁) Y.y₂ (b₁ β) Y.y₀ = (α b₁) Y.y₀(b₁ β) Y.y₁ = (α b₁) Y.y₁(b₁ β) Y.y₂ = (α b₁) Y.y₂ All goals completed! 🐙 def b₂ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₀ | Y.y₂ => X.x₁ example : b₂ β = α b₂ := b₂ β = α b₂ y:Y(b₂ β) y = (α b₂) y (b₂ β) Y.y₀ = (α b₂) Y.y₀(b₂ β) Y.y₁ = (α b₂) Y.y₁(b₂ β) Y.y₂ = (α b₂) Y.y₂ (b₂ β) Y.y₀ = (α b₂) Y.y₀(b₂ β) Y.y₁ = (α b₂) Y.y₁(b₂ β) Y.y₂ = (α b₂) Y.y₂ All goals completed! 🐙

The remaining 𝑺-maps b_3 to b_8 are not 𝑺↻-maps.

def b₃ : Y X | Y.y₀ => X.x₁ | Y.y₁ => X.x₀ | Y.y₂ => X.x₀ example : b₃ β α b₃ := b₃ β α b₃ h:b₃ β = α b₃False h:b₃ β = α b₃h_contra:(b₃ β) Y.y₀ = (α b₃) Y.y₀ := congrFun h Y.y₀False h:b₃ β = α b₃h_contra:X.x₁ = X.x₀ := congrFun h Y.y₀False All goals completed! 🐙 def b₄ : Y X | Y.y₀ => X.x₁ | Y.y₁ => X.x₀ | Y.y₂ => X.x₁ example : b₄ β α b₄ := b₄ β α b₄ h:b₄ β = α b₄False h:b₄ β = α b₄h_contra:(b₄ β) Y.y₀ = (α b₄) Y.y₀ := congrFun h Y.y₀False h:b₄ β = α b₄h_contra:X.x₁ = X.x₀ := congrFun h Y.y₀False All goals completed! 🐙 def b₅ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₀ example : b₅ β α b₅ := b₅ β α b₅ h:b₅ β = α b₅False h:b₅ β = α b₅h_contra:(b₅ β) Y.y₂ = (α b₅) Y.y₂ := congrFun h Y.y₂False h:b₅ β = α b₅h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙 def b₆ : Y X | Y.y₀ => X.x₀ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁ example : b₆ β α b₆ := b₆ β α b₆ h:b₆ β = α b₆False h:b₆ β = α b₆h_contra:(b₆ β) Y.y₂ = (α b₆) Y.y₂ := congrFun h Y.y₂False h:b₆ β = α b₆h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙 def b₇ : Y X | Y.y₀ => X.x₁ | Y.y₁ => X.x₁ | Y.y₂ => X.x₀ example : b₇ β α b₇ := b₇ β α b₇ h:b₇ β = α b₇False h:b₇ β = α b₇h_contra:(b₇ β) Y.y₂ = (α b₇) Y.y₂ := congrFun h Y.y₂False h:b₇ β = α b₇h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙 def b₈ : Y X | Y.y₀ => X.x₁ | Y.y₁ => X.x₁ | Y.y₂ => X.x₁ example : b₈ β α b₈ := b₈ β α b₈ h:b₈ β = α b₈False h:b₈ β = α b₈h_contra:(b₈ β) Y.y₂ = (α b₈) Y.y₂ := congrFun h Y.y₂False h:b₈ β = α b₈h_contra:X.x₁ = X.x₀ := congrFun h Y.y₂False All goals completed! 🐙
Exercise 24 (p. 147)

Show that our map a does not have any retractions, even when considered (via the insertion J in Section 7 of this article) as being a map in the 'looser' category 𝑺↓.

Solution: Exercise 24

Emulating the insertion J,

def X' : SimpleGraph := { tA := X carrierA := Set.univ tD := X carrierD := Set.univ toFun := α toFun_mem := fun _ Set.mem_univ _ } def Y' : SimpleGraph := { tA := Y carrierA := Set.univ tD := Y carrierD := Set.univ toFun := β toFun_mem := fun _ Set.mem_univ _ } def a'' : X' Y' := (a, a), (∀ x X'.carrierA, (ExIII_19_24.a, ExIII_19_24.a).1 x Y'.carrierA) (∀ x X'.carrierD, (ExIII_19_24.a, ExIII_19_24.a).2 x Y'.carrierD) (a, a).2 X'.toFun = Y'.toFun (a, a).1 x X'.carrierA, (ExIII_19_24.a, ExIII_19_24.a).1 x Y'.carrierA x X'.carrierD, (ExIII_19_24.a, ExIII_19_24.a).2 x Y'.carrierD(a, a).2 X'.toFun = Y'.toFun (a, a).1 x X'.carrierA, (ExIII_19_24.a, ExIII_19_24.a).1 x Y'.carrierA All goals completed! 🐙 x X'.carrierD, (ExIII_19_24.a, ExIII_19_24.a).2 x Y'.carrierD All goals completed! 🐙 (a, a).2 X'.toFun = Y'.toFun (a, a).1 x:X'.tA((a, a).2 X'.toFun) x = (Y'.toFun (a, a).1) x ((a, a).2 X'.toFun) X.x₀ = (Y'.toFun (a, a).1) X.x₀((a, a).2 X'.toFun) X.x₁ = (Y'.toFun (a, a).1) X.x₁ ((a, a).2 X'.toFun) X.x₀ = (Y'.toFun (a, a).1) X.x₀((a, a).2 X'.toFun) X.x₁ = (Y'.toFun (a, a).1) X.x₁ All goals completed! 🐙

we can show that a has no retractions.

example : ¬( p : Y' X', p a'' = 𝟙 X') := ¬ p, p a'' = 𝟙 X' (p : Y' X'), p a'' 𝟙 X' p:Y' X'p a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 Y'.toFun = X'.toFun p.1p, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1p, a'' 𝟙 X' have hpβ₀ : y, (α p.1) y = X.x₀ := ¬ p, p a'' = 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(α p.1) y = X.x₀ p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(match p.1 y with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(match X.x₀ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(match X.x₁ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(match X.x₀ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1y:Y'.tA(match X.x₁ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ All goals completed! 🐙 p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y'.tA), (p.2 β) y = X.x₀p, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀p, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 (β Y.y₂) = X.x₀ := hpβ₀ Y.y₂p, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 (β Y.y₂) = X.x₀ := hpβ₀ Y.y₂:β Y.y₂ = Y.y₁ := rflp, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁p, a'' 𝟙 X' p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁¬(p.1 a, p.2 a), = (id, id), p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p.2 (a x) = x := congrFun h₃False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p.2 (a x) = x := congrFun h₃hpa:p.2 (a X.x₁) = X.x₁ := hpa₀ X.x₁False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p.2 (a x) = x := congrFun h₃hpa:p.2 (a X.x₁) = X.x₁ := hpa₀ X.x₁ha:a X.x₁ = Y.y₁ := rflFalse p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p.2 (a x) = x := congrFun h₃hpa:p.2 Y.y₁ = X.x₁ha:a X.x₁ = Y.y₁False p:(Y'.tA X'.tA) × (Y'.tD X'.tD)left✝¹: x Y'.carrierA, p.1 x X'.carrierAleft✝: x Y'.carrierD, p.2 x X'.carrierDhp_comm:p.2 β = α p.1hpβ₀: (y : Y), p.2 (β y) = X.x₀hpβ:p.2 Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:(p.1 a, p.2 a), = (id, id), h₂:(p.1 a, p.2 a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p.2 a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p.2 (a x) = x := congrFun h₃hpa:X.x₀ = X.x₁ha:a X.x₁ = Y.y₁False All goals completed! 🐙

Or, alternatively, using our functor J defined earlier,

example : ¬( p : , J p J a' = J (𝟙 )) := ¬ p, J p J a' = J (𝟙 ) (p : ), J p J a' J (𝟙 ) p: J p J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p .toEnd = .toEnd pJ p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α pJ p, J a' J (𝟙 ) have hpβ₀ : y, (α p) y = X.x₀ := ¬ p, J p J a' = J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(α p) y = X.x₀ p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(match p y with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(match X.x₀ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(match X.x₁ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(match X.x₀ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α py:.t(match X.x₁ with | X.x₀ => X.x₀ | X.x₁ => X.x₀) = X.x₀ All goals completed! 🐙 p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : .t), (p β) y = X.x₀J p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀J p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p (β Y.y₂) = X.x₀ := hpβ₀ Y.y₂J p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p (β Y.y₂) = X.x₀ := hpβ₀ Y.y₂:β Y.y₂ = Y.y₁ := rflJ p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁J p, J a' J (𝟙 ) p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁¬((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p (a x) = x := congrFun h₃False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p (a x) = x := congrFun h₃hpa:p (a X.x₁) = X.x₁ := hpa₀ X.x₁False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p (a x) = x := congrFun h₃hpa:p (a X.x₁) = X.x₁ := hpa₀ X.x₁ha:a X.x₁ = Y.y₁ := rflFalse p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p (a x) = x := congrFun h₃hpa:p Y.y₁ = X.x₁ha:a X.x₁ = Y.y₁False p:.t .tleft✝: x .carrier, p x .carrierhp_comm:p β = α phpβ₀: (y : Y), p (β y) = X.x₀hpβ:p Y.y₁ = X.x₀:β Y.y₂ = Y.y₁h₁:((ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1), (ConcreteCategory.hom p, ) (ConcreteCategory.hom a, a'._proof_1)), = ((ConcreteCategory.hom (SetWithEndomapHom.id )), (ConcreteCategory.hom (SetWithEndomapHom.id ))), h₂:(p a, p a) = (𝟙 X, 𝟙 X) := congrArg Subtype.val h₁h₃:p a = 𝟙 X := congrArg Prod.snd h₂hpa₀: (x : X), p (a x) = x := congrFun h₃hpa:X.x₀ = X.x₁ha:a X.x₁ = Y.y₁False All goals completed! 🐙
Exercise 25 (p. 148)

Show that for any two graphs and any 𝑺⇊-map between them X \xrightarrow{f_A} Y,\; P \xrightarrow{f_D} Q,\; X \xrightarrow{s} P,\; X \xrightarrow{t} P,\; Y \xrightarrow{s'} Q,\; Y \xrightarrow{t'} Q the equation {f_D \circ s = f_D \circ t} can only be true when f_A maps every arrow in X to a loop (relative to s', t') in Y.

Solution: Exercise 25

We first give a proof without using Category IrreflexiveGraph that we defined previously.

example {X P Y Q : Type} (s t : X P) (s' t' : Y Q) (fA : X Y) (fD : P Q) (hfSrc_comm : fD s = s' fA) (hfTgt_comm : fD t = t' fA) : fD s = fD t x, s' (fA x) = t' (fA x) := X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAfD s = fD t (x : X), s' (fA x) = t' (fA x) X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAfD s = fD t (x : X), s' (fA x) = t' (fA x)X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fA(∀ (x : X), s' (fA x) = t' (fA x)) fD s = fD t X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAfD s = fD t (x : X), s' (fA x) = t' (fA x) intro h X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh:fD s = fD tx:Xs' (fA x) = t' (fA x) X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh:fD s = fD tx:X(s' fA) x = (t' fA) x X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh:fD s = fD tx:X(fD s) x = (fD t) x All goals completed! 🐙 X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fA(∀ (x : X), s' (fA x) = t' (fA x)) fD s = fD t X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh: (x : X), s' (fA x) = t' (fA x)fD s = fD t X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh: (x : X), s' (fA x) = t' (fA x)s' fA = t' fA X:TypeP:TypeY:TypeQ:Types:X Pt:X Ps':Y Qt':Y QfA:X YfD:P QhfSrc_comm:fD s = s' fAhfTgt_comm:fD t = t' fAh: (x : X), s' (fA x) = t' (fA x)x:X(s' fA) x = (t' fA) x All goals completed! 🐙

Using Category IrreflexiveGraph, we have

variable (XP YQ : IrreflexiveGraph) (f : XP YQ) -- Align to the notation in the book set_option quotPrecheck false local notation "fA" => f.val.1 local notation "fD" => f.val.2 set_option quotPrecheck true local notation "s" => XP.toSrc local notation "s'" => YQ.toSrc local notation "t" => XP.toTgt local notation "t'" => YQ.toTgt example : (fD s = fD t) ( x, s' (fA x) = t' (fA x)) := XP:IrreflexiveGraphYQ:IrreflexiveGraphf:XP YQ(↑f).2 XP.toSrc = (↑f).2 XP.toTgt (x : XP.tA), YQ.toSrc ((↑f).1 x) = YQ.toTgt ((↑f).1 x) XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1(↑f, ).2 XP.toSrc = (↑f, ).2 XP.toTgt (x : XP.tA), YQ.toSrc ((↑f, ).1 x) = YQ.toTgt ((↑f, ).1 x) XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1f.2 XP.toSrc = f.2 XP.toTgt (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x) XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1f.2 XP.toSrc = f.2 XP.toTgt (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1(∀ (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)) f.2 XP.toSrc = f.2 XP.toTgt XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1f.2 XP.toSrc = f.2 XP.toTgt (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x) intro h XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h:f.2 XP.toSrc = f.2 XP.toTgtx:XP.tAYQ.toSrc (f.1 x) = YQ.toTgt (f.1 x) XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h:f.2 XP.toSrc = f.2 XP.toTgtx:XP.tA(YQ.toSrc f.1) x = (YQ.toTgt f.1) x XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h:f.2 XP.toSrc = f.2 XP.toTgtx:XP.tA(f.2 XP.toSrc) x = (f.2 XP.toTgt) x All goals completed! 🐙 XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1(∀ (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)) f.2 XP.toSrc = f.2 XP.toTgt XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h: (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)f.2 XP.toSrc = f.2 XP.toTgt XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h: (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)YQ.toSrc f.1 = YQ.toTgt f.1 XP:IrreflexiveGraphYQ:IrreflexiveGraphf:(XP.tA YQ.tA) × (XP.tD YQ.tD)left✝¹: x XP.carrierA, f.1 x YQ.carrierAleft✝: x XP.carrierD, f.2 x YQ.carrierDhfSrc_comm:f.2 XP.toSrc = YQ.toSrc f.1hfTgt_comm:f.2 XP.toTgt = YQ.toTgt f.1h: (x : XP.tA), YQ.toSrc (f.1 x) = YQ.toTgt (f.1 x)x:XP.tA(YQ.toSrc f.1) x = (YQ.toTgt f.1) x All goals completed! 🐙
Exercise 26 (p. 148)

There is an 'inclusion' map {\mathbb{Z} \xrightarrow{f} \mathbb{Q}} in 𝑺 for which

  1. {\mathbb{Z}^{↻5\times()} \xrightarrow{f} \mathbb{Q}^{↻5\times()}} is a map in 𝑺↻, and

  2. \mathbb{Q}^{↻5\times()} is an automorphism, and

  3. f is injective.

Find the f and prove the three statements.

Solution: Exercise 26

Rule is {f(x) = x / 1}.

def f : := fun x (x : )

1. We show that {\mathbb{Z}^{↻5\times()} \xrightarrow{f} \mathbb{Q}^{↻5\times()}} is a map in 𝑺↻.

def Z : SetWithEndomap := { t := carrier := Set.univ toEnd := fun x 5 * x toEnd_mem := fun _ Set.mem_univ _ } def Q : SetWithEndomap := { t := carrier := Set.univ toEnd := fun x 5 * x toEnd_mem := fun _ Set.mem_univ _ } example : Z Q := f, (∀ x Z.carrier, f x Q.carrier) f Z.toEnd = Q.toEnd f x Z.carrier, f x Q.carrierf Z.toEnd = Q.toEnd f x Z.carrier, f x Q.carrier All goals completed! 🐙 f Z.toEnd = Q.toEnd f x:(f Z.toEnd) x = (Q.toEnd f) x x:(5 * x) = 5 * x All goals completed! 🐙

2. We show that \mathbb{Q}^{↻5\times()} is an automorphism.

example : SetWithInvEndomap := { t := Q.t carrier := Q.carrier toEnd := Q.toEnd toEnd_mem := fun _ Set.mem_univ _ inv := inv, inv Q.toEnd = 𝟙 Q.t Q.toEnd inv = 𝟙 Q.t finv: := fun x x / 5 inv, inv Q.toEnd = 𝟙 Q.t Q.toEnd inv = 𝟙 Q.t finv: := fun x x / 5finv Q.toEnd = 𝟙 Q.t Q.toEnd finv = 𝟙 Q.t finv: := fun x x / 5finv Q.toEnd = 𝟙 Q.tfinv: := fun x x / 5Q.toEnd finv = 𝟙 Q.t finv: := fun x x / 5finv Q.toEnd = 𝟙 Q.tfinv: := fun x x / 5Q.toEnd finv = 𝟙 Q.t (finv: := fun x x / 5x:Q.t(Q.toEnd finv) x = 𝟙 Q.t x; finv: := fun x x / 5x:Q.t5 * (x / 5) = x; All goals completed! 🐙) }

3. We show that f is injective.

example : {T : Type} (x₁ x₂ : T ), f x₁ = f x₂ x₁ = x₂ := {T : Type} (x₁ x₂ : T ), f x₁ = f x₂ x₁ = x₂ p: := fun y y.num {T : Type} (x₁ x₂ : T ), f x₁ = f x₂ x₁ = x₂ have h₁ : p f = 𝟙 := {T : Type} (x₁ x₂ : T ), f x₁ = f x₂ x₁ = x₂ p: := fun y y.num(fun y y.num) f = 𝟙 p: := fun y y.numx:((fun y y.num) f) x = 𝟙 x All goals completed! 🐙 intro _ p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ (x₂ : T✝ ), f x₁ = f x₂ x₁ = x₂ p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ f x₁ = f x₂ x₁ = x₂ p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂x₁ = x₂ calc x₁ _ = 𝟙 x₁ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂x₁ = 𝟙 x₁ All goals completed! 🐙 _ = (p f) x₁ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂𝟙 x₁ = (p f) x₁ All goals completed! 🐙 _ = p f x₁ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂(p f) x₁ = p f x₁ All goals completed! 🐙 _ = p f x₂ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂p f x₁ = p f x₂ All goals completed! 🐙 _ = (p f) x₂ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂p f x₂ = (p f) x₂ All goals completed! 🐙 _ = 𝟙 x₂ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂(p f) x₂ = 𝟙 x₂ All goals completed! 🐙 _ = x₂ := p: := fun y y.numh₁:p f = 𝟙 := id (funext fun x Eq.refl (((fun y y.num) f) x))T✝:Typex₁:T✝ x₂:T✝ h₂:f x₁ = f x₂𝟙 x₂ = x₂ All goals completed! 🐙
Exercise 27 (p. 148)

Consider our standard idempotent

inductive X | x₀ | x₁ def α : X X | X.x₀ => X.x₀ | X.x₁ => X.x₀ def : SetWithIdemEndomap := { t := X carrier := Set.univ toEnd := α toEnd_mem := fun _ Set.mem_univ _ idem := α α = α x:X(α α) x = α x (α α) X.x₀ = α X.x₀(α α) X.x₁ = α X.x₁ (α α) X.x₀ = α X.x₀(α α) X.x₁ = α X.x₁ All goals completed! 🐙 }

and let Y^{↻\beta} be any automorphism. Show that any 𝑺↻-map {X^{↻\alpha} \xrightarrow{f} Y^{↻\beta}} must be non-injective, i.e. must map both elements of X to the same (fixed) point of \beta in Y.

Solution: Exercise 27

We show that any 𝑺↻-map {X^{↻\alpha} \xrightarrow{f} Y^{↻\beta}} must be non-injective.

example ( : SetWithInvEndomap) (f : .toSetWithEndomap .toSetWithEndomap) : f X.x₀ = f X.x₁ := :SetWithInvEndomapf:.toSetWithEndomap .toSetWithEndomap(ConcreteCategory.hom f) X.x₀ = (ConcreteCategory.hom f) X.x₁ :SetWithInvEndomapf:.toSetWithEndomap .toSetWithEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .t(ConcreteCategory.hom f) X.x₀ = (ConcreteCategory.hom f) X.x₁ :SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd f(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ :SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd fhf_comm_x₀:(f .toEnd) X.x₀ = (.toEnd f) X.x₀ := congrFun hf_comm X.x₀(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ :SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd fhf_comm_x₀:(f .toEnd) X.x₀ = (.toEnd f) X.x₀ := congrFun hf_comm X.x₀hf_comm_x₁:(f .toEnd) X.x₁ = (.toEnd f) X.x₁ := congrFun hf_comm X.x₁(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ :SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd fhf_comm_x₀:f X.x₀ = .toEnd (f X.x₀) := congrFun hf_comm X.x₀hf_comm_x₁:f X.x₀ = .toEnd (f X.x₁) := congrFun hf_comm X.x₁(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ have hβfx_eq : .toEnd (f X.x₀) = .toEnd (f X.x₁) := :SetWithInvEndomapf:.toSetWithEndomap .toSetWithEndomap(ConcreteCategory.hom f) X.x₀ = (ConcreteCategory.hom f) X.x₁ All goals completed! 🐙 :SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd fhf_comm_x₀:f X.x₀ = .toEnd (f X.x₀) := congrFun hf_comm X.x₀hf_comm_x₁:f X.x₀ = .toEnd (f X.x₁) := congrFun hf_comm X.x₁hβfx_eq:.toEnd (f X.x₀) = .toEnd (f X.x₁) := Eq.mpr (id (congrArg (fun _a _a = .toEnd (f X.x₁)) (Eq.symm hf_comm_x₀))) (Eq.mpr (id (congrArg (fun _a _a = .toEnd (f X.x₁)) hf_comm_x₁)) (Eq.refl (.toEnd (f X.x₁))))h_cancel:(βinv .toEnd) (f X.x₀) = (βinv .toEnd) (f X.x₁) := congrArg βinv hβfx_eq(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ rwa [hβ_inv:SetWithInvEndomapβinv:.t .thβ_inv:βinv .toEnd = 𝟙 .tright✝:.toEnd βinv = 𝟙 .tf:.t .tleft✝: x .carrier, f x .carrierhf_comm:f .toEnd = .toEnd fhf_comm_x₀:f X.x₀ = .toEnd (f X.x₀) := congrFun hf_comm X.x₀hf_comm_x₁:f X.x₀ = .toEnd (f X.x₁) := congrFun hf_comm X.x₁hβfx_eq:.toEnd (f X.x₀) = .toEnd (f X.x₁) := Eq.mpr (id (congrArg (fun _a _a = .toEnd (f X.x₁)) (Eq.symm hf_comm_x₀))) (Eq.mpr (id (congrArg (fun _a _a = .toEnd (f X.x₁)) hf_comm_x₁)) (Eq.refl (.toEnd (f X.x₁))))h_cancel:𝟙 .t (f X.x₀) = 𝟙 .t (f X.x₁)(ConcreteCategory.hom f, ) X.x₀ = (ConcreteCategory.hom f, ) X.x₁ at h_cancel
Exercise 28 (p. 148)

If X^{↻\alpha} is any object of 𝑺↻ for which there exists an injective 𝑺↻-map f to some Y^{↻\beta} where \beta is in the subcategory of automorphisms, then \alpha itself must be injective.

Solution: Exercise 28

cf. Mono f.val, Mono Xα.toEnd.val.

example ( : SetWithEndomap) ( : SetWithInvEndomap) (f : .toSetWithEndomap) (hf_inj : {U : Type} (y₁ y₂ : U .t), f.val y₁ = f.val y₂ y₁ = y₂) : {T : Type} (x₁ x₂ : T .t), .toEnd x₁ = .toEnd x₂ x₁ = x₂ := :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂ {T : Type} (x₁ x₂ : T .t), .toEnd x₁ = .toEnd x₂ x₁ = x₂ intro _ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .t (x₂ : T✝ .t), .toEnd x₁ = .toEnd x₂ x₁ = x₂ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .t.toEnd x₁ = .toEnd x₂ x₁ = x₂ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂x₁ = x₂ have h₂ : f.val .toEnd x₁ = f.val .toEnd x₂ := :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂ {T : Type} (x₁ x₂ : T .t), .toEnd x₁ = .toEnd x₂ x₁ = x₂ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂.toEnd x₁ = .toEnd x₂ All goals completed! 🐙 repeat :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂h₂:(.toEnd f) x₁ = (.toEnd f) x₂x₁ = x₂ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂h₂:(.toEnd f) x₁ = (.toEnd f) x₂βinv:.t .thβ_inv:βinv .toEnd = 𝟙 .t .toEnd βinv = 𝟙 .tx₁ = x₂ have h₃ : βinv .toEnd f.val x₁ = βinv .toEnd f.val x₂ := :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂ {T : Type} (x₁ x₂ : T .t), .toEnd x₁ = .toEnd x₂ x₁ = x₂ :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂h₂:(.toEnd f) x₁ = (.toEnd f) x₂βinv:.t .thβ_inv:βinv .toEnd = 𝟙 .t .toEnd βinv = 𝟙 .t.toEnd f x₁ = .toEnd f x₂ All goals completed! 🐙 :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂h₂:(.toEnd f) x₁ = (.toEnd f) x₂βinv:.t .thβ_inv:βinv .toEnd = 𝟙 .t .toEnd βinv = 𝟙 .th₃:𝟙 .t f x₁ = 𝟙 .t f x₂x₁ = x₂ repeat :SetWithEndomap:SetWithInvEndomapf: .toSetWithEndomaphf_inj: {U : Type} (y₁ y₂ : U .t), f y₁ = f y₂ y₁ = y₂T✝:Typex₁:T✝ .tx₂:T✝ .th₁:.toEnd x₁ = .toEnd x₂h₂:(.toEnd f) x₁ = (.toEnd f) x₂βinv:.t .thβ_inv:βinv .toEnd = 𝟙 .t .toEnd βinv = 𝟙 .th₃:f x₁ = f x₂x₁ = x₂ All goals completed! 🐙

11. Types of structure

Exercise 29 (p. 150)

Every map {X \xrightarrow{f} Y} in 𝑿 gives rise to a map in the category of 𝑨-structures, by the associative law.

Solution: Exercise 29

TODO Exercise III.29

Exercise 30 (p. 151)

If S, s, t is a given bipointed object ... in a category 𝒞, then for each object X of 𝒞, the graph of 'X fields' on S is actually a reflexive graph, and for each map {X \xrightarrow{f} Y} in 𝒞, the induced maps on sets constitute a map of reflexive graphs.

Solution: Exercise 30

TODO Exercise III.30