From 2bc5a95f09b8f2f3537489a19254d9896bf47c7c Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 5 Jan 2022 17:55:45 +0000 Subject: I: 4: a: prove retract hierarchy --- src/CatTheory/Morphism/Properties.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/CatTheory') diff --git a/src/CatTheory/Morphism/Properties.agda b/src/CatTheory/Morphism/Properties.agda index e268a6e..ef560f9 100644 --- a/src/CatTheory/Morphism/Properties.agda +++ b/src/CatTheory/Morphism/Properties.agda @@ -52,3 +52,14 @@ Iso-invˡ {g = g} {f = f} {h = h} {i = i} g∘f≈id iso = record Iso-invʳ : i SectionOf h → Iso (f ∘ h) (i ∘ g) → Iso f g Iso-invʳ h∘i≈id iso = Iso-swap $ Iso-invˡ h∘i≈id $ Iso-swap iso where open Cheat! + +Iso⇒Retract : Iso f g → g RetractOf f +Iso⇒Retract iso = isoˡ + where open Iso iso + +Retract⇒Mono : g RetractOf f → Mono f +Retract⇒Mono {g = g} {f = f} g∘f≈id h₁ h₂ f∘h₁≈f∘h₂ = begin + h₁ ≈˘⟨ cancelˡ g∘f≈id ⟩ + g ∘ (f ∘ h₁) ≈⟨ refl⟩∘⟨ f∘h₁≈f∘h₂ ⟩ + g ∘ (f ∘ h₂) ≈⟨ cancelˡ g∘f≈id ⟩ + h₂ ∎ -- cgit v1.2.3