Session 5: Division of maps: Sections and retractions🔗

1. Determination problems🔗

Exercise 1 (p. 70)

(a) Show that if there is a map g for which {h = g \circ f}, then for any pair a_1, a_2 of points {\mathbf{1} \rightarrow A} of the domain A of f (and of h) we have: \text{if}\; fa_1 = fa_2 \;\text{then}\; ha_1 = ha_2. (So, if for some pair of points one has {f a_1 = f a_2} but {h a_1 \ne h a_2}, then h is not determined by f.)

(b) Does the converse hold? That is, if maps (of sets) f and h satisfy the conditions above ('for any pair ... then {h a_1 = h a_2}'), must there be a map {B \xrightarrow{g} C} with {h = g \circ f}?

Solution: Exercise 1

We use types instead of sets here, and we begin by showing that part (a) holds.

example {A B C : Type} {f : A ⟶ B} {h : A ⟶ C}
    (hg : ∃ g : B ⟶ C, h = g ⊚ f)
    : ∀ a₁ a₂ : Point A, f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂ := byA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Chg:∃ g, h = g ⊚ f⊢ ∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂
  obtain ⟨g, hg⟩ := hgA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Cg:B ⟶ Chg:h = g ⊚ f⊢ ∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂
  intro _ _A:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Cg:B ⟶ Chg:h = g ⊚ fa₁✝:Point Aa₂✝:Point A⊢ f ⊚ a₁✝ = f ⊚ a₂✝ → h ⊚ a₁✝ = h ⊚ a₂✝ hfaA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Cg:B ⟶ Chg:h = g ⊚ fa₁✝:Point Aa₂✝:Point Ahfa:f ⊚ a₁✝ = f ⊚ a₂✝⊢ h ⊚ a₁✝ = h ⊚ a₂✝
  rw [hg]A:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Cg:B ⟶ Chg:h = g ⊚ fa₁✝:Point Aa₂✝:Point Ahfa:f ⊚ a₁✝ = f ⊚ a₂✝⊢ (g ⊚ f) ⊚ a₁✝ = (g ⊚ f) ⊚ a₂✝
  repeat rw [← Category.assoc]A:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ Cg:B ⟶ Chg:h = g ⊚ fa₁✝:Point Aa₂✝:Point Ahfa:f ⊚ a₁✝ = f ⊚ a₂✝⊢ g ⊚ f ⊚ a₁✝ = g ⊚ f ⊚ a₂✝
  rw [hfa]All goals completed! 🐙

For part (b), we first prove the converse in the case when f is surjective.

example {A B C : Type} {f : A ⟶ B} {h : A ⟶ C}
    (H : ∀ a₁ a₂ : Point A, f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂)
    (hfsurj : Function.Surjective f)
    : ∃ g : B ⟶ C, h = g ⊚ f := byA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective f⊢ ∃ g, h = g ⊚ f
  let g : B ⟶ C := fun β ↦ h (Classical.choose (hfsurj β))A:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)⊢ ∃ g, h = g ⊚ f
  use ghA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)⊢ h = g ⊚ f
  funext αh.hA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)α:A⊢ h α = (g ⊚ f) α
  let a₁ : Point A := fun _ ↦ αh.hA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)α:Aa₁:Point A := fun x ↦ α⊢ h α = (g ⊚ f) α
  let a₂ : Point A := fun _ ↦ Classical.choose (hfsurj (f α))h.hA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)α:Aa₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ Classical.choose ⋯⊢ h α = (g ⊚ f) α
  have hfa : f ⊚ a₁ = f ⊚ a₂ := byA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective f⊢ ∃ g, h = g ⊚ f
    funexthA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)α:Aa₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ Classical.choose ⋯x✝:One⊢ (f ⊚ a₁) x✝ = (f ⊚ a₂) x✝
    exact (Classical.choose_spec (hfsurj (f α))).symmAll goals completed! 🐙
  have hha : h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah.hA:TypeB:TypeC:Typef:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂hfsurj:Function.Surjective fg:B ⟶ C := fun β ↦ h (Classical.choose ⋯)α:Aa₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ Classical.choose ⋯hfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (Classical.choose_spec (hfsurj (f α)))hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfa⊢ h α = (g ⊚ f) α
  apply congrFun hha ()All goals completed! 🐙

Proof in the general case is slightly more complicated and is given below.

open Classical in
example {A B C : Type} [Nonempty C] {f : A ⟶ B} {h : A ⟶ C}
    (H : ∀ a₁ a₂ : Point A, f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂)
    : ∃ g : B ⟶ C, h = g ⊚ f := byA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂⊢ ∃ g, h = g ⊚ f
  -- β : B may or may not be in the image of f,
  -- so we need to handle both cases
  let g : B ⟶ C := fun β ↦
    if β_in_image : ∃ α : A, f α = β then
      h (choose β_in_image)
    else
      choice inferInstanceA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯⊢ ∃ g, h = g ⊚ f
  use ghA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯⊢ h = g ⊚ f
  funext αh.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:A⊢ h α = (g ⊚ f) α
  let β_in_image_exists : ∃ α' : A, f α' = f α := ⟨α, rfl⟩h.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfl⊢ h α = (g ⊚ f) α
  let a₁ : Point A := fun _ ↦ αh.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ α⊢ h α = (g ⊚ f) α
  let a₂ : Point A := fun _ ↦ choose β_in_image_existsh.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_exists⊢ h α = (g ⊚ f) α
  have hfa : f ⊚ a₁ = f ⊚ a₂ := byA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂⊢ ∃ g, h = g ⊚ f
    funexthA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existsx✝:One⊢ (f ⊚ a₁) x✝ = (f ⊚ a₂) x✝
    exact (choose_spec β_in_image_exists).symmAll goals completed! 🐙
  have hha : h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existshfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (choose_spec β_in_image_exists)hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfa⊢ h α = (g ⊚ f) α
  have h_eq_h_chosen : h α = h (choose β_in_image_exists) :=
    congrFun hha ()h.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existshfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (choose_spec β_in_image_exists)hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah_eq_h_chosen:h α = h (choose β_in_image_exists) := congrFun hha ()⊢ h α = (g ⊚ f) α
  have g_eq_h_chosen : g (f α) = h (choose β_in_image_exists) := byA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂⊢ ∃ g, h = g ⊚ f
    dsimp [g]A:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existshfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (choose_spec β_in_image_exists)hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah_eq_h_chosen:h α = h (choose β_in_image_exists) := congrFun hha ()⊢ (if β_in_image : ∃ α_1, f α_1 = f α then h (choose β_in_image) else choice ⋯) = h (choose β_in_image_exists)
    rw [dif_pos β_in_image_exists]All goals completed! 🐙
  rw [types_comp_apply]h.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existshfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (choose_spec β_in_image_exists)hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah_eq_h_chosen:h α = h (choose β_in_image_exists) := congrFun hha ()g_eq_h_chosen:g (f α) = h (choose β_in_image_exists) := 
  id
    (Eq.mpr (id (congrArg (fun _a ↦ _a = h (choose β_in_image_exists)) (dif_pos β_in_image_exists)))
      (Eq.refl (h (choose β_in_image_exists))))⊢ h α = g (f α)
  rw [g_eq_h_chosen]h.hA:TypeB:TypeC:Typeinst✝:Nonempty Cf:A ⟶ Bh:A ⟶ CH:∀ (a₁ a₂ : Point A), f ⊚ a₁ = f ⊚ a₂ → h ⊚ a₁ = h ⊚ a₂g:B ⟶ C := fun β ↦ if β_in_image : ∃ α, f α = β then h (choose β_in_image) else choice ⋯α:Aβ_in_image_exists:∃ α', f α' = f α := Exists.intro α rfla₁:Point A := fun x ↦ αa₂:Point A := fun x ↦ choose β_in_image_existshfa:f ⊚ a₁ = f ⊚ a₂ := funext fun x ↦ Eq.symm (choose_spec β_in_image_exists)hha:h ⊚ a₁ = h ⊚ a₂ := H a₁ a₂ hfah_eq_h_chosen:h α = h (choose β_in_image_exists) := congrFun hha ()g_eq_h_chosen:g (f α) = h (choose β_in_image_exists) := 
  id
    (Eq.mpr (id (congrArg (fun _a ↦ _a = h (choose β_in_image_exists)) (dif_pos β_in_image_exists)))
      (Eq.refl (h (choose β_in_image_exists))))⊢ h α = h (choose β_in_image_exists)
  exact h_eq_h_chosenAll goals completed! 🐙

2. A special case: Constant maps🔗

Definition: Constant map (p. 71)

A map that can be factored through \mathbf{1} is called a constant map.

We implement IsConstantMap in Lean as follows:

def IsConstantMap {A C : Type} (h : A ⟶ C) :=
  ∃ (f : A ⟶ One) (g : One ⟶ C), h = g ⊚ f

3. Choice problems🔗

Exercise 2 (p. 71)

(a) Show that if there is an f with {g \circ f = h}, then h and g satisfy: For any a in A there is at least one b in B for which {h(a) = g(b)}.

(b) Does the converse hold? That is, if h and g satisfy the condition above, must there be a map f with {h = g \circ f}?

Solution: Exercise 2

We show that part (a) holds.

example {A B C : Type} {g : B ⟶ C} {h : A ⟶ C}
    (hf : ∃ f : A ⟶ B, g ⊚ f = h)
    : ∀ a : A, ∃ b : B, h a = g b := byA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Chf:∃ f, g ⊚ f = h⊢ ∀ (a : A), ∃ b, h a = g b
  intro aA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Chf:∃ f, g ⊚ f = ha:A⊢ ∃ b, h a = g b
  obtain ⟨f, hf⟩ := hfA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Ca:Af:A ⟶ Bhf:g ⊚ f = h⊢ ∃ b, h a = g b
  use f ahA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Ca:Af:A ⟶ Bhf:g ⊚ f = h⊢ h a = g (f a)
  rw [← hf]hA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Ca:Af:A ⟶ Bhf:g ⊚ f = h⊢ (g ⊚ f) a = g (f a)
  rflAll goals completed! 🐙

We show that the converse holds in part (b).

example {A B C : Type} {g : B ⟶ C} {h : A ⟶ C}
    (H : ∀ a : A, ∃ b : B, h a = g b)
    : ∃ f : A ⟶ B, g ⊚ f = h := byA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ CH:∀ (a : A), ∃ b, h a = g b⊢ ∃ f, g ⊚ f = h
  choose f_fun h_spec using HA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Cf_fun:A → Bh_spec:∀ (a : A), h a = g (f_fun a)⊢ ∃ f, g ⊚ f = h
  use f_funhA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Cf_fun:A → Bh_spec:∀ (a : A), h a = g (f_fun a)⊢ g ⊚ f_fun = h
  funext ah.hA:TypeB:TypeC:Typeg:B ⟶ Ch:A ⟶ Cf_fun:A → Bh_spec:∀ (a : A), h a = g (f_fun a)a:A⊢ (g ⊚ f_fun) a = h a
  exact (h_spec a).symmAll goals completed! 🐙

4. Two special cases of division: Sections and retractions🔗

Definition: Section (p. 72)

{A \xrightarrow{f} B} is a section of {B \xrightarrow{g} A} if {g \circ f = 1_A}.

See the original presentation of this definition of section in Article II.

5. Stacking or sorting🔗

Exercise 3 (p. 75)

Draw the internal diagrams of all the sections of f.

Solution: Exercise 3

We label the elements in the first column of A as a_{11}, a_{12}, a_{13}, a_{14} and the elements in the second column of A as a_{21}, a_{22}; we label the element in the first column of B as b_1 and the element in the second column of B as b_2.

inductive A
  | a₁₁ | a₁₂ | a₁₃ | a₁₄ | a₂₁ | a₂₂
  deriving Fintype

inductive B
  | b₁ | b₂
  deriving Fintype

def f : A ⟶ B
  | A.a₁₁ => B.b₁
  | A.a₁₂ => B.b₁
  | A.a₁₃ => B.b₁
  | A.a₁₄ => B.b₁
  | A.a₂₁ => B.b₂
  | A.a₂₂ => B.b₂

Then the sections are

def s₁ : B ⟶ A
  | B.b₁ => A.a₁₁
  | B.b₂ => A.a₂₁

example : f ⊚ s₁ = 𝟙 B := by⊢ f ⊚ s₁ = 𝟙 B funext xhx:B⊢ (f ⊚ s₁) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₁) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₁) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₁) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₁) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₂ : B ⟶ A
  | B.b₁ => A.a₁₂
  | B.b₂ => A.a₂₁

example : f ⊚ s₂ = 𝟙 B := by⊢ f ⊚ s₂ = 𝟙 B funext xhx:B⊢ (f ⊚ s₂) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₂) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₂) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₂) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₂) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₃ : B ⟶ A
  | B.b₁ => A.a₁₃
  | B.b₂ => A.a₂₁

example : f ⊚ s₃ = 𝟙 B := by⊢ f ⊚ s₃ = 𝟙 B funext xhx:B⊢ (f ⊚ s₃) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₃) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₃) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₃) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₃) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₄ : B ⟶ A
  | B.b₁ => A.a₁₄
  | B.b₂ => A.a₂₁

example : f ⊚ s₄ = 𝟙 B := by⊢ f ⊚ s₄ = 𝟙 B funext xhx:B⊢ (f ⊚ s₄) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₄) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₄) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₄) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₄) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₅ : B ⟶ A
  | B.b₁ => A.a₁₁
  | B.b₂ => A.a₂₂

example : f ⊚ s₅ = 𝟙 B := by⊢ f ⊚ s₅ = 𝟙 B funext xhx:B⊢ (f ⊚ s₅) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₅) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₅) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₅) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₅) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₆ : B ⟶ A
  | B.b₁ => A.a₁₂
  | B.b₂ => A.a₂₂

example : f ⊚ s₆ = 𝟙 B := by⊢ f ⊚ s₆ = 𝟙 B funext xhx:B⊢ (f ⊚ s₆) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₆) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₆) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₆) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₆) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₇ : B ⟶ A
  | B.b₁ => A.a₁₃
  | B.b₂ => A.a₂₂

example : f ⊚ s₇ = 𝟙 B := by⊢ f ⊚ s₇ = 𝟙 B funext xhx:B⊢ (f ⊚ s₇) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₇) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₇) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₇) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₇) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙

def s₈ : B ⟶ A
  | B.b₁ => A.a₁₄
  | B.b₂ => A.a₂₂

example : f ⊚ s₈ = 𝟙 B := by⊢ f ⊚ s₈ = 𝟙 B funext xhx:B⊢ (f ⊚ s₈) x = 𝟙 B x; fin_cases xh.«0»⊢ (f ⊚ s₈) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₈) B.b₂ = 𝟙 B B.b₂ <;>h.«0»⊢ (f ⊚ s₈) B.b₁ = 𝟙 B B.b₁h.«1»⊢ (f ⊚ s₈) B.b₂ = 𝟙 B B.b₂ rflAll goals completed! 🐙