blob: d0a6e7b7e9d3763f28645a4566cc900921cae751 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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₂
|
