diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 18:02:53 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 18:02:53 +0000 |
| commit | 1361fa660294004d4b231211102d681e6c3fc4c9 (patch) | |
| tree | 0c4e275e6d8b2475c50df7489223e18bf9f18492 | |
| parent | 2bc5a95f09b8f2f3537489a19254d9896bf47c7c (diff) | |
I: 4: b: show monomorphisms compose
| -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 ef560f9..ffae923 100644 --- a/src/CatTheory/Morphism/Properties.agda +++ b/src/CatTheory/Morphism/Properties.agda @@ -63,3 +63,7 @@ Retract⇒Mono {g = g} {f = f} g∘f≈id h₁ h₂ f∘h₁≈f∘h₂ = begin g ∘ (f ∘ h₁) ≈⟨ refl⟩∘⟨ f∘h₁≈f∘h₂ ⟩ g ∘ (f ∘ h₂) ≈⟨ cancelˡ g∘f≈id ⟩ h₂ ∎ + +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 |