Skip to content

Commit e5fef74

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #347 from agda/BaseChange
Cleaning up Slice Functor and surrounding infrastructure
2 parents 85ecdcf + fce3d00 commit e5fef74

File tree

5 files changed

+117
-90
lines changed

5 files changed

+117
-90
lines changed

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category using (Category)
4+
5+
module Categories.Adjoint.Instance.BaseChange {o ℓ e} (C : Category o ℓ e) where
6+
7+
open import Categories.Adjoint using (_⊣_)
8+
open import Categories.Adjoint.Compose using (_∘⊣_)
9+
open import Categories.Adjoint.Instance.Slice using (Forgetful⊣Free)
10+
open import Categories.Category.Slice C using (Slice)
11+
open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice≃slice)
12+
open import Categories.Category.Equivalence.Properties using (module C≅D)
13+
open import Categories.Diagram.Pullback C using (Pullback)
14+
open import Categories.Functor.Slice.BaseChange C using (BaseChange!; BaseChange*)
15+
16+
open Category C
17+
18+
module _ {A B : Obj} (f : B ⇒ A) (pullback : ∀ {C} {h : C ⇒ A} → Pullback f h) where
19+
20+
!⊣* : BaseChange! f ⊣ BaseChange* f pullback
21+
!⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ Forgetful⊣Free (Slice A) (pullback⇒product pullback)

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

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
open import Categories.Category using (Category)
4+
5+
module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where
6+
7+
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)
10+
open import Categories.NaturalTransformation using (ntHelper)
11+
open import Categories.Object.Product C
12+
13+
open Category C
14+
open HomReasoning
15+
16+
open SliceObj
17+
open Slice⇒
18+
19+
module _ {A : Obj} (product : ∀ {X} → Product A X) where
20+
21+
private
22+
module product {X} = Product (product {X})
23+
open product
24+
25+
Forgetful⊣Free : Forgetful ⊣ Free product
26+
Forgetful⊣Free = record
27+
{ unit = ntHelper record
28+
{ η = λ _ → slicearr project₁
29+
; commute = λ {X} {Y} f → begin
30+
⟨ arr Y , id ⟩ ∘ h f ≈⟨ ∘-distribʳ-⟨⟩ ⟩
31+
⟨ arr Y ∘ h f , id ∘ h f ⟩ ≈⟨ ⟨⟩-cong₂ (△ f) identityˡ ⟩
32+
⟨ arr X , h f ⟩ ≈˘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
33+
⟨ id ∘ arr X , h f ∘ id ⟩ ≈˘⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
34+
[ product ⇒ product ] id × h f ∘ ⟨ arr X , id ⟩ ∎
35+
}
36+
; counit = ntHelper record
37+
{ η = λ _ → π₂
38+
; commute = λ _ → project₂
39+
}
40+
; zig = project₂
41+
; zag = begin
42+
[ product ⇒ product ]id× π₂ ∘ ⟨ π₁ , id ⟩ ≈⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
43+
⟨ id ∘ π₁ , π₂ ∘ id ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
44+
⟨ π₁ , π₂ ⟩ ≈⟨ η ⟩
45+
id ∎
46+
}

‎src/Categories/Category/Construction/Comma.agda‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ module _ {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂} {C : C
4343
h : B [ β₁ , β₂ ]
4444
commute : CommutativeSquare f₁ (T₁ g) (S₁ h) f₂
4545

46-
Comma : Functor A C → Functor B C → Category _ _ _
46+
Comma : Functor A C → Functor B C → Category (o₁ ⊔ o₂ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₂ ⊔ e₃) (e₁ ⊔ e₂)
4747
Comma T S = record
4848
{ Obj = CommaObj T S
4949
; _⇒_ = Comma⇒
@@ -132,8 +132,8 @@ module _ {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂} where
132132
module C = Category C
133133

134134
infix 4 _↙_ _↘_
135-
_↙_ : (X : C.Obj) (T : Functor D C) → Category _ _ _
135+
_↙_ : (X : C.Obj) (T : Functor D C) → Category (o₂ ⊔ ℓ₁) (ℓ₂ ⊔ e₁) e₂
136136
X ↙ T = const! X ↓ T
137137

138-
_↘_ : (S : Functor D C) (X : C.Obj) → Category _ _ _
138+
_↘_ : (S : Functor D C) (X : C.Obj) → Category (o₂ ⊔ ℓ₁) (ℓ₂ ⊔ e₁) e₂
139139
S ↘ X = S ↓ const! X

‎src/Categories/Functor/Slice.agda‎

Lines changed: 23 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,18 @@
11
{-# OPTIONS --without-K --safe #-}
22

3-
open import Categories.Category
3+
open import Categories.Category using (Category)
44

55
module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where
66

7-
open import Data.Product using (_,_)
7+
open import Function using () renaming (id to id→)
88

9-
open import Categories.Adjoint
10-
open import Categories.Category.CartesianClosed
11-
open import Categories.Category.CartesianClosed.Locally
12-
open import Categories.Functor hiding (id)
13-
open import Categories.Functor.Properties
9+
open import Categories.Diagram.Pullback C using (Pullback; unglue; Pullback-resp-≈)
10+
open import Categories.Functor using (Functor)
11+
open import Categories.Functor.Properties using ([_]-resp-∘)
1412
open import Categories.Morphism.Reasoning C
15-
open import Categories.NaturalTransformation hiding (id)
1613
open import Categories.Object.Product C
1714

1815
import Categories.Category.Slice as S
19-
import Categories.Diagram.Pullback as P
2016
import Categories.Category.Construction.Pullbacks as Pbs
2117

2218
open Category C
@@ -27,74 +23,32 @@ module _ {A : Obj} where
2723
open S.SliceObj
2824
open S.Slice⇒
2925

26+
-- A functor between categories induces one between the corresponding slices at a given object of C.
3027
Base-F : ∀ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} (F : Functor C D) → Functor (S.Slice C A) (S.Slice D (Functor.F₀ F A))
31-
Base-F {D = D} F = record
32-
{ F₀ = λ { (S.sliceobj arr) → S.sliceobj (F₁ arr) }
33-
; F₁ = λ { (S.slicearr △) → S.slicearr ([ F ]-resp-∘ △) }
28+
Base-F F = record
29+
{ F₀ = λ s → S.sliceobj (F₁ (arr s))
30+
; F₁ = λ s⇒ → S.slicearr ([ F ]-resp-∘ (△ s⇒))
3431
; identity = identity
3532
; homomorphism = homomorphism
3633
; F-resp-≈ = F-resp-≈
3734
}
38-
where module D = Category D
39-
open Functor F
35+
where open Functor F
4036

4137
open S C
4238

4339
Forgetful : Functor (Slice A) C
4440
Forgetful = record
45-
{ F₀ = λ X → Y X
46-
; F₁ = λ f → h f
41+
{ F₀ = Y
42+
; F₁ = h
4743
; identity = refl
4844
; homomorphism = refl
49-
; F-resp-≈ = λ eq → eq
45+
; F-resp-≈ = id→
5046
}
5147

52-
BaseChange! : ∀ {B} (f : B ⇒ A) → Functor (Slice B) (Slice A)
53-
BaseChange! f = record
54-
{ F₀ = λ X → sliceobj (f ∘ arr X)
55-
; F₁ = λ g → slicearr (pullʳ (△ g))
56-
; identity = refl
57-
; homomorphism = refl
58-
; F-resp-≈ = λ eq → eq
59-
}
60-
61-
62-
module _ (pullbacks : ∀ {X Y Z} (h : X ⇒ Z) (i : Y ⇒ Z) → P.Pullback C h i) where
48+
module _ (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
6349
private
64-
open P C
65-
module pullbacks {X Y Z} h i = Pullback (pullbacks {X} {Y} {Z} h i)
66-
open pullbacks
67-
68-
BaseChange* : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B)
69-
BaseChange* f = record
70-
{ F₀ = λ X → sliceobj (p₂ (arr X) f)
71-
; F₁ = λ {X Y} g → slicearr {h = Pullback.p₂ (unglue (pullbacks (arr Y) f)
72-
(Pullback-resp-≈ (pullbacks (arr X) f) (△ g) refl))}
73-
(p₂∘universal≈h₂ (arr Y) f)
74-
; identity = λ {X} → ⟺ (unique (arr X) f id-comm identityʳ)
75-
; homomorphism = λ {X Y Z} {h i} → unique-diagram (arr Z) f (p₁∘universal≈h₁ (arr Z) f ○ assoc ○ ⟺ (pullʳ (p₁∘universal≈h₁ (arr Y) f)) ○ ⟺ (pullˡ (p₁∘universal≈h₁ (arr Z) f)))
76-
(p₂∘universal≈h₂ (arr Z) f ○ ⟺ (p₂∘universal≈h₂ (arr Y) f) ○ ⟺ (pullˡ (p₂∘universal≈h₂ (arr Z) f)))
77-
; F-resp-≈ = λ {X Y} eq″ → unique (arr Y) f (p₁∘universal≈h₁ (arr Y) f ○ ∘-resp-≈ˡ eq″) (p₂∘universal≈h₂ (arr Y) f)
78-
}
79-
80-
81-
!⊣* : ∀ {B} (f : B ⇒ A) → BaseChange! f ⊣ BaseChange* f
82-
!⊣* f = record
83-
{ unit = ntHelper record
84-
{ η = λ X → slicearr (p₂∘universal≈h₂ (f ∘ arr X) f {eq = identityʳ})
85-
; commute = λ {X Y} g → unique-diagram (f ∘ arr Y) f
86-
(cancelˡ (p₁∘universal≈h₁ (f ∘ arr Y) f) ○ ⟺ (cancelʳ (p₁∘universal≈h₁ (f ∘ arr X) f)) ○ pushˡ (⟺ (p₁∘universal≈h₁ (f ∘ arr Y) f)))
87-
(pullˡ (p₂∘universal≈h₂ (f ∘ arr Y) f) ○ △ g ○ ⟺ (p₂∘universal≈h₂ (f ∘ arr X) f) ○ pushˡ (⟺ (p₂∘universal≈h₂ (f ∘ arr Y) f)))
88-
}
89-
; counit = ntHelper record
90-
{ η = λ X → slicearr (pullbacks.commute (arr X) f)
91-
; commute = λ {X Y} g → p₁∘universal≈h₁ (arr Y) f
92-
}
93-
; zig = λ {X} → p₁∘universal≈h₁ (f ∘ arr X) f
94-
; zag = λ {Y} → unique-diagram (arr Y) f
95-
(pullˡ (p₁∘universal≈h₁ (arr Y) f) ○ pullʳ (p₁∘universal≈h₁ (f ∘ pullbacks.p₂ (arr Y) f) f))
96-
(pullˡ (p₂∘universal≈h₂ (arr Y) f) ○ p₂∘universal≈h₂ (f ∘ pullbacks.p₂ (arr Y) f) f ○ ⟺ identityʳ)
97-
}
50+
module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i)
51+
open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁)
9852

9953
pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C
10054
pullback-functorial f = record
@@ -109,7 +63,7 @@ module _ {A : Obj} where
10963
(p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B))
11064
}
11165
where p : ∀ X → Pullback f (arr X)
112-
p X = pullbacks f (arr X)
66+
p X = pullback f (arr X)
11367
module p X = Pullback (p X)
11468

11569
p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y
@@ -128,35 +82,17 @@ module _ {A : Obj} where
12882

12983
module _ (product : {X : Obj} → Product A X) where
13084

85+
private
86+
module product {X} = Product (product {X})
87+
open product
88+
13189
-- this is adapted from proposition 1.33 of Aspects of Topoi (Freyd, 1972)
13290
Free : Functor C (Slice A)
13391
Free = record
134-
{ F₀ = λ _ → sliceobj [ product ]π₁
92+
{ F₀ = λ _ → sliceobj π₁
13593
; F₁ = λ f → slicearr ([ product ⇒ product ]π₁∘× ○ identityˡ)
13694
; identity = id×id product
13795
; homomorphism = sym [ product ⇒ product ⇒ product ]id×∘id×
138-
; F-resp-≈ = λ f≈g → Product.⟨⟩-cong₂ product refl (∘-resp-≈ˡ f≈g)
96+
; F-resp-≈ = λ f≈g → ⟨⟩-cong₂ refl (∘-resp-≈ˡ f≈g)
13997
}
14098

141-
Forgetful⊣Free : Forgetful ⊣ Free
142-
Forgetful⊣Free = record
143-
{ unit = ntHelper record
144-
{ η = λ _ → slicearr (Product.project₁ product)
145-
; commute = λ {X} {Y} f → begin
146-
[ product ]⟨ arr Y , id ⟩ ∘ h f ≈⟨ [ product ]⟨⟩∘ ⟩
147-
[ product ]⟨ arr Y ∘ h f , id ∘ h f ⟩ ≈⟨ Product.⟨⟩-cong₂ product (△ f) identityˡ ⟩
148-
[ product ]⟨ arr X , h f ⟩ ≈˘⟨ Product.⟨⟩-cong₂ product identityˡ identityʳ ⟩
149-
[ product ]⟨ id ∘ arr X , h f ∘ id ⟩ ≈˘⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
150-
[ product ⇒ product ] id × h f ∘ [ product ]⟨ arr X , id ⟩ ∎
151-
}
152-
; counit = ntHelper record
153-
{ η = λ _ → Product.π₂ product
154-
; commute = λ _ → Product.project₂ product
155-
}
156-
; zig = Product.project₂ product
157-
; zag = begin
158-
[ product ⇒ product ]id× [ product ]π₂ ∘ [ product ]⟨ [ product ]π₁ , id ⟩ ≈⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
159-
[ product ]⟨ id ∘ [ product ]π₁ , [ product ]π₂ ∘ id ⟩ ≈⟨ Product.⟨⟩-cong₂ product identityˡ identityʳ ⟩
160-
[ product ]⟨ [ product ]π₁ , [ product ]π₂ ⟩ ≈⟨ Product.η product ⟩
161-
id ∎
162-
}

‎src/Categories/Functor/Slice/BaseChange.agda‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category using (Category)
4+
5+
module Categories.Functor.Slice.BaseChange {o ℓ e} (C : Category o ℓ e) where
6+
7+
open import Categories.Category.Slice C using (Slice)
8+
open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice⇒slice; slice⇒slice-slice)
9+
open import Categories.Functor using (Functor; _∘F_)
10+
open import Categories.Functor.Slice using (Forgetful; Free)
11+
open import Categories.Diagram.Pullback C using (Pullback)
12+
13+
open Category C
14+
15+
module _ {A B : Obj} (f : B ⇒ A) where
16+
17+
-- Any morphism induces a functor between slices.
18+
BaseChange! : Functor (Slice B) (Slice A)
19+
BaseChange! = Forgetful (Slice A) ∘F slice⇒slice-slice f
20+
21+
-- Any morphism which admits pullbacks induces a functor the other way between slices.
22+
-- This is adjoint to BaseChange!: see Categories.Adjoint.Instance.BaseChange.
23+
BaseChange* : (∀ {C} {h : C ⇒ A} → Pullback f h) → Functor (Slice A) (Slice B)
24+
BaseChange* pullback = slice-slice⇒slice f ∘F Free (Slice A) (pullback⇒product pullback)

0 commit comments

Comments
 (0)