diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 18:05:08 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 18:05:08 +0000 |
| commit | eebb9efadd33a3d901dfa87b00b5dde347d8fa6a (patch) | |
| tree | 7c884672fb474f7a94a0f3dd7049d712a89e9edd /src/CatTheory/Morphism | |
| parent | 1361fa660294004d4b231211102d681e6c3fc4c9 (diff) | |
I: 4: c: show monomorphisms decompose
Diffstat (limited to 'src/CatTheory/Morphism')
| -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 |