diff options
| -rw-r--r-- | src/CatTheory/Morphism/Properties.agda | 4 |
1 files changed, 4 insertions, 0 deletions
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 |