Skip to content

Commit 7a6d419

Browse files
mortbergmortberg
authored
Clean code for category of elements and simplify a presheaf notation (#1266)
1 parent 1a003b2 commit 7a6d419

File tree

4 files changed

+85
-123
lines changed

4 files changed

+85
-123
lines changed

‎Cubical/Categories/Constructions/Elements.agda‎

Lines changed: 75 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -1,141 +1,103 @@
1-
21
-- The category of elements of a functor to Set
2+
module Cubical.Categories.Constructions.Elements where
33

4+
open import Cubical.Foundations.Prelude
45
open import Cubical.Foundations.Equiv
56
open import Cubical.Foundations.Isomorphism
6-
open import Cubical.Foundations.Function
77
open import Cubical.Foundations.HLevels
8-
open import Cubical.Foundations.Path
9-
open import Cubical.Foundations.Prelude
108

119
open import Cubical.Data.Sigma
1210

1311
open import Cubical.Categories.Category
14-
import Cubical.Categories.Constructions.Slice.Base as Slice
1512
open import Cubical.Categories.Functor
1613
open import Cubical.Categories.Instances.Sets
1714
open import Cubical.Categories.Isomorphism
18-
import Cubical.Categories.Morphism as Morphism
19-
2015

21-
module Cubical.Categories.Constructions.Elements where
22-
23-
-- some issues
24-
-- * always need to specify objects during composition because can't infer isSet
2516
open Category
2617
open Functor
2718

2819
module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
20+
21+
open Category C
22+
23+
private
2924
getIsSet : ∀ {ℓS} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆))
3025
getIsSet F c = snd (F ⟅ c ⟆)
3126

32-
Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS)
33-
Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
34-
35-
infix 50 ∫_
36-
∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
37-
-- objects are (c , x) pairs where c ∈ C and x ∈ F c
38-
(∫ F) .ob = Element F
39-
-- morphisms are f : c → c' which take x to x'
40-
(∫ F) .Hom[_,_] (c , x) (c' , x') = fiber (λ (f : C [ c , c' ]) → (F ⟪ f ⟫) x) x'
41-
(∫ F) .id {x = (c , x)} = C .id , funExt⁻ (F .F-id) x
42-
(∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
43-
= (f ⋆⟨ C ⟩ g) , ((F ⟪ f ⋆⟨ C ⟩ g ⟫) x
44-
≡⟨ funExt⁻ (F .F-seq _ _) _ ⟩
45-
(F ⟪ g ⟫) ((F ⟪ f ⟫) x)
46-
≡⟨ cong (F ⟪ g ⟫) p ⟩
47-
(F ⟪ g ⟫) x₁
48-
≡⟨ q ⟩
49-
x₂
50-
∎)
51-
(∫ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i
52-
= (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdL i
53-
where
54-
isS = getIsSet F c
55-
isS' = getIsSet F c'
56-
cIdL = C .⋆IdL f
57-
58-
-- proof from composition with id
59-
p' : (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x ≡ x'
60-
p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f')
61-
(∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
62-
= (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdR i
63-
where
64-
cIdR = C .⋆IdR f
65-
isS' = getIsSet F c'
66-
67-
p' : (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x ≡ x'
68-
p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id))
69-
(∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
70-
= (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ ((F ⟪ a ⟫) x) x₃) p1 p2 cAssoc i
71-
where
72-
cAssoc = C .⋆Assoc f g h
73-
isS₃ = getIsSet F c₃
74-
75-
p1 : (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x ≡ x₃
76-
p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h')
77-
78-
p2 : (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x ≡ x₃
79-
p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h'))
80-
(∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
81-
82-
ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {c,f c',f' : Element F}
83-
→ {χ1,ef1 χ2,ef2 : (∫ F) [ c,f , c',f' ]} → (fst χ1,ef1 ≡ fst χ2,ef2) → (χ1,ef1 ≡ χ2,ef2)
84-
ElementHom≡ F {c1 , f1} {c2 , f2} {χ1 , ef1} {χ2 , ef2} eχ = cong₂ _,_ eχ
85-
(fst (isOfHLevelPathP' 0 (snd (F ⟅ c2 ⟆) _ _) ef1 ef2))
86-
87-
ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
88-
F-ob (ForgetElements F) = fst
89-
F-hom (ForgetElements F) = fst
90-
F-id (ForgetElements F) = refl
91-
F-seq (ForgetElements F) _ _ = refl
92-
93-
module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
94-
open isUnivalent
95-
isUnivalent∫ : isUnivalent (∫ F)
96-
isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
97-
( isoToPath∫
98-
, (λ f≅f' → CatIso≡ _ _
99-
(Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
100-
(cong fst
101-
(secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
102-
, λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
103-
( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
104-
∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
105-
106-
isoToPath∫ : ∀ {c c' f f'}
107-
→ CatIso (∫ F) (c , f) (c' , f')
108-
→ (c , f) ≡ (c' , f')
109-
isoToPath∫ {f = f} f≅f' = ΣPathP
110-
( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
111-
, toPathP ( (λ j → transport (λ i → fst
112-
(F-isoToPath isUnivC isUnivalentSET F
113-
(F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
114-
∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
115-
∙ f≅f' .fst .snd))
116-
27+
Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS)
28+
Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
29+
30+
infix 50 ∫_
31+
32+
∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
33+
-- objects are (c , x) pairs where c ∈ C and x ∈ F c
34+
(∫ F) .ob = Element F
35+
-- morphisms are f : c → c' which take x to x'
36+
(∫ F) .Hom[_,_] (c , x) (c' , x') = fiber (λ (f : C [ c , c' ]) → F .F-hom f x) x'
37+
(∫ F) .id .fst = id C
38+
(∫ F) .id {x} .snd = funExt⁻ (F .F-id) (x .snd)
39+
(∫ F) ._⋆_ (f , p) (g , q) .fst = f ⋆⟨ C ⟩ g
40+
(∫ F) ._⋆_ (f , p) (g , q) .snd = funExt⁻ (F .F-seq _ _) _ ∙∙ cong (F ⟪ g ⟫) p ∙∙ q
41+
(∫ F) .⋆IdL _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆IdL C _)
42+
(∫ F) .⋆IdR _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆IdR C _)
43+
(∫ F) .⋆Assoc _ _ _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆Assoc C _ _ _)
44+
(∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
45+
46+
ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {x y : Element F}
47+
→ {f g : (∫ F) [ x , y ]} → fst f ≡ fst g → f ≡ g
48+
ElementHom≡ F = Σ≡Prop (λ _ → getIsSet F _ _ _)
49+
50+
ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
51+
F-ob (ForgetElements F) = fst
52+
F-hom (ForgetElements F) = fst
53+
F-id (ForgetElements F) = refl
54+
F-seq (ForgetElements F) _ _ = refl
55+
56+
module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
57+
open isUnivalent
58+
isUnivalent∫ : isUnivalent (∫ F)
59+
isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
60+
( isoToPath∫
61+
, (λ f≅f' → CatIso≡ _ _
62+
(Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
63+
(cong fst
64+
(secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
65+
, λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
66+
( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
67+
∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
68+
69+
isoToPath∫ : ∀ {c c' f f'}
70+
→ CatIso (∫ F) (c , f) (c' , f')
71+
→ (c , f) ≡ (c' , f')
72+
isoToPath∫ {f = f} f≅f' = ΣPathP
73+
( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
74+
, toPathP ( (λ j → transport (λ i → fst
75+
(F-isoToPath isUnivC isUnivalentSET F
76+
(F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
77+
∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
78+
∙ f≅f' .fst .snd))
11779

11880
module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
119-
open Covariant {C = C ^op}
81+
open Covariant {C = C ^op}
12082

121-
-- same thing but for presheaves
122-
∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
123-
∫ᴾ F = (∫ F) ^op
83+
-- same thing but for presheaves
84+
∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
85+
∫ᴾ F = (∫ F) ^op
12486

125-
Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS)
126-
Elementᴾ F = (∫ᴾ F) .ob
87+
Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS)
88+
Elementᴾ F = (∫ᴾ F) .ob
12789

128-
-- helpful results
90+
-- helpful results
12991

130-
module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where
92+
module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where
13193

132-
-- morphisms are equal as long as the morphisms in C are equal
133-
∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ])
134-
→ (p : o1 ≡ o1') (q : o2 ≡ o2')
135-
→ (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
136-
→ PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
137-
∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _)
94+
-- morphisms are equal as long as the morphisms in C are equal
95+
∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ])
96+
→ (p : o1 ≡ o1') (q : o2 ≡ o2')
97+
→ (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
98+
→ PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
99+
∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _)
138100

139-
∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ])
140-
→ fst f ≡ fst g → f ≡ g
141-
∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p
101+
∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ])
102+
→ fst f ≡ fst g → f ≡ g
103+
∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p

‎Cubical/Categories/Presheaf/Base.agda‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -26,21 +26,21 @@ isUnivalentPresheafCategory = isUnivalentFUNCTOR _ _ isUnivalentSET
2626
open Category
2727
open Functor
2828

29-
action : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS)
29+
action : {C : Category ℓ ℓ'} → (P : Presheaf C ℓS)
3030
→ {a b : C .ob} → C [ a , b ] → fst (P ⟅ b ⟆) → fst (P ⟅ a ⟆)
31-
action C P = P .F-hom
31+
action P = P .F-hom
3232

3333
-- Convenient notation for naturality
34-
syntax action C P f ϕ = ϕ ∘ᴾ⟨ C , P ⟩ f
34+
syntax action P f ϕ = ϕ ∘ᴾ⟨ P ⟩ f
3535

3636
∘ᴾId : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a : C .ob}
3737
→ (ϕ : fst (P ⟅ a ⟆))
38-
→ ϕ ∘ᴾ⟨ C , P ⟩ C .id ≡ ϕ
38+
→ ϕ ∘ᴾ⟨ P ⟩ C .id ≡ ϕ
3939
∘ᴾId C P ϕ i = P .F-id i ϕ
4040

4141
∘ᴾAssoc : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a b c : C .ob}
4242
→ (ϕ : fst (P ⟅ c ⟆))
4343
→ (f : C [ b , c ])
4444
→ (g : C [ a , b ])
45-
→ ϕ ∘ᴾ⟨ C , P ⟩ (f ∘⟨ C ⟩ g) ≡ (ϕ ∘ᴾ⟨ C , P ⟩ f) ∘ᴾ⟨ C , P ⟩ g
45+
→ ϕ ∘ᴾ⟨ P ⟩ (f ∘⟨ C ⟩ g) ≡ (ϕ ∘ᴾ⟨ P ⟩ f) ∘ᴾ⟨ P ⟩ g
4646
∘ᴾAssoc C P ϕ f g i = P .F-seq f g i ϕ

‎Cubical/Categories/Presheaf/Morphism.agda‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,17 +56,17 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
5656
pushElt (A , η) = (F ⟅ A ⟆) , (h .N-ob A (lift η) .lower)
5757

5858
pushEltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ])
59-
→ (pushElt η .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f)
60-
≡ pushElt (B , η .snd ∘ᴾ⟨ C , P ⟩ f) .snd
59+
→ (pushElt η .snd ∘ᴾ⟨ Q ⟩ F .F-hom f)
60+
≡ pushElt (B , η .snd ∘ᴾ⟨ P ⟩ f) .snd
6161
pushEltNat η f i = h .N-hom f (~ i) (lift (η .snd)) .lower
6262

6363
pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q)
6464
pushEltF .F-ob = pushElt
6565
pushEltF .F-hom {x}{y} (f , commutes) .fst = F .F-hom f
6666
pushEltF .F-hom {x}{y} (f , commutes) .snd =
67-
pushElt _ .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f
67+
pushElt _ .snd ∘ᴾ⟨ Q ⟩ F .F-hom f
6868
≡⟨ pushEltNat y f ⟩
69-
pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd
69+
pushElt (_ , y .snd ∘ᴾ⟨ P ⟩ f) .snd
7070
≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , commutes)) ⟩
7171
pushElt x .snd ∎
7272
pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id)

‎Cubical/Categories/Presheaf/Representable.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
7474
isUniversal : (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst)
7575
→ Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
7676
isUniversal vertex element =
77-
∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ C , P ⟩ f
77+
∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ P ⟩ f
7878

7979
isPropIsUniversal : ∀ vertex element → isProp (isUniversal vertex element)
8080
isPropIsUniversal vertex element = isPropΠ (λ _ → isPropIsEquiv _)

0 commit comments

Comments
 (0)