I: 2: a: show isomorphisms composei-1-c

1 files changed, 29 insertions, 0 deletions

diff --git a/src/CatTheory/Morphism/Properties.agda b/src/CatTheory/Morphism/Properties.agda
new file mode 100644
index 0000000..d0a6e7b
--- /dev/null
+++ b/src/CatTheory/Morphism/Properties.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --without-K --safe #-}
+open import Categories.Category
+
+module CatTheory.Morphism.Properties {o ℓ e} (𝒞 : Category o ℓ e) where
+
+open Category 𝒞
+open HomReasoning
+
+import Categories.Morphism as M
+open M 𝒞
+open import Categories.Morphism.Reasoning 𝒞
+
+private
+  variable
+    A B C D : Obj
+    f g h i : A ⇒ B
+
+Iso-∘ : Iso f g → Iso h i → Iso (f ∘ h) (i ∘ g)
+Iso-∘ {f = f} {g = g} {h = h} {i = i} iso₁ iso₂ = record
+  { isoˡ = begin
+    (i ∘ g) ∘ f ∘ h ≈⟨ cancelInner iso₁.isoˡ ⟩
+    i ∘ h           ≈⟨ iso₂.isoˡ ⟩
+    id              ∎
+  ; isoʳ = begin
+    (f ∘ h) ∘ i ∘ g ≈⟨ cancelInner iso₂.isoʳ ⟩
+    f ∘ g           ≈⟨ iso₁.isoʳ ⟩
+    id              ∎
+  }
+  where module iso₁ = Iso iso₁; module iso₂ = Iso iso₂