diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 17:55:45 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 17:55:45 +0000 |
| commit | 2bc5a95f09b8f2f3537489a19254d9896bf47c7c (patch) | |
| tree | 33e7d19a96dc0a0d0952041cda662b861851d7fa | |
| parent | ed2e037c8373f1c697ca46055523a72143b2a332 (diff) | |
I: 4: a: prove retract hierarchy
| -rw-r--r-- | src/CatTheory/Morphism/Properties.agda | 11 |
1 files changed, 11 insertions, 0 deletions
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₂ ∎ |