blob: b7c31031dc47351d9f1c233ea603b770cf3cb007 (
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
module Object.Biproduct {o ℓ e} (𝒞 : Category o ℓ e) where
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
open import Categories.Object.Biproduct 𝒞 using () renaming (module Biproduct to Biproduct′)
open import Categories.Object.Biproduct 𝒞 public hiding (module Biproduct)
open import Morphism.Zero 𝒞 using (IsZero⇒)
open Category 𝒞
module Biproduct {A B : Obj} (BP : Biproduct A B) where
open Biproduct′ BP public
open ⇒-Reasoning
open HomReasoning
private
permute⟩∘⟨refl : {C : Obj} {f : C ⇒ A⊕B} → i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ f ≈ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ f
permute⟩∘⟨refl = refl⟩∘⟨ assoc²εβ ○ extendʳ permute ○ refl⟩∘⟨ assoc²βε
π₁i₂-constant : {C : Obj} (f g : C ⇒ B) → (π₁ ∘ i₂) ∘ f ≈ (π₁ ∘ i₂) ∘ g
π₁i₂-constant f g = begin
(π₁ ∘ i₂) ∘ f ≈⟨ assoc ⟩
π₁ ∘ i₂ ∘ f ≈⟨ insertˡ π₁∘i₁≈id ⟩
π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₂ ⟨
π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ ⟨ π₁ ∘ i₂ ∘ g , f ⟩ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩
π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ ⟨ π₁ ∘ i₂ ∘ g , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₁ ⟩
π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ g ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨
π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ∘ g ≈⟨ cancelˡ π₁∘i₁≈id ⟩
π₁ ∘ i₂ ∘ π₂ ∘ i₂ ∘ g ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ π₂∘i₂≈id ⟩
π₁ ∘ i₂ ∘ g ≈⟨ sym-assoc ⟩
(π₁ ∘ i₂) ∘ g ∎
π₁i₂-coconstant : {C : Obj} (f g : A ⇒ C) → f ∘ π₁ ∘ i₂ ≈ g ∘ π₁ ∘ i₂
π₁i₂-coconstant f g = begin
f ∘ π₁ ∘ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ π₂∘i₂≈id ⟩
f ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ pushˡ (Equiv.sym inject₁) ⟩
[ f , g ∘ π₁ ∘ i₂ ] ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩
[ f , g ∘ π₁ ∘ i₂ ] ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ≈⟨ extendʳ inject₂ ⟩
g ∘ (π₁ ∘ i₂) ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ≈⟨ refl⟩∘⟨ pullʳ (Equiv.sym permute⟩∘⟨refl) ⟩
g ∘ π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ cancelˡ π₁∘i₁≈id ⟩
g ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ π₂∘i₂≈id ⟩
g ∘ π₁ ∘ i₂ ∎
π₂i₁-coconstant : {C : Obj} (f g : B ⇒ C) → f ∘ π₂ ∘ i₁ ≈ g ∘ π₂ ∘ i₁
π₂i₁-coconstant f g = begin
f ∘ π₂ ∘ i₁ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ π₁∘i₁≈id ⟩
f ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ pushˡ (Equiv.sym inject₂) ⟩
[ g ∘ π₂ ∘ i₁ , f ] ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨
[ g ∘ π₂ ∘ i₁ , f ] ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ≈⟨ extendʳ inject₁ ⟩
g ∘ (π₂ ∘ i₁) ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ≈⟨ refl⟩∘⟨ pullʳ permute⟩∘⟨refl ⟩
g ∘ π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ cancelˡ π₂∘i₂≈id ⟩
g ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ π₁∘i₁≈id ⟩
g ∘ π₂ ∘ i₁ ∎
π₂i₁-constant : {C : Obj} (f g : C ⇒ A) → (π₂ ∘ i₁) ∘ f ≈ (π₂ ∘ i₁) ∘ g
π₂i₁-constant f g = begin
(π₂ ∘ i₁) ∘ f ≈⟨ assoc ⟩
π₂ ∘ i₁ ∘ f ≈⟨ insertˡ π₂∘i₂≈id ⟩
π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₁ ⟨
π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ ⟨ f , π₂ ∘ i₁ ∘ g ⟩ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨
π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ ⟨ f , π₂ ∘ i₁ ∘ g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₂ ⟩
π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ g ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩
π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ∘ g ≈⟨ cancelˡ π₂∘i₂≈id ⟩
π₂ ∘ i₁ ∘ π₁ ∘ i₁ ∘ g ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ π₁∘i₁≈id ⟩
π₂ ∘ i₁ ∘ g ≈⟨ sym-assoc ⟩
(π₂ ∘ i₁) ∘ g ∎
𝟎⇒ : A ⇒ B
𝟎⇒ = π₂ ∘ i₁
𝟎⇐ : B ⇒ A
𝟎⇐ = π₁ ∘ i₂
π₁∘i₂-isZero : IsZero⇒ (π₁ ∘ i₂)
π₁∘i₂-isZero = record
{ constant = π₁i₂-constant
; coconstant = π₁i₂-coconstant
}
π₂∘i₁-isZero : IsZero⇒ (π₂ ∘ i₁)
π₂∘i₁-isZero = record
{ constant = π₂i₁-constant
; coconstant = π₂i₁-coconstant
}
|
