From eebb9efadd33a3d901dfa87b00b5dde347d8fa6a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 5 Jan 2022 18:05:08 +0000 Subject: I: 4: c: show monomorphisms decompose --- src/CatTheory/Morphism/Properties.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/CatTheory/Morphism/Properties.agda b/src/CatTheory/Morphism/Properties.agda index ffae923..b19e04b 100644 --- a/src/CatTheory/Morphism/Properties.agda +++ b/src/CatTheory/Morphism/Properties.agda @@ -67,3 +67,7 @@ Retract⇒Mono {g = g} {f = f} g∘f≈id h₁ h₂ f∘h₁≈f∘h₂ = begin Mono∘ : Mono f → Mono g → Mono (f ∘ g) Mono∘ {f = f} {g = g} f-mono g-mono h₁ h₂ f∘g∘h₁≈f∘g∘h₂ = g-mono h₁ h₂ $ f-mono (g ∘ h₁) (g ∘ h₂) $ sym-assoc ○ f∘g∘h₁≈f∘g∘h₂ ○ assoc + +Mono-invʳ : Mono (f ∘ g) → Mono g +Mono-invʳ {f = f} {g = g} mono h₁ h₂ g∘h₁≈g∘h₂ = + mono h₁ h₂ $ assoc ○ ∘-resp-≈ʳ g∘h₁≈g∘h₂ ○ sym-assoc -- cgit v1.2.3