From 3d72d984c0a1aa60f137d5380ea49b1d5716ea48 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 5 Jan 2022 16:04:40 +0000
Subject: I: 2: a: show isomorphisms compose

---
 src/CatTheory/Morphism/Properties.agda | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 src/CatTheory/Morphism/Properties.agda

(limited to 'src/CatTheory/Morphism')

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₂
-- 
cgit v1.2.3