blob: b19e04ba9b2c1cbc702ff1ee87324e019475a8a3 (
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
{-# 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!
Iso⇒Retract : Iso f g → g RetractOf f
Iso⇒Retract iso = isoˡ
where open Iso iso
Retract⇒Mono : g RetractOf f → Mono f
Retract⇒Mono {g = g} {f = f} g∘f≈id h₁ h₂ f∘h₁≈f∘h₂ = begin
h₁ ≈˘⟨ cancelˡ g∘f≈id ⟩
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
Mono-invʳ : Mono (f ∘ g) → Mono g
Mono-invʳ {f = f} {g = g} mono h₁ h₂ g∘h₁≈g∘h₂ =
mono h₁ h₂ $ assoc ○ ∘-resp-≈ʳ g∘h₁≈g∘h₂ ○ sym-assoc
|
