Session 12: Categories of diagrams

1. Dynamical systems or automata

Exercise 1 (p. 161)

Suppose that {x' = \alpha^3(x)} and that {X^{↻\alpha} \xrightarrow{f} Y^{↻\beta}} is a map in 𝑺↻. Let {y = f(x)} and {y' = \beta^3(y)}. Prove that {f(x') = y'}.

Solution: Exercise 1

We proceed by repeatedly applying the property {f \circ \alpha = \beta \circ f}.

example {Xα Yβ : SetWithEndomap} (f : Xα ⟶ Yβ)
    {x x' : Xα.t} {y y' : Yβ.t}
    (hx' : x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) x)
    (hy : y = f.val x)
    (hy' : y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y)
    : f.val x' = y' := byXα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y⊢ ↑f x' = y'
  have hf_comm := f.property.2Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = y'
  rw [hy', hy]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (↑f x)
  rw [← types_comp_apply f.val (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd)]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = ((Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) ⊚ ↑f) x
  rw [← Category.assoc, ← Category.assoc]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd ⊚ ↑f) x
  rw [← hf_comm]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ ↑f ⊚ Xα.toEnd) x
  rw [Category.assoc Xα.toEnd]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (Yβ.toEnd ⊚ (Yβ.toEnd ⊚ ↑f) ⊚ Xα.toEnd) x
  rw [← hf_comm]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (Yβ.toEnd ⊚ (↑f ⊚ Xα.toEnd) ⊚ Xα.toEnd) x
  rw [Category.assoc, Category.assoc]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (((Yβ.toEnd ⊚ ↑f) ⊚ Xα.toEnd) ⊚ Xα.toEnd) x
  rw [← hf_comm]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (((↑f ⊚ Xα.toEnd) ⊚ Xα.toEnd) ⊚ Xα.toEnd) x
  rw [← Category.assoc, ← Category.assoc]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = (↑f ⊚ Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) x
  rw [types_comp_apply]Xα:SetWithEndomapYβ:SetWithEndomapf:Xα ⟶ Yβx:Xα.tx':Xα.ty:Yβ.ty':Yβ.thx':x' = (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) xhy:y = ↑f xhy':y' = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) yhf_comm:↑f ⊚ Xα.toEnd = Yβ.toEnd ⊚ ↑f := f.property.right⊢ ↑f x' = ↑f ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) x)
  rw [hx']All goals completed! 🐙

Exercise 2 (p. 162)

'With age comes stability'. In a finite dynamical system, every state eventually settles into a cycle.

...

For two units of time, x is living on the fringes, but after that he settles into an organized periodic behaviour, repeating the same routine every four units of time. What about y and z? Don’t take the title seriously; humans can change the system! This sort of thing applies to light bulbs, though. If a particular light bulb can only be lit four times before burning out, after which pressing the on—off button has no effect, draw the automaton modeling its behavior.

Solution: Exercise 2

The automaton modelling the behaviour of a light bulb that can only be lit four times before burning out may be represented as follows:

inductive BulbState
  | off₀ | on₁ | off₁ | on₂ | off₂ | on₃ | off₃ | on₄ | burntOut
  deriving Fintype, DecidableEq

open BulbState

def pressButton : BulbState ⟶ BulbState
  | off₀ => on₁ -- lit 1st time
  | on₁  => off₁
  | off₁ => on₂ -- lit 2nd time
  | on₂  => off₂
  | off₂ => on₃ -- lit 3rd time
  | on₃  => off₃
  | off₃ => on₄ -- lit 4th time
  | on₄  => burntOut
  | burntOut => burntOut

To verify correct operation, we begin by setting up a simulation of pressing the on-off button eight times, starting from off₀, and counting how many times the bulb lights up.

abbrev LitCount := Nat

def LitStates : List BulbState := [on₁, on₂, on₃, on₄]

def pressAndCount (this : BulbState) : StateM LitCount BulbState := do
  let next := pressButton this
  if next ∈ LitStates then
    modify (· + 1)
  return next

def EightPresses : List Unit := List.replicate 8 ()

def simulateEightPresses : StateM LitCount BulbState :=
  EightPresses.foldlM (fun s _ ↦ pressAndCount s) off₀

Run the simulation starting with a lit count of 0, and return the final bulb state and lit count.

def getResult : BulbState × LitCount := simulateEightPresses.run 0

Confirm that at the end of the run, the bulb has been lit four times and is now burntOut.

example : getResult = (burntOut, 4) := rfl

Lastly, confirm that once the bulb is burntOut, pressing the on—off button has no effect (i.e., burntOut is a fixed point).

example : Function.IsFixedPt pressButton burntOut := rfl

2. Family trees

We implement the category 𝑺↻↻ in which an object is a set with a specified pair of endomaps, as described on p. 162.

structure SetWithTwoEndomaps extends SetWithEndomap where
  toEnd2 : t ⟶ t
  toEnd2_mem {a} : a ∈ carrier → toEnd a ∈ carrier

instance instCatSetWithTwoEndomaps : Category SetWithTwoEndomaps where
  Hom X Y := {
    f : X.t ⟶ Y.t //
        (∀ x ∈ X.carrier, f x ∈ Y.carrier) -- maps to codomain
        ∧ f ⊚ X.toEnd = Y.toEnd ⊚ f -- first endomap commutes
        ∧ f ⊚ X.toEnd2 = Y.toEnd2 ⊚ f -- second endomap commutes
  }
  id X := ⟨
    𝟙 X.t,
    byX:SetWithTwoEndomaps⊢ (∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrier) ∧ 𝟙 X.t ⊚ X.toEnd = X.toEnd ⊚ 𝟙 X.t ∧ 𝟙 X.t ⊚ X.toEnd2 = X.toEnd2 ⊚ 𝟙 X.t
      constructorleftX:SetWithTwoEndomaps⊢ ∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrierrightX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd = X.toEnd ⊚ 𝟙 X.t ∧ 𝟙 X.t ⊚ X.toEnd2 = X.toEnd2 ⊚ 𝟙 X.t
      ·leftX:SetWithTwoEndomaps⊢ ∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrier intro _ hxleftX:SetWithTwoEndomapsx✝:X.thx:x✝ ∈ X.carrier⊢ 𝟙 X.t x✝ ∈ X.carrier
        exact hxAll goals completed! 🐙
      ·rightX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd = X.toEnd ⊚ 𝟙 X.t ∧ 𝟙 X.t ⊚ X.toEnd2 = X.toEnd2 ⊚ 𝟙 X.t constructorright.leftX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd = X.toEnd ⊚ 𝟙 X.tright.rightX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd2 = X.toEnd2 ⊚ 𝟙 X.t <;>right.leftX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd = X.toEnd ⊚ 𝟙 X.tright.rightX:SetWithTwoEndomaps⊢ 𝟙 X.t ⊚ X.toEnd2 = X.toEnd2 ⊚ 𝟙 X.t rflAll goals completed! 🐙
  ⟩
  comp := by⊢ {X Y Z : SetWithTwoEndomaps} →
  { f // (∀ x ∈ X.carrier, f x ∈ Y.carrier) ∧ f ⊚ X.toEnd = Y.toEnd ⊚ f ∧ f ⊚ X.toEnd2 = Y.toEnd2 ⊚ f } →
    { f // (∀ x ∈ Y.carrier, f x ∈ Z.carrier) ∧ f ⊚ Y.toEnd = Z.toEnd ⊚ f ∧ f ⊚ Y.toEnd2 = Z.toEnd2 ⊚ f } →
      { f // (∀ x ∈ X.carrier, f x ∈ Z.carrier) ∧ f ⊚ X.toEnd = Z.toEnd ⊚ f ∧ f ⊚ X.toEnd2 = Z.toEnd2 ⊚ f }
    rintro _ _ _ ⟨f, hf⟩ ⟨g, hg⟩X✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.thf:(∀ x ∈ X✝.carrier, f x ∈ Y✝.carrier) ∧ f ⊚ X✝.toEnd = Y✝.toEnd ⊚ f ∧ f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fg:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ g ∧ g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ { f // (∀ x ∈ X✝.carrier, f x ∈ Z✝.carrier) ∧ f ⊚ X✝.toEnd = Z✝.toEnd ⊚ f ∧ f ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ f }
    exact ⟨
      g ⊚ f,
      byX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.thf:(∀ x ∈ X✝.carrier, f x ∈ Y✝.carrier) ∧ f ⊚ X✝.toEnd = Y✝.toEnd ⊚ f ∧ f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fg:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ g ∧ g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f ∧ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f
        obtain ⟨hf_mtc, hf_comm, hf2_comm⟩ := hfX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ g ∧ g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ ghf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ f⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f ∧ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f
        obtain ⟨hg_mtc, hg_comm, hg2_comm⟩ := hgX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f ∧ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f
        constructorleftX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ ∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrierrightX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f ∧ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f
        ·leftX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ ∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier intro x hxleftX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ gx:X✝.thx:x ∈ X✝.carrier⊢ (g ⊚ f) x ∈ Z✝.carrier
          exact hg_mtc (f x) (hf_mtc x hx)All goals completed! 🐙
        ·rightX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f ∧ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f constructorright.leftX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ fright.rightX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f
          ·right.leftX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd = Z✝.toEnd ⊚ g ⊚ f rw [← Category.assoc, hf_comm, Category.assoc, hg_comm,
              ← Category.assoc]All goals completed! 🐙
          ·right.rightX✝:SetWithTwoEndomapsY✝:SetWithTwoEndomapsZ✝:SetWithTwoEndomapsf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comm:f ⊚ X✝.toEnd = Y✝.toEnd ⊚ fhf2_comm:f ⊚ X✝.toEnd2 = Y✝.toEnd2 ⊚ fhg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comm:g ⊚ Y✝.toEnd = Z✝.toEnd ⊚ ghg2_comm:g ⊚ Y✝.toEnd2 = Z✝.toEnd2 ⊚ g⊢ (g ⊚ f) ⊚ X✝.toEnd2 = Z✝.toEnd2 ⊚ g ⊚ f rw [← Category.assoc, hf2_comm, Category.assoc, hg2_comm,
              ← Category.assoc]All goals completed! 🐙
    ⟩

Exercise 3 (p. 163)

(a) Suppose {\mathbf{P} = {}^{m↻}P^{↻f}} is the set P of all people together with the endomaps {m = \mathit{mother}} and {f = \mathit{father}}. Show that 'gender' is a map in the category 𝑺↻↻ from \mathbf{P} to the object

inductive Gender
  | female | male

def m₁ : Gender ⟶ Gender := fun _ ↦ Gender.female

def f₁ : Gender ⟶ Gender := fun _ ↦ Gender.male

def G : SetWithTwoEndomaps := {
  t := Gender
  carrier := Set.univ
  toEnd := m₁
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := f₁
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

(b) In a certain society, all the people have always been divided into two 'clans', the Wolf-clan and the Bear-clan. Marriages within a clan are forbidden, so that a Wolf may not marry a Wolf. A child's clan is the same as that of its mother. Show that the sorting of people into clans is actually a map in 𝑺↻↻ from \mathbf{P} to the object

inductive Clan
  | wolf | bear

def m₂ : Clan ⟶ Clan := fun c ↦ c

def f₂ : Clan ⟶ Clan
  | Clan.wolf => Clan.bear
  | Clan.bear => Clan.wolf

def C : SetWithTwoEndomaps := {
  t := Clan
  carrier := Set.univ
  toEnd := m₂
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := f₂
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

(c) Find appropriate 'father' and 'mother' maps to make {\mathbf{G} \times \mathbf{C}} into an object in 𝑺↻↻ so that 'clan' and 'gender' can be combined into a single map {\mathbf{P} \rightarrow \mathbf{G} \times \mathbf{C}}. (Later, when we have the precise definition of multiplication of objects in categories, you will see that {\mathbf{G} \times \mathbf{C}} really is the product of \mathbf{G} and \mathbf{C}.)

Solution: Exercise 3

(a) For \mathbf{P} in 𝑺↻↻, we first define a Person type to use in place of the set P of all people, and we identity each Person as being either a mother or a father.

inductive ParentType
  | isMother | isFather

structure Person₁ where
  parentType : ParentType

We next define the mother and father endomaps on Person, which ignore their input (as irrelevant) and simply return a Person of the appropriate ParentType.

def mother₁ : Person₁ ⟶ Person₁ := fun _ ↦ ⟨ParentType.isMother⟩

def father₁ : Person₁ ⟶ Person₁ := fun _ ↦ ⟨ParentType.isFather⟩

Now we can define the object \mathbf{P}.

def P₁ : SetWithTwoEndomaps := {
  t := Person₁
  carrier := Set.univ
  toEnd := mother₁
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := father₁
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

Lastly, we define the map gender, which sends each Person to their corresponding Gender.

def gender : P₁.t ⟶ G.t
  | ⟨ParentType.isMother⟩ => Gender.female
  | ⟨ParentType.isFather⟩ => Gender.male

Since we can form a valid morphism using our categorical framework, it follows that gender is a map in the category 𝑺↻↻ from \mathbf{P} to \mathbf{G}.

def gender' : P₁ ⟶ G := ⟨
  gender,
  by⊢ (∀ x ∈ P₁.carrier, gender x ∈ G.carrier) ∧ gender ⊚ P₁.toEnd = G.toEnd ⊚ gender ∧ gender ⊚ P₁.toEnd2 = G.toEnd2 ⊚ gender
    constructorleft⊢ ∀ x ∈ P₁.carrier, gender x ∈ G.carrierright⊢ gender ⊚ P₁.toEnd = G.toEnd ⊚ gender ∧ gender ⊚ P₁.toEnd2 = G.toEnd2 ⊚ gender
    ·left⊢ ∀ x ∈ P₁.carrier, gender x ∈ G.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ gender ⊚ P₁.toEnd = G.toEnd ⊚ gender ∧ gender ⊚ P₁.toEnd2 = G.toEnd2 ⊚ gender constructorright.left⊢ gender ⊚ P₁.toEnd = G.toEnd ⊚ genderright.right⊢ gender ⊚ P₁.toEnd2 = G.toEnd2 ⊚ gender <;>right.left⊢ gender ⊚ P₁.toEnd = G.toEnd ⊚ genderright.right⊢ gender ⊚ P₁.toEnd2 = G.toEnd2 ⊚ gender rflAll goals completed! 🐙
⟩

For good measure, we can also verify the two commutative properties explicitly.

example : gender ⊚ mother₁ = m₁ ⊚ gender := rfl

example : gender ⊚ father₁ = f₁ ⊚ gender := rfl

(b) The implementation of part (b) is similar to that of part (a), with an appropriate change to our Person structure to handle clan.

inductive ParentClan
  | isWolf | isBear

structure Person₂ where
  parentClan : ParentClan

def mother₂ : Person₂ ⟶ Person₂ := fun p ↦ ⟨p.parentClan⟩

def father₂ : Person₂ ⟶ Person₂
  | ⟨ParentClan.isWolf⟩ => ⟨ParentClan.isBear⟩
  | ⟨ParentClan.isBear⟩ => ⟨ParentClan.isWolf⟩

def P₂ : SetWithTwoEndomaps := {
  t := Person₂
  carrier := Set.univ
  toEnd := mother₂
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := father₂
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

def clan : P₂.t ⟶ C.t
  | ⟨ParentClan.isWolf⟩ => Clan.wolf
  | ⟨ParentClan.isBear⟩ => Clan.bear

def clan' : P₂ ⟶ C := ⟨
  clan,
  by⊢ (∀ x ∈ P₂.carrier, clan x ∈ C.carrier) ∧ clan ⊚ P₂.toEnd = C.toEnd ⊚ clan ∧ clan ⊚ P₂.toEnd2 = C.toEnd2 ⊚ clan
    constructorleft⊢ ∀ x ∈ P₂.carrier, clan x ∈ C.carrierright⊢ clan ⊚ P₂.toEnd = C.toEnd ⊚ clan ∧ clan ⊚ P₂.toEnd2 = C.toEnd2 ⊚ clan
    ·left⊢ ∀ x ∈ P₂.carrier, clan x ∈ C.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ clan ⊚ P₂.toEnd = C.toEnd ⊚ clan ∧ clan ⊚ P₂.toEnd2 = C.toEnd2 ⊚ clan constructorright.left⊢ clan ⊚ P₂.toEnd = C.toEnd ⊚ clanright.right⊢ clan ⊚ P₂.toEnd2 = C.toEnd2 ⊚ clan
      all_goals
        funext pright.right.hp:P₂.t⊢ (clan ⊚ P₂.toEnd2) p = (C.toEnd2 ⊚ clan) p
        match p with
        | ⟨ParentClan.isWolf⟩ =>p:P₂.t⊢ (clan ⊚ P₂.toEnd2) { parentClan := ParentClan.isWolf } = (C.toEnd2 ⊚ clan) { parentClan := ParentClan.isWolf }p:P₂.t⊢ (clan ⊚ P₂.toEnd) { parentClan := ParentClan.isWolf } = (C.toEnd ⊚ clan) { parentClan := ParentClan.isWolf } rflAll goals completed! 🐙
        | ⟨ParentClan.isBear⟩ =>p:P₂.t⊢ (clan ⊚ P₂.toEnd2) { parentClan := ParentClan.isBear } = (C.toEnd2 ⊚ clan) { parentClan := ParentClan.isBear }p:P₂.t⊢ (clan ⊚ P₂.toEnd) { parentClan := ParentClan.isBear } = (C.toEnd ⊚ clan) { parentClan := ParentClan.isBear } rflAll goals completed! 🐙
⟩

structure Person₃ where
  parentType : ParentType
  parentClan : ParentClan

def mother₃ : Person₃ ⟶ Person₃ :=
  fun p ↦ ⟨ParentType.isMother, p.parentClan⟩

def father₃ : Person₃ ⟶ Person₃
  | ⟨_, ParentClan.isWolf⟩ => ⟨ParentType.isFather, ParentClan.isBear⟩
  | ⟨_, ParentClan.isBear⟩ => ⟨ParentType.isFather, ParentClan.isWolf⟩

def P₃ : SetWithTwoEndomaps := {
  t := Person₃
  carrier := Set.univ
  toEnd := mother₃
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := father₃
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

As required, we define appropriate 'mother' and 'father' maps (m and f, respectively, to align with the book).

def m₃ : (Gender × Clan) ⟶ (Gender × Clan) :=
  fun (_, c) ↦ (Gender.female, c)

def f₃ : (Gender × Clan) ⟶ (Gender × Clan)
  | (_, Clan.wolf) => (Gender.male, Clan.bear)
  | (_, Clan.bear) => (Gender.male, Clan.wolf)

def GC : SetWithTwoEndomaps := {
  t := Gender × Clan
  carrier := Set.univ
  toEnd := m₃
  toEnd_mem := fun _ ↦ Set.mem_univ _
  toEnd2 := f₃
  toEnd2_mem := fun _ ↦ Set.mem_univ _
}

def gender_and_clan : P₃.t ⟶ GC.t
  | ⟨ParentType.isMother, ParentClan.isWolf⟩ =>
        ⟨Gender.female, Clan.wolf⟩
  | ⟨ParentType.isMother, ParentClan.isBear⟩ =>
        ⟨Gender.female, Clan.bear⟩
  | ⟨ParentType.isFather, ParentClan.isWolf⟩ =>
        ⟨Gender.male, Clan.wolf⟩
  | ⟨ParentType.isFather, ParentClan.isBear⟩ =>
        ⟨Gender.male, Clan.bear⟩

def gender_and_clan' : P₃ ⟶ GC := ⟨
  gender_and_clan,
  by⊢ (∀ x ∈ P₃.carrier, gender_and_clan x ∈ GC.carrier) ∧
  gender_and_clan ⊚ P₃.toEnd = GC.toEnd ⊚ gender_and_clan ∧ gender_and_clan ⊚ P₃.toEnd2 = GC.toEnd2 ⊚ gender_and_clan
    constructorleft⊢ ∀ x ∈ P₃.carrier, gender_and_clan x ∈ GC.carrierright⊢ gender_and_clan ⊚ P₃.toEnd = GC.toEnd ⊚ gender_and_clan ∧ gender_and_clan ⊚ P₃.toEnd2 = GC.toEnd2 ⊚ gender_and_clan
    ·left⊢ ∀ x ∈ P₃.carrier, gender_and_clan x ∈ GC.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ gender_and_clan ⊚ P₃.toEnd = GC.toEnd ⊚ gender_and_clan ∧ gender_and_clan ⊚ P₃.toEnd2 = GC.toEnd2 ⊚ gender_and_clan constructorright.left⊢ gender_and_clan ⊚ P₃.toEnd = GC.toEnd ⊚ gender_and_clanright.right⊢ gender_and_clan ⊚ P₃.toEnd2 = GC.toEnd2 ⊚ gender_and_clan
      all_goals
        funext pright.right.hp:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd2) p = (GC.toEnd2 ⊚ gender_and_clan) p
        match p with
        | ⟨ParentType.isMother, ParentClan.isWolf⟩ =>p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd2) { parentType := ParentType.isMother, parentClan := ParentClan.isWolf } =
  (GC.toEnd2 ⊚ gender_and_clan) { parentType := ParentType.isMother, parentClan := ParentClan.isWolf }p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd) { parentType := ParentType.isMother, parentClan := ParentClan.isWolf } =
  (GC.toEnd ⊚ gender_and_clan) { parentType := ParentType.isMother, parentClan := ParentClan.isWolf } rflAll goals completed! 🐙
        | ⟨ParentType.isMother, ParentClan.isBear⟩ =>p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd2) { parentType := ParentType.isMother, parentClan := ParentClan.isBear } =
  (GC.toEnd2 ⊚ gender_and_clan) { parentType := ParentType.isMother, parentClan := ParentClan.isBear }p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd) { parentType := ParentType.isMother, parentClan := ParentClan.isBear } =
  (GC.toEnd ⊚ gender_and_clan) { parentType := ParentType.isMother, parentClan := ParentClan.isBear } rflAll goals completed! 🐙
        | ⟨ParentType.isFather, ParentClan.isWolf⟩ =>p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd2) { parentType := ParentType.isFather, parentClan := ParentClan.isWolf } =
  (GC.toEnd2 ⊚ gender_and_clan) { parentType := ParentType.isFather, parentClan := ParentClan.isWolf }p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd) { parentType := ParentType.isFather, parentClan := ParentClan.isWolf } =
  (GC.toEnd ⊚ gender_and_clan) { parentType := ParentType.isFather, parentClan := ParentClan.isWolf } rflAll goals completed! 🐙
        | ⟨ParentType.isFather, ParentClan.isBear⟩ =>p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd2) { parentType := ParentType.isFather, parentClan := ParentClan.isBear } =
  (GC.toEnd2 ⊚ gender_and_clan) { parentType := ParentType.isFather, parentClan := ParentClan.isBear }p:P₃.t⊢ (gender_and_clan ⊚ P₃.toEnd) { parentType := ParentType.isFather, parentClan := ParentClan.isBear } =
  (GC.toEnd ⊚ gender_and_clan) { parentType := ParentType.isFather, parentClan := ParentClan.isBear } rflAll goals completed! 🐙
⟩