Skip to content

Commit 54daf36

Browse files
ghost-not-in-the-shellghost-not-in-the-shell
committed
restricted version of yoneda lemma without naturality done
1 parent f061938 commit 54daf36

8 files changed

+187
-178
lines changed

‎Categories.agda

+62-62
Original file line numberDiff line numberDiff line change
@@ -16,28 +16,28 @@ instance
1616
𝓒𝓪𝓽∣op =
1717
let id : ∀ {𝓒} → 𝓒 ⟶ 𝓒
1818
id = record
19-
{ _₀_ = id
20-
; _₁_ = id
21-
; _₂_ = id
22-
; resp-∘₀ = refl
23-
; resp-∘₂ = refl
19+
{ _₀_ = id
20+
; _₁_ = id
21+
; _₁-cong_ = id
22+
; resp-∘₀ = refl
23+
; resp-∘₂ = refl
2424
}
2525

2626
_∘_ : ∀ {𝓒 𝓓 𝓔} → 𝓓 ⟶ 𝓔 → 𝓒 ⟶ 𝓓 → 𝓒 ⟶ 𝓔
2727
_∘_ {𝓒} {𝓓} {𝓔} 𝓖 𝓕 =
2828
let open CategoryReasoning 𝓔
2929
in record
30-
{ _₀_ = 𝓖 ₀_ ∘ 𝓕 ₀_
31-
; _₁_ = 𝓖 ₁_ ∘ 𝓕 ₁_
32-
; _₂_ = 𝓖 ₂_ ∘ 𝓕 ₂_
33-
; resp-∘₀ = λ {A} → begin
34-
𝓖 ₁ 𝓕 ₁ id₍ A ₎ ↓⟨ 𝓖 ₂ (resp-∘₀ 𝓕) ⟩
30+
{ _₀_ = 𝓖 ₀_ ∘ 𝓕 ₀_
31+
; _₁_ = 𝓖 ₁_ ∘ 𝓕 ₁_
32+
; _₁-cong_ = 𝓖 ₁-cong_ ∘ 𝓕 ₁-cong_
33+
; resp-∘₀ = λ {A} → begin
34+
𝓖 ₁ 𝓕 ₁ id₍ A ₎ ↓⟨ 𝓖 ₁-cong (resp-∘₀ 𝓕) ⟩
3535
𝓖 ₁ id₍ 𝓕 ₀ A ₎ ↓⟨ resp-∘₀ 𝓖 ⟩
3636
id₍ 𝓖 ₀ 𝓕 ₀ A ₎ ∎
37-
; resp-∘₂ = λ {A B C}
38-
{f : 𝓒 ∣ A ⟶ B}
39-
{g : 𝓒 ∣ B ⟶ C} → begin
40-
𝓖 ₁ 𝓕 ₁ (g ∘ f) ↓⟨ 𝓖 ₂ (resp-∘₂ 𝓕) ⟩
37+
; resp-∘₂ = λ {A B C}
38+
{f : 𝓒 ∣ A ⟶ B}
39+
{g : 𝓒 ∣ B ⟶ C} → begin
40+
𝓖 ₁ 𝓕 ₁ (g ∘ f) ↓⟨ 𝓖 ₁-cong (resp-∘₂ 𝓕) ⟩
4141
𝓖 ₁ (𝓕 ₁ g ∘ 𝓕 ₁ f) ↓⟨ resp-∘₂ 𝓖 ⟩
4242
𝓖 ₁ 𝓕 ₁ g ∘ 𝓖 ₁ 𝓕 ₁ f ∎
4343
}
@@ -59,7 +59,7 @@ module _ {𝓒 𝓓} where
5959
.𝓒𝓪𝓽∣∼-refl : ∀ {𝓕} → 𝓒𝓪𝓽∣ 𝓕 ∼ 𝓕
6060
.𝓒𝓪𝓽∣∼-sym : ∀ {𝓕 𝓖} → 𝓒𝓪𝓽∣ 𝓕 ∼ 𝓖 → 𝓒𝓪𝓽∣ 𝓖 ∼ 𝓕
6161
.𝓒𝓪𝓽∣∼-trans : ∀ {𝓕 𝓖 𝓗} → 𝓒𝓪𝓽∣ 𝓕 ∼ 𝓖 → 𝓒𝓪𝓽∣ 𝓖 ∼ 𝓗 → 𝓒𝓪𝓽∣ 𝓕 ∼ 𝓗
62-
𝓒𝓪𝓽∣∼-refl {𝓕} = ≡-refl , λ f∼g → 𝓕 ₂ f∼g
62+
𝓒𝓪𝓽∣∼-refl {𝓕} = ≡-refl , λ f∼g → 𝓕 ₁-cong f∼g
6363
𝓒𝓪𝓽∣∼-sym (≡-refl , 𝓕₁∼𝓖₁) = ≡-refl , λ f∼g → sym (𝓕₁∼𝓖₁ (sym f∼g))
6464
𝓒𝓪𝓽∣∼-trans (≡-refl , 𝓕₁∼𝓖₁) (≡-refl , 𝓖₁∼𝓗₁) = ≡-refl , λ f∼g → trans (𝓕₁∼𝓖₁ f∼g) (𝓖₁∼𝓗₁ refl)
6565

@@ -138,57 +138,57 @@ instance
138138
𝓒𝓪𝓽∣op✓ =
139139
let ! : ∀ {𝓧} → 𝓧 ⟶ 𝟙
140140
! = record
141-
{ _₀_ = !
142-
; _₁_ = !
143-
; _₂_ = !
144-
; resp-∘₀ = tt
145-
; resp-∘₂ = tt
141+
{ _₀_ = !
142+
; _₁_ = !
143+
; _₁-cong_ = !
144+
; resp-∘₀ = tt
145+
; resp-∘₂ = tt
146146
}
147147

148148
π₁ : ∀ {𝓒 𝓓} → 𝓒 × 𝓓 ⟶ 𝓒
149149
π₁ = record
150-
{ _₀_ = π₁
151-
; _₁_ = π₁
152-
; _₂_ = π₁
153-
; resp-∘₀ = refl
154-
; resp-∘₂ = refl
150+
{ _₀_ = π₁
151+
; _₁_ = π₁
152+
; _₁-cong_ = π₁
153+
; resp-∘₀ = refl
154+
; resp-∘₂ = refl
155155
}
156156

157157
π₂ : ∀ {𝓒 𝓓} → 𝓒 × 𝓓 ⟶ 𝓓
158158
π₂ = record
159-
{ _₀_ = π₂
160-
; _₁_ = π₂
161-
; _₂_ = π₂
162-
; resp-∘₀ = refl
163-
; resp-∘₂ = refl
159+
{ _₀_ = π₂
160+
; _₁_ = π₂
161+
; _₁-cong_ = π₂
162+
; resp-∘₀ = refl
163+
; resp-∘₂ = refl
164164
}
165165

166166
⟨_,_⟩ : ∀ {𝓒 𝓓 𝓧} → 𝓧 ⟶ 𝓒 → 𝓧 ⟶ 𝓓 → 𝓧 ⟶ 𝓒 × 𝓓
167167
⟨ 𝓕 , 𝓖 ⟩ = record
168-
{ _₀_ = ⟨ 𝓕 ₀_ , 𝓖 ₀_ ⟩
169-
; _₁_ = ⟨ 𝓕 ₁_ , 𝓖 ₁_ ⟩
170-
; _₂_ = ⟨ 𝓕 ₂_ , 𝓖 ₂_ ⟩
171-
; resp-∘₀ = resp-∘₀ 𝓕 , resp-∘₀ 𝓖
172-
; resp-∘₂ = resp-∘₂ 𝓕 , resp-∘₂ 𝓖
168+
{ _₀_ = ⟨ 𝓕 ₀_ , 𝓖 ₀_ ⟩
169+
; _₁_ = ⟨ 𝓕 ₁_ , 𝓖 ₁_ ⟩
170+
; _₁-cong_ = ⟨ 𝓕 ₁-cong_ , 𝓖 ₁-cong_ ⟩
171+
; resp-∘₀ = resp-∘₀ 𝓕 , resp-∘₀ 𝓖
172+
; resp-∘₂ = resp-∘₂ 𝓕 , resp-∘₂ 𝓖
173173
}
174174

175175
ε : ∀ {𝓒 𝓓} → [ 𝓒 , 𝓓 ] × 𝓒 ⟶ 𝓓
176176
ε {_} {𝓓} =
177177
let open CategoryReasoning 𝓓
178178
in record
179-
{ _₀_ = λ { (𝓕 , A) → 𝓕 ₀ A }
180-
; _₁_ = λ { {𝓕 , A} {𝓖 , B} (α , f) → α ₍ B ₎ ∘ 𝓕 ₁ f }
181-
; _₂_ = λ { {𝓕 , A} {𝓖 , B} {α , f} {α′ , f′} (α∼α′ , f∼f′) → ∘-cong₂ 𝓓 α∼α′ (𝓕 ₂ f∼f′) }
182-
; resp-∘₀ = λ { {𝓕 , A} → begin
179+
{ _₀_ = λ { (𝓕 , A) → 𝓕 ₀ A }
180+
; _₁_ = λ { {𝓕 , A} {𝓖 , B} (α , f) → α ₍ B ₎ ∘ 𝓕 ₁ f }
181+
; _₁-cong_ = λ { {𝓕 , A} {𝓖 , B} {α , f} {α′ , f′} (α∼α′ , f∼f′) → ∘-cong₂ 𝓓 α∼α′ (𝓕 ₁-cong f∼f′) }
182+
; resp-∘₀ = λ { {𝓕 , A} → begin
183183
id ∘ 𝓕 ₁ id ↓⟨ ∘-unitˡ 𝓓 ⟩
184184
𝓕 ₁ id ↓⟨ resp-∘₀ 𝓕 ⟩
185185
id ∎ }
186-
; resp-∘₂ = λ { {𝓕 , A} {𝓖 , B} {𝓗 , C}
187-
{α , f} -- α : 𝓝𝓪𝓽 ∣ 𝓕 ⟶ 𝓖
188-
-- f : 𝓒 ∣ A ⟶ B
189-
{β , g} -- β : 𝓝𝓪𝓽 ∣ 𝓖 ⟶ 𝓗
190-
-- g : 𝓒 ∣ B ⟶ C
191-
→ begin
186+
; resp-∘₂ = λ { {𝓕 , A} {𝓖 , B} {𝓗 , C}
187+
{α , f} -- α : 𝓝𝓪𝓽 ∣ 𝓕 ⟶ 𝓖
188+
-- f : 𝓒 ∣ A ⟶ B
189+
{β , g} -- β : 𝓝𝓪𝓽 ∣ 𝓖 ⟶ 𝓗
190+
-- g : 𝓒 ∣ B ⟶ C
191+
→ begin
192192
(β ∘₁ α) ₍ C ₎ ∘ 𝓕 ₁ (g ∘ f) ↓⟨ refl ⟩∘⟨ resp-∘₂ 𝓕 ⟩
193193
(β ₍ C ₎ ∘ α ₍ C ₎) ∘ (𝓕 ₁ g ∘ 𝓕 ₁ f) ↓⟨ ∘-assoc 𝓓 ⟩
194194
β ₍ C ₎ ∘ (α ₍ C ₎ ∘ (𝓕 ₁ g ∘ 𝓕 ₁ f)) ↑⟨ refl ⟩∘⟨ ∘-assoc 𝓓 ⟩
@@ -202,33 +202,33 @@ instance
202202
ƛ_ {𝓒} {𝓓} {𝓧} 𝓕 =
203203
let open CategoryReasoning 𝓓
204204
in record
205-
{ _₀_ = λ A → record
206-
{ _₀_ = λ B → 𝓕 ₀ (A , B)
207-
; _₁_ = λ {B₁ B₂} (b : 𝓒 ∣ B₁ ⟶ B₂) → 𝓕 ₁ (id₍ A ₎ , b)
208-
; _₂_ = λ {B₁ B₂} {b₁ b₂ : 𝓒 ∣ B₁ ⟶ B₂} b₁∼b₂ → 𝓕 ₂ (refl₍ id₍ A ₎ ₎ , b₁∼b₂)
209-
; resp-∘₀ = resp-∘₀ 𝓕
210-
; resp-∘₂ = λ {B₁ B₂ B₃}
211-
{b₁ : 𝓒 ∣ B₁ ⟶ B₂}
212-
{b₂ : 𝓒 ∣ B₂ ⟶ B₃} → begin
213-
𝓕 ₁ (id , b₂ ∘ b₁) ↑⟨ 𝓕 ₂ (∘-unitˡ 𝓧 , refl) ⟩
205+
{ _₀_ = λ A → record
206+
{ _₀_ = λ B → 𝓕 ₀ (A , B)
207+
; _₁_ = λ {B₁ B₂} (b : 𝓒 ∣ B₁ ⟶ B₂) → 𝓕 ₁ (id₍ A ₎ , b)
208+
; _₁-cong_ = λ {B₁ B₂} {b₁ b₂ : 𝓒 ∣ B₁ ⟶ B₂} b₁∼b₂ → 𝓕 ₁-cong (refl₍ id₍ A ₎ ₎ , b₁∼b₂)
209+
; resp-∘₀ = resp-∘₀ 𝓕
210+
; resp-∘₂ = λ {B₁ B₂ B₃}
211+
{b₁ : 𝓒 ∣ B₁ ⟶ B₂}
212+
{b₂ : 𝓒 ∣ B₂ ⟶ B₃} → begin
213+
𝓕 ₁ (id , b₂ ∘ b₁) ↑⟨ 𝓕 ₁-cong (∘-unitˡ 𝓧 , refl) ⟩
214214
𝓕 ₁ (id ∘ id , b₂ ∘ b₁) ↓⟨ resp-∘₂ 𝓕 ⟩
215215
𝓕 ₁ (id , b₂) ∘ 𝓕 ₁ (id , b₁) ∎
216216
}
217-
; _₁_ = λ {A₁ A₂} (a : 𝓧 ∣ A₁ ⟶ A₂) → record
217+
; _₁_ = λ {A₁ A₂} (a : 𝓧 ∣ A₁ ⟶ A₂) → record
218218
{ _₍_₎ = λ B → 𝓕 ₁ (a , id₍ B ₎)
219219
; natural = λ {B₁ B₂}
220220
{b : 𝓒 ∣ B₁ ⟶ B₂} → begin
221221
𝓕 ₁ (a , id) ∘ 𝓕 ₁ (id , b) ↑⟨ resp-∘₂ 𝓕 ⟩
222-
𝓕 ₁ (a ∘ id , id ∘ b) ↓⟨ 𝓕 ₂ (◁→▷ 𝓧 (∘-unitʳ 𝓧) (∘-unitˡ 𝓧) , ◁→▷ 𝓒 (∘-unitˡ 𝓒) (∘-unitʳ 𝓒)) ⟩
222+
𝓕 ₁ (a ∘ id , id ∘ b) ↓⟨ 𝓕 ₁-cong (◁→▷ 𝓧 (∘-unitʳ 𝓧) (∘-unitˡ 𝓧) , ◁→▷ 𝓒 (∘-unitˡ 𝓒) (∘-unitʳ 𝓒)) ⟩
223223
𝓕 ₁ (id ∘ a , b ∘ id) ↓⟨ resp-∘₂ 𝓕 ⟩
224224
𝓕 ₁ (id , b) ∘ 𝓕 ₁ (a , id) ∎
225225
}
226-
; _₂_ = λ {A₁ A₂} {a₁ a₂ : 𝓧 ∣ A₁ ⟶ A₂} a₁∼a₂ {B} → 𝓕 ₂ (a₁∼a₂ , refl₍ id₍ B ₎ ₎)
227-
; resp-∘₀ = resp-∘₀ 𝓕
228-
; resp-∘₂ = λ {A₁ A₂ A₃}
229-
{a₁ : 𝓧 ∣ A₁ ⟶ A₂}
230-
{a₂ : 𝓧 ∣ A₂ ⟶ A₃} → begin
231-
𝓕 ₁ (a₂ ∘ a₁ , id) ↑⟨ 𝓕 ₂ (refl , ∘-unitʳ 𝓒) ⟩
226+
; _₁-cong_ = λ {A₁ A₂} {a₁ a₂ : 𝓧 ∣ A₁ ⟶ A₂} a₁∼a₂ {B} → 𝓕 ₁-cong (a₁∼a₂ , refl₍ id₍ B ₎ ₎)
227+
; resp-∘₀ = resp-∘₀ 𝓕
228+
; resp-∘₂ = λ {A₁ A₂ A₃}
229+
{a₁ : 𝓧 ∣ A₁ ⟶ A₂}
230+
{a₂ : 𝓧 ∣ A₂ ⟶ A₃} → begin
231+
𝓕 ₁ (a₂ ∘ a₁ , id) ↑⟨ 𝓕 ₁-cong (refl , ∘-unitʳ 𝓒) ⟩
232232
𝓕 ₁ (a₂ ∘ a₁ , id ∘ id) ↓⟨ resp-∘₂ 𝓕 ⟩
233233
𝓕 ₁ (a₂ , id) ∘ 𝓕 ₁ (a₁ , id) ∎
234234
}

‎Functor.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@ open import Rosetta.Equivalence
66
record Functor (𝓒 𝓓 : Category) : Set where
77
infixr 6 _₀_
88
infixr 6 _₁_
9-
infixr 6 _₂_
9+
infixr 6 _₁-cong_
1010
field
11-
_₀_ : ob 𝓒 → ob 𝓓
12-
_₁_ : ∀ {A B} → 𝓒 ∣ A ⟶ B → 𝓓 ∣ _₀_ A ⟶ _₀_ B
13-
._₂_ : ∀ {A B} {f g : 𝓒 ∣ A ⟶ B}
11+
_₀_ : ob 𝓒 → ob 𝓓
12+
_₁_ : ∀ {A B} → 𝓒 ∣ A ⟶ B → 𝓓 ∣ _₀_ A ⟶ _₀_ B
13+
._₁-cong_ : ∀ {A B} {f g : 𝓒 ∣ A ⟶ B}
1414
→ 𝓒 ∣ f ∼ g
1515
→ 𝓓 ∣ _₁_ f ∼ _₁_ g
1616

‎HomFunctor.agda

+63-63
Original file line numberDiff line numberDiff line change
@@ -15,26 +15,26 @@ open CategoryReasoning 𝓒
1515
→ ∀ B
1616
→ 𝓢𝓮𝓽 ∣ 𝒉𝒐𝒎 𝓒 A B ⟶ 𝒉𝒐𝒎 𝓒 A′ B
1717
𝓱𝓸𝓶₍ f , B ₎ = record
18-
{ _₀_ = _∘ f
19-
; _₁_ = _⟩∘⟨ refl₍ f ₎
18+
{ _$_ = _∘ f
19+
; 𝒄𝒐𝒏𝒈 = _⟩∘⟨ refl₍ f ₎
2020
}
2121

2222
𝓱𝓸𝓶₍-,_₎ : ∀ B → 𝓒 ᵒᵖ ⟶ 𝓢𝓮𝓽
2323
𝓱𝓸𝓶₍-, B ₎ = record
24-
{ _₀_ = λ - → 𝒉𝒐𝒎 𝓒 - B
25-
; _₁_ = 𝓱𝓸𝓶₍_, B ₎
26-
; _₂_ = λ f₁∼f₂ g₁∼g₂ → g₁∼g₂ ⟩∘⟨ f₁∼f₂
27-
; resp-∘₀ = λ {A}
28-
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
29-
g₁∼g₂ → begin
24+
{ _₀_ = λ - → 𝒉𝒐𝒎 𝓒 - B
25+
; _₁_ = 𝓱𝓸𝓶₍_, B ₎
26+
; _₁-cong_ = λ f₁∼f₂ g₁∼g₂ → g₁∼g₂ ⟩∘⟨ f₁∼f₂
27+
; resp-∘₀ = λ {A}
28+
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
29+
g₁∼g₂ → begin
3030
g₁ ∘ id ↓⟨ ∘-unitʳ 𝓒 ⟩
3131
g₁ ↓⟨ g₁∼g₂ ⟩
3232
g₂ ∎
33-
; resp-∘₂ = λ {A A′ A″}
34-
{f : 𝓒 ᵒᵖ ∣ A ⟶ A′}
35-
{f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″}
36-
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
37-
g₁∼g₂ → begin
33+
; resp-∘₂ = λ {A A′ A″}
34+
{f : 𝓒 ᵒᵖ ∣ A ⟶ A′}
35+
{f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″}
36+
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
37+
g₁∼g₂ → begin
3838
g₁ ∘ (f′ ∘̅ f) ↓⟨ g₁∼g₂ ⟩∘⟨ refl ⟩
3939
g₂ ∘ (f ∘ f′) ↑⟨ ∘-assoc 𝓒 ⟩
4040
(g₂ ∘ f) ∘ f′ ∎
@@ -46,26 +46,26 @@ open CategoryReasoning 𝓒
4646
→ 𝓒 ∣ B ⟶ B′
4747
→ 𝓢𝓮𝓽 ∣ 𝒉𝒐𝒎 𝓒 A B ⟶ 𝒉𝒐𝒎 𝓒 A B′
4848
𝓱𝓸𝓶⁽ A , h ⁾ = record
49-
{ _₀_ = h ∘_
50-
; _₁_ = refl₍ h ₎ ⟩∘⟨_
49+
{ _$_ = h ∘_
50+
; 𝒄𝒐𝒏𝒈 = refl₍ h ₎ ⟩∘⟨_
5151
}
5252

5353
𝓱𝓸𝓶⁽_,-⁾ : ∀ A → 𝓒 ⟶ 𝓢𝓮𝓽
5454
𝓱𝓸𝓶⁽ A ,-⁾ = record
55-
{ _₀_ = λ - → 𝒉𝒐𝒎 𝓒 A -
56-
; _₁_ = 𝓱𝓸𝓶⁽ A ,_⁾
57-
; _₂_ = λ h₁∼h₂ g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂
58-
; resp-∘₀ = λ {B}
59-
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
60-
g₁∼g₂ → begin
55+
{ _₀_ = λ - → 𝒉𝒐𝒎 𝓒 A -
56+
; _₁_ = 𝓱𝓸𝓶⁽ A ,_⁾
57+
; _₁-cong_ = λ h₁∼h₂ g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂
58+
; resp-∘₀ = λ {B}
59+
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
60+
g₁∼g₂ → begin
6161
id ∘ g₁ ↓⟨ ∘-unitˡ 𝓒 ⟩
6262
g₁ ↓⟨ g₁∼g₂ ⟩
6363
g₂ ∎
64-
; resp-∘₂ = λ {B B′ B″}
65-
{h : 𝓒 ∣ B ⟶ B′}
66-
{h′ : 𝓒 ∣ B′ ⟶ B″}
67-
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
68-
g₁∼g₂ → begin
64+
; resp-∘₂ = λ {B B′ B″}
65+
{h : 𝓒 ∣ B ⟶ B′}
66+
{h′ : 𝓒 ∣ B′ ⟶ B″}
67+
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
68+
g₁∼g₂ → begin
6969
(h′ ∘ h) ∘ g₁ ↓⟨ refl ⟩∘⟨ g₁∼g₂ ⟩
7070
(h′ ∘ h) ∘ g₂ ↓⟨ ∘-assoc 𝓒 ⟩
7171
h′ ∘ (h ∘ g₂) ∎
@@ -75,24 +75,24 @@ open CategoryReasoning 𝓒
7575

7676
𝓱𝓸𝓶₍-,-₎ : 𝓒 ᵒᵖ × 𝓒 ⟶ 𝓢𝓮𝓽
7777
𝓱𝓸𝓶₍-,-₎ = record
78-
{ _₀_ = λ { (A , B) → 𝒉𝒐𝒎 𝓒 A B }
79-
; _₁_ = λ { {A , B} {A′ , B′} (f , h) → record
80-
{ _₀_ = λ g → h ∘ g ∘ f
81-
; _₁_ = λ g₁∼g₂ → refl₍ h ₎ ⟩∘⟨ g₁∼g₂ ⟩∘⟨ refl₍ f ₎
78+
{ _₀_ = λ { (A , B) → 𝒉𝒐𝒎 𝓒 A B }
79+
; _₁_ = λ { {A , B} {A′ , B′} (f , h) → record
80+
{ _$_ = λ g → h ∘ g ∘ f
81+
; 𝒄𝒐𝒏𝒈 = λ g₁∼g₂ → refl₍ h ₎ ⟩∘⟨ g₁∼g₂ ⟩∘⟨ refl₍ f ₎
8282
} }
83-
; _₂_ = λ { (f₁∼f₂ , h₁∼h₂) g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂ ⟩∘⟨ f₁∼f₂ }
84-
; resp-∘₀ = λ { {A , B} {g₁} {g₂} g₁∼g₂ → begin
83+
; _₁-cong_ = λ { (f₁∼f₂ , h₁∼h₂) g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂ ⟩∘⟨ f₁∼f₂ }
84+
; resp-∘₀ = λ { {A , B} {g₁} {g₂} g₁∼g₂ → begin
8585
id ∘ g₁ ∘ id ↓⟨ ∘-unitˡ 𝓒 ⟩
8686
g₁ ∘ id ↓⟨ ∘-unitʳ 𝓒 ⟩
8787
g₁ ↓⟨ g₁∼g₂ ⟩
8888
g₂ ∎ }
89-
; resp-∘₂ = λ { {A , B} {A′ , B′} {A″ , B″}
90-
{f , h } -- f : 𝓒 ᵒᵖ ∣ A ⟶ A′
91-
-- h : 𝓒 ∣ B ⟶ B′
92-
{f′ , h′} -- f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″
93-
-- h′ : 𝓒 ∣ B′ ⟶ B″
94-
{g₁} {g₂} -- g₁ g₂ : 𝓒 ∣ A ⟶ B
95-
g₁∼g₂ → begin
89+
; resp-∘₂ = λ { {A , B} {A′ , B′} {A″ , B″}
90+
{f , h } -- f : 𝓒 ᵒᵖ ∣ A ⟶ A′
91+
-- h : 𝓒 ∣ B ⟶ B′
92+
{f′ , h′} -- f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″
93+
-- h′ : 𝓒 ∣ B′ ⟶ B″
94+
{g₁} {g₂} -- g₁ g₂ : 𝓒 ∣ A ⟶ B
95+
g₁∼g₂ → begin
9696
(h′ ∘ h) ∘ g₁ ∘ (f′ ∘̅ f) ↓⟨ refl ⟩∘⟨ g₁∼g₂ ⟩∘⟨ refl ⟩
9797
(h′ ∘ h) ∘ g₂ ∘ (f ∘ f′) ↓⟨ ∘-assoc 𝓒 ⟩
9898
h′ ∘ h ∘ g₂ ∘ f ∘ f′ ↑⟨ refl ⟩∘⟨ ∘-assoc 𝓒 ⟩
@@ -131,43 +131,43 @@ open CategoryReasoning 𝓒
131131

132132
𝓱₋ : 𝓒 ⟶ [ 𝓒 ᵒᵖ , 𝓢𝓮𝓽 ]
133133
𝓱₋ = record
134-
{ _₀_ = 𝓱₍_₎₀
135-
; _₁_ = 𝓱₍_₎₁
136-
; _₂_ = λ h₁∼h₂ g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂
137-
; resp-∘₀ = λ {B A}
138-
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
139-
g₁∼g₂ → begin
134+
{ _₀_ = 𝓱₍_₎₀
135+
; _₁_ = 𝓱₍_₎₁
136+
; _₁-cong_ = λ h₁∼h₂ g₁∼g₂ → h₁∼h₂ ⟩∘⟨ g₁∼g₂
137+
; resp-∘₀ = λ {B A}
138+
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
139+
g₁∼g₂ → begin
140140
id ∘ g₁ ↓⟨ ∘-unitˡ 𝓒 ⟩
141141
g₁ ↓⟨ g₁∼g₂ ⟩
142142
g₂ ∎
143-
; resp-∘₂ = λ {B B′ B″}
144-
{h : 𝓒 ∣ B ⟶ B′}
145-
{h′ : 𝓒 ∣ B′ ⟶ B″}
146-
{A}
147-
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
148-
g₁∼g₂ → begin
143+
; resp-∘₂ = λ {B B′ B″}
144+
{h : 𝓒 ∣ B ⟶ B′}
145+
{h′ : 𝓒 ∣ B′ ⟶ B″}
146+
{A}
147+
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
148+
g₁∼g₂ → begin
149149
(h′ ∘ h) ∘ g₁ ↓⟨ refl ⟩∘⟨ g₁∼g₂ ⟩
150150
(h′ ∘ h) ∘ g₂ ↓⟨ ∘-assoc 𝓒 ⟩
151151
h′ ∘ (h ∘ g₂) ∎
152152
}
153153

154154
𝓱⁻ : 𝓒 ᵒᵖ ⟶ [ 𝓒 , 𝓢𝓮𝓽 ]
155155
𝓱⁻ = record
156-
{ _₀_ = 𝓱⁽_⁾⁰
157-
; _₁_ = 𝓱⁽_⁾¹
158-
; _₂_ = λ f₁∼f₂ g₁∼g₂ → g₁∼g₂ ⟩∘⟨ f₁∼f₂
159-
; resp-∘₀ = λ {A B}
160-
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
161-
g₁∼g₂ → begin
156+
{ _₀_ = 𝓱⁽_⁾⁰
157+
; _₁_ = 𝓱⁽_⁾¹
158+
; _₁-cong_ = λ f₁∼f₂ g₁∼g₂ → g₁∼g₂ ⟩∘⟨ f₁∼f₂
159+
; resp-∘₀ = λ {A B}
160+
{g₁ g₂ : 𝓒 ∣ A ⟶ B}
161+
g₁∼g₂ → begin
162162
g₁ ∘ id ↓⟨ ∘-unitʳ 𝓒 ⟩
163163
g₁ ↓⟨ g₁∼g₂ ⟩
164164
g₂ ∎
165-
; resp-∘₂ = λ {A A′ A″}
166-
{f : 𝓒 ᵒᵖ ∣ A ⟶ A′}
167-
{f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″}
168-
{B}
169-
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
170-
g₁∼g₂ → begin
165+
; resp-∘₂ = λ {A A′ A″}
166+
{f : 𝓒 ᵒᵖ ∣ A ⟶ A′}
167+
{f′ : 𝓒 ᵒᵖ ∣ A′ ⟶ A″}
168+
{B}
169+
{g₁ g₂ : 𝓒 ∣ A ⟶ B }
170+
g₁∼g₂ → begin
171171
g₁ ∘ (f′ ∘̅ f) ↓⟨ g₁∼g₂ ⟩∘⟨ refl ⟩
172172
g₂ ∘ (f ∘ f′) ↑⟨ ∘-assoc 𝓒 ⟩
173173
(g₂ ∘ f) ∘ f′ ∎

0 commit comments

Comments
 (0)