blob: e268a6e6cee00902c0e5c8bbc139395ad148a982 (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
module CatTheory.Morphism.Properties {o ℓ e} (𝒞 : Category o ℓ e) where
open Category 𝒞
open HomReasoning
open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
open import Function using (_$_)
import Categories.Morphism.Properties as Mₚ
module Cheat! = Mₚ 𝒞
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₂
Iso-invˡ : g RetractOf f → Iso (f ∘ h) (i ∘ g) → Iso h i
Iso-invˡ {g = g} {f = f} {h = h} {i = i} g∘f≈id iso = record
{ isoˡ = begin
i ∘ h ≈⟨ intro-center g∘f≈id ⟩
i ∘ (g ∘ f) ∘ h ≈⟨ refl⟩∘⟨ assoc ⟩
i ∘ g ∘ f ∘ h ≈⟨ sym-assoc ⟩
(i ∘ g) ∘ (f ∘ h) ≈⟨ isoˡ ⟩
id ∎
; isoʳ = begin
h ∘ i ≈⟨ intro-last g∘f≈id ⟩
h ∘ (i ∘ g) ∘ f ≈⟨ intro-first g∘f≈id ⟩
g ∘ (f ∘ h) ∘ (i ∘ g) ∘ f ≈⟨ sym-assoc ⟩
(g ∘ f ∘ h) ∘ (i ∘ g) ∘ f ≈⟨ cancelInner isoʳ ⟩
g ∘ f ≈⟨ g∘f≈id ⟩
id ∎
}
where open Iso iso
Iso-invʳ : i SectionOf h → Iso (f ∘ h) (i ∘ g) → Iso f g
Iso-invʳ h∘i≈id iso = Iso-swap $ Iso-invˡ h∘i≈id $ Iso-swap iso
where open Cheat!
|
