diff options
Diffstat (limited to 'src/CatTheory/Morphism/Properties.agda')
| -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₂ ∎ |