Skip to content

Commit 182cc4e

Browse files
TanebTaneb
committed
Define adjoint
1 parent 44363cc commit 182cc4e

File tree

1 file changed

+101
-2
lines changed

1 file changed

+101
-2
lines changed

‎src/Categories/Adjoint/Instance/Slice.agda‎

Lines changed: 101 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,18 @@ open import Categories.Category using (Category)
55
module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where
66

77
open import Categories.Adjoint using (_⊣_)
8-
open import Categories.Category.Slice C using (SliceObj; Slice⇒; slicearr)
9-
open import Categories.Functor.Slice C using (Forgetful; Free)
8+
open import Categories.Category.BinaryProducts C
9+
open import Categories.Category.Cartesian using (Cartesian)
10+
open import Categories.Category.CartesianClosed using (CartesianClosed)
11+
open import Categories.Category.Slice C using (SliceObj; sliceobj; Slice⇒; slicearr)
12+
open import Categories.Functor.Slice C using (Forgetful; Free; Coforgetful)
13+
open import Categories.Morphism.Reasoning C
1014
open import Categories.NaturalTransformation using (ntHelper)
15+
open import Categories.Diagram.Pullback C hiding (swap)
1116
open import Categories.Object.Product C
17+
open import Categories.Object.Terminal C
18+
19+
open import Function.Base using (_$_)
1220

1321
open Category C
1422
open HomReasoning
@@ -44,3 +52,94 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where
4452
⟨ π₁ , π₂ ⟩ ≈⟨ η ⟩
4553
id ∎
4654
}
55+
56+
module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
57+
58+
open CartesianClosed ccc
59+
open Cartesian cartesian
60+
open Terminal terminal
61+
open BinaryProducts products
62+
63+
Free⊣Coforgetful : Free {A = A} product ⊣ Coforgetful ccc pullback
64+
Free⊣Coforgetful = record
65+
{ unit = ntHelper record
66+
{ η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X))
67+
; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin
68+
p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ f ≈⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
69+
λg swap ∘ f ≈⟨ subst ⟩
70+
λg (swap ∘ first f) ≈⟨ λ-cong swap∘⁂ ⟩
71+
λg (second f ∘ swap) ≈˘⟨ λ-cong (∘-resp-≈ʳ β′) ⟩
72+
λg (second f ∘ eval′ ∘ first (λg swap)) ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl))) ⟩
73+
λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _)) ≈˘⟨ λ-cong (pull-last first∘first) ⟩
74+
λg ((second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ first (p.universal (sliceobj π₁) _)) ≈˘⟨ subst ⟩
75+
λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
76+
p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ p.universal (sliceobj π₁) _ ∎
77+
}
78+
; counit = ntHelper record
79+
{ η = λ X → slicearr (counit-△ X)
80+
; commute = λ {S} {T} f → begin
81+
(eval′ ∘ first (p.p₂ T) ∘ swap) ∘ second (p.universal T _) ≈⟨ pull-last swap∘⁂ ⟩
82+
eval′ ∘ first (p.p₂ T) ∘ first (p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
83+
eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ T) Equiv.refl ⟩∘⟨refl ⟩
84+
eval′ ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∘ swap ≈⟨ pullˡ β′ ⟩
85+
(h f ∘ eval′ ∘ first (p.p₂ S)) ∘ swap ≈⟨ assoc²' ⟩
86+
h f ∘ eval′ ∘ first (p.p₂ S) ∘ swap ∎
87+
}
88+
; zig = λ {X} → begin
89+
(eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap) ∘ second (p.universal (sliceobj π₁) _) ≈⟨ assoc²' ⟩
90+
eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap ∘ second (p.universal (sliceobj π₁) _) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘⁂ ⟩
91+
eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ first (p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
92+
eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl ⟩∘⟨refl ⟩
93+
eval′ ∘ first (λg swap) ∘ swap ≈⟨ pullˡ β′ ⟩
94+
swap ∘ swap ≈⟨ swap∘swap ⟩
95+
id ∎
96+
; zag = λ {X} → p.unique-diagram X !-unique₂ $ begin
97+
p.p₂ X ∘ p.universal X _ ∘ p.universal (sliceobj π₁) _ ≈⟨ pullˡ (p.p₂∘universal≈h₂ X) ⟩
98+
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩
99+
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩
100+
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap ≈⟨ subst ⟩
101+
λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap)) ≈⟨ λ-cong (pullʳ β′) ⟩
102+
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pull-last swap∘swap) ⟩
103+
λg (eval′ ∘ first (p.p₂ X) ∘ id) ≈⟨ λ-cong (∘-resp-≈ʳ identityʳ) ⟩
104+
λg (eval′ ∘ first (p.p₂ X)) ≈⟨ η-exp′ ⟩
105+
p.p₂ X ≈˘⟨ identityʳ ⟩
106+
p.p₂ X ∘ id ∎
107+
}
108+
where
109+
p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′))
110+
p X = pullback (λg π₂) (λg (arr X ∘ eval′))
111+
module p X = Pullback (p X)
112+
113+
abstract1
114+
unit-pb : ∀ (X : Obj) → eval′ ∘ first {A = X} {C = A} (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap)
115+
unit-pb X = begin
116+
eval′ ∘ first (λg π₂ ∘ !) ≈˘⟨ refl⟩∘⟨ first∘first ⟩
117+
eval′ ∘ first (λg π₂) ∘ first ! ≈⟨ pullˡ β′ ⟩
118+
π₂ ∘ first ! ≈⟨ π₂∘⁂ ○ identityˡ ⟩
119+
π₂ ≈˘⟨ project₁ ⟩
120+
π₁ ∘ swap ≈˘⟨ refl⟩∘⟨ β′ ⟩
121+
π₁ ∘ eval′ ∘ first (λg swap) ≈˘⟨ extendʳ β′ ⟩
122+
eval′ ∘ first (λg (π₁ ∘ eval′)) ∘ first (λg swap) ≈⟨ refl⟩∘⟨ first∘first ⟩
123+
eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap) ∎
124+
-- A good chunk of the above, maybe all if you squint, is duplicated with F₁-lemma
125+
-- eval′ ∘ first (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (f ∘ eval′) ∘ first (λg g)
126+
-- With f : X ⇒ Y and g : Z × Y ⇒ X. Not sure what conditions f and g need to have
127+
128+
-- Would it be better if Free used π₂ rather than π₁?
129+
-- It would mean we could avoid this swap
130+
counit-△ : ∀ X → arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈ π₁
131+
counit-△ X = begin
132+
arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈˘⟨ assoc² ⟩
133+
((arr X ∘ eval′) ∘ first (p.p₂ X)) ∘ swap ≈⟨ lemma ⟩∘⟨refl ⟩
134+
(π₂ ∘ first (p.p₁ X)) ∘ swap ≈⟨ (π₂∘⁂ ○ identityˡ) ⟩∘⟨refl ⟩
135+
π₂ ∘ swap ≈⟨ project₂ ⟩
136+
π₁ ∎
137+
where
138+
lemma : (arr X ∘ eval′) ∘ first (p.p₂ X) ≈ π₂ ∘ first (p.p₁ X)
139+
lemma = λ-inj $ begin
140+
λg ((arr X ∘ eval′) ∘ first (p.p₂ X)) ≈˘⟨ subst ⟩
141+
λg (arr X ∘ eval′) ∘ p.p₂ X ≈˘⟨ p.commute X ⟩
142+
λg π₂ ∘ p.p₁ X ≈⟨ subst ⟩
143+
λg (π₂ ∘ first (p.p₁ X)) ∎
144+
145+

0 commit comments

Comments
 (0)