{-# OPTIONS --safe #-}
module Cubical.Categories.Presheaf.Properties where
open import Cubical.Categories.Category renaming (isIso to isIsoC)
open import Cubical.Categories.Constructions.Lift
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Functor
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Equivalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv using (fiber)
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)
import Cubical.Categories.Morphism as Morphism
import Cubical.Categories.Constructions.Slice as Slice
import Cubical.Categories.Constructions.Elements as Elements
import Cubical.Functions.Fibration as Fibration
private
variable
ℓ ℓ' : Level
ℓS ℓS' : Level
e e' : Level
module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) where
open Category
open Functor
open _≃ᶜ_
open WeakInverse
open NatTrans
open NatIso
open Slice (PresheafCategory C ℓS) F
open Elements.Contravariant {C = C}
open Fibration.ForSets
fibersEqIfRepsEqNatTrans : ∀ {A} (ϕ : A ⇒ F) {c x x'} {px : x ≡ x'} {a' : fiber (ϕ ⟦ c ⟧) x} {b' : fiber (ϕ ⟦ c ⟧) x'}
→ fst a' ≡ fst b'
→ PathP (λ i → fiber (ϕ ⟦ c ⟧) (px i)) a' b'
fibersEqIfRepsEqNatTrans ϕ {c} {x} {x'} {px} {a , fiba} {b , fibb} p
= fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧) p
K-ob : (s : SliceCat .ob) → (PresheafCategory (∫ᴾ F) ℓS .ob)
K-ob (sliceob {A} ϕ) .F-ob (c , x)
= (fiber (ϕ ⟦ c ⟧) x)
, isOfHLevelΣ 2 (snd (A ⟅ c ⟆)) λ _ → isSet→isGroupoid (snd (F ⟅ c ⟆)) _ _
K-ob (sliceob {A} ϕ) .F-hom {d , y} {c , x} (h , com) (b , eq)
= ((A ⟪ h ⟫) b)
, ((ϕ ⟦ c ⟧) ((A ⟪ h ⟫) b)
≡[ i ]⟨ (ϕ .N-hom h) i b ⟩
(F ⟪ h ⟫) ((ϕ ⟦ d ⟧) b)
≡[ i ]⟨ (F ⟪ h ⟫) (eq i) ⟩
(F ⟪ h ⟫) y
≡⟨ com ⟩
x
∎)
K-ob (sliceob {A} ϕ) .F-id {x = (c , x)}
= funExt λ { (a , fibp)
→ fibersEqIfRepsEqNatTrans ϕ (λ i → A .F-id i a) }
K-ob (sliceob {A} ϕ) .F-seq {x = (c , x)} {(d , y)} {(e , z)} (f' , eq1) (g' , eq2)
= funExt λ { ( a , fibp )
→ fibersEqIfRepsEqNatTrans ϕ (λ i → (A .F-seq f' g') i a) }
K-hom : {sA sB : SliceCat .ob}
→ (ε : SliceCat [ sA , sB ])
→ (K-ob sA) ⇒ (K-ob sB)
K-hom {sA = s1@(sliceob {A} ϕ)} {s2@(sliceob {B} ψ)} (slicehom ε com) = natTrans η-ob (λ h → funExt (η-hom h))
where
P = K-ob s1
Q = K-ob s2
η-ob : (el : (∫ᴾ F) .ob) → (fst (P ⟅ el ⟆) → fst (Q ⟅ el ⟆) )
η-ob (c , x) (a , ϕa≡x) = ((ε ⟦ c ⟧) a) , εψ≡ϕ ∙ ϕa≡x
where
εψ≡ϕ : (ψ ⟦ c ⟧) ((ε ⟦ c ⟧) a) ≡ (ϕ ⟦ c ⟧) a
εψ≡ϕ i = ((com i) ⟦ c ⟧) a
η-hom : ∀ {el1 el2} (h : (∫ᴾ F) [ el1 , el2 ]) (ae : fst (P ⟅ el2 ⟆)) → η-ob el1 ((P ⟪ h ⟫) ae) ≡ (Q ⟪ h ⟫) (η-ob el2 ae)
η-hom {el1 = (c , x)} {d , y} (h , eqh) (a , eqa)
= fibersEqIfRepsEqNatTrans ψ (λ i → ε .N-hom h i a)
K : Functor SliceCat (PresheafCategory (∫ᴾ F) ℓS)
K .F-ob = K-ob
K .F-hom = K-hom
K .F-id = makeNatTransPath
(funExt λ cx@(c , x)
→ funExt λ aeq@(a , eq)
→ fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} _ refl)
K .F-seq (slicehom α eqa) (slicehom β eqb)
= makeNatTransPath
(funExt λ cx@(c , x)
→ funExt λ aeq@(a , eq)
→ fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} _ refl)
L-ob : (P : PresheafCategory (∫ᴾ F) ℓS .ob)
→ SliceCat .ob
L-ob P = sliceob {S-ob = L-ob-ob} L-ob-hom
where
LF-ob : (c : C .ob) → (SET _) .ob
LF-ob c = (Σ[ x ∈ fst (F ⟅ c ⟆) ] fst (P ⟅ c , x ⟆)) , isSetΣ (snd (F ⟅ c ⟆)) (λ x → snd (P ⟅ c , x ⟆))
LF-hom : ∀ {x y}
→ (f : C [ y , x ])
→ (SET _) [ LF-ob x , LF-ob y ]
LF-hom {x = c} {d} f (x , a) = ((F ⟪ f ⟫) x) , (P ⟪ f , refl ⟫) a
L-ob-ob : Functor (C ^op) (SET _)
L-ob-ob .F-ob = LF-ob
L-ob-ob .F-hom = LF-hom
L-ob-ob .F-id {x = c}
= funExt idFunExt
where
idFunExt : ∀ (un : fst (LF-ob c))
→ (LF-hom (C .id) un) ≡ un
idFunExt (x , X) = ΣPathP (leftEq , rightEq)
where
leftEq : (F ⟪ C .id ⟫) x ≡ x
leftEq i = F .F-id i x
rightEq : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
((P ⟪ C .id , refl ⟫) X) X
rightEq = left ▷ right
where
∫id = C .id , funExt⁻ (F .F-id) x
right : (P ⟪ ∫id ⟫) X ≡ X
right i = P .F-id i X
left : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
((P ⟪ C .id , refl ⟫) X)
((P ⟪ ∫id ⟫) X)
left i = (P ⟪ ∫ᴾhomEq {F = F} (C .id , refl) ∫id (λ i → (c , leftEq i)) refl refl i ⟫) X
L-ob-ob .F-seq {x = c} {d} {e} f g
= funExt seqFunEq
where
seqFunEq : ∀ (un : fst (LF-ob c))
→ (LF-hom (g ⋆⟨ C ⟩ f) un) ≡ (LF-hom g) (LF-hom f un)
seqFunEq un@(x , X) = ΣPathP (leftEq , rightEq)
where
leftEq : (F ⟪ g ⋆⟨ C ⟩ f ⟫) x ≡ (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
leftEq i = F .F-seq f g i x
rightEq : PathP (λ i → fst (P ⟅ e , leftEq i ⟆))
((P ⟪ g ⋆⟨ C ⟩ f , refl ⟫) X)
((P ⟪ g , refl ⟫) ((P ⟪ f , refl ⟫) X))
rightEq = left ▷ right
where
right : (P ⟪ (g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl) ⟫) X ≡ (P ⟪ g , refl ⟫) ((P ⟪ f , refl ⟫) X)
right i = P .F-seq (f , refl) (g , refl) i X
left : PathP (λ i → fst (P ⟅ e , leftEq i ⟆))
((P ⟪ g ⋆⟨ C ⟩ f , refl ⟫) X)
((P ⟪ (g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl) ⟫) X)
left i = (P ⟪ ∫ᴾhomEq {F = F} (g ⋆⟨ C ⟩ f , refl) ((g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl)) (λ i → (e , leftEq i)) refl refl i ⟫) X
L-ob-hom : L-ob-ob ⇒ F
L-ob-hom .N-ob c (x , _) = x
L-ob-hom .N-hom f = funExt λ (x , _) → refl
L-hom : ∀ {P Q} → PresheafCategory (∫ᴾ F) ℓS [ P , Q ] →
SliceCat [ L-ob P , L-ob Q ]
L-hom {P} {Q} η = slicehom arr com
where
A = S-ob (L-ob P)
ϕ = S-arr (L-ob P)
B = S-ob (L-ob Q)
ψ = S-arr (L-ob Q)
arr : A ⇒ B
arr .N-ob c (x , X) = x , ((η ⟦ c , x ⟧) X)
arr .N-hom {c} {d} f = funExt natu
where
natuType : fst (A ⟅ c ⟆) → Type _
natuType xX@(x , X) = ((F ⟪ f ⟫) x , (η ⟦ d , (F ⟪ f ⟫) x ⟧) ((P ⟪ f , refl ⟫) X)) ≡ ((F ⟪ f ⟫) x , (Q ⟪ f , refl ⟫) ((η ⟦ c , x ⟧) X))
natu : ∀ (xX : fst (A ⟅ c ⟆)) → natuType xX
natu (x , X) = ΣPathP (refl , λ i → (η .N-hom (f , refl) i) X)
com : arr ⋆⟨ PresheafCategory C ℓS ⟩ ψ ≡ ϕ
com = makeNatTransPath (funExt comFunExt)
where
comFunExt : ∀ (c : C .ob)
→ (arr ●ᵛ ψ) ⟦ c ⟧ ≡ ϕ ⟦ c ⟧
comFunExt c = funExt λ x → refl
L : Functor (PresheafCategory (∫ᴾ F) ℓS) SliceCat
L .F-ob = L-ob
L .F-hom = L-hom
L .F-id {cx} = SliceHom-≡-intro' (makeNatTransPath (funExt λ c → refl))
L .F-seq {cx} {dy} P Q = SliceHom-≡-intro' (makeNatTransPath (funExt λ c → refl))
module _ where
open Iso
typeSectionIso : ∀ {A B : Type ℓS} {isSetB : isSet B} → (ϕ : A → B)
→ Iso A (Σ[ b ∈ B ] fiber ϕ b)
typeSectionIso ϕ .fun a = (ϕ a) , (a , refl)
typeSectionIso ϕ .inv (b , (a , eq)) = a
typeSectionIso {isSetB = isSetB} ϕ .rightInv (b , (a , eq))
= ΣPathP (eq
, ΣPathP (refl
, isOfHLevel→isOfHLevelDep 1 (λ b' → isSetB _ _) refl eq eq))
typeSectionIso ϕ .leftInv a = refl
ηTrans : 𝟙⟨ SliceCat ⟩ ⇒ (L ∘F K)
ηTrans .N-ob sob@(sliceob {A} ϕ) = slicehom A⇒LK comm
where
LKA = S-ob (L ⟅ K ⟅ sob ⟆ ⟆)
ψ = S-arr (L ⟅ K ⟅ sob ⟆ ⟆)
A⇒LK : A ⇒ LKA
A⇒LK .N-ob c = typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧) .fun
A⇒LK .N-hom {c} {d} f = funExt homFunExt
where
homFunExt : (x : fst (A ⟅ c ⟆))
→ (((ϕ ⟦ d ⟧) ((A ⟪ f ⟫) x)) , ((A ⟪ f ⟫) x , refl)) ≡ ((F ⟪ f ⟫) ((ϕ ⟦ c ⟧) x) , (A ⟪ f ⟫) x , _)
homFunExt x = ΣPathP ((λ i → (ϕ .N-hom f i) x) , fibersEqIfRepsEqNatTrans ϕ refl)
comm : (A⇒LK) ●ᵛ ψ ≡ ϕ
comm = makeNatTransPath (funExt λ x → refl)
ηTrans .N-hom {sliceob {A} α} {sliceob {B} β} (slicehom ϕ eq)
= SliceHom-≡-intro' (makeNatTransPath (funExt (λ c → funExt λ a → natFunExt c a)))
where
natFunExt : ∀ (c : C .ob) (a : fst (A ⟅ c ⟆))
→ ((β ⟦ c ⟧) ((ϕ ⟦ c ⟧) a) , (ϕ ⟦ c ⟧) a , _) ≡ ((α ⟦ c ⟧) a , (ϕ ⟦ c ⟧) a , _)
natFunExt c a = ΣPathP ((λ i → ((eq i) ⟦ c ⟧) a) , fibersEqIfRepsEqNatTrans β refl)
ηIso : ∀ (sob : SliceCat .ob)
→ isIsoC SliceCat (ηTrans ⟦ sob ⟧)
ηIso sob@(sliceob ϕ) = sliceIso _ _ (FUNCTORIso _ _ _ isIsoCf)
where
isIsoCf : ∀ (c : C .ob)
→ isIsoC _ (ηTrans .N-ob sob .S-hom ⟦ c ⟧)
isIsoCf c = Morphism.CatIso→isIso (Iso→CatIso (typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧)))
module _ where
open Iso
typeFiberIso : ∀ {ℓ ℓ'} {A : Type ℓ} {isSetA : isSet A} {x} (B : A → Type ℓ')
→ Iso (B x) (fiber {A = Σ[ a ∈ A ] B a} (λ (x , _) → x) x)
typeFiberIso {x = x} _ .fun b = (x , b) , refl
typeFiberIso _ .inv ((a , b) , eq) = subst _ eq b
typeFiberIso {isSetA = isSetA} {x = x} B .rightInv ((a , b) , eq)
= fibersEqIfRepsEq {isSetB = isSetA} (λ (x , _) → x) (ΣPathP (sym eq , symP (transport-filler (λ i → B (eq i)) b)))
typeFiberIso {x = x} _ .leftInv b = sym (transport-filler refl b)
εTrans : (K ∘F L) ⇒ 𝟙⟨ PresheafCategory (∫ᴾ F) ℓS ⟩
εTrans .N-ob P = natTrans γ-ob (λ f → funExt (λ a → γ-homFunExt f a))
where
KLP = K ⟅ L ⟅ P ⟆ ⟆
γ-ob : (el : (∫ᴾ F) .ob)
→ (fst (KLP ⟅ el ⟆) → fst (P ⟅ el ⟆) )
γ-ob el@(c , _) = typeFiberIso {isSetA = snd (F ⟅ c ⟆)} (λ x → fst (P ⟅ c , x ⟆)) .inv
γ-homFunExt : ∀ {el2 el1} → (f' : (∫ᴾ F) [ el2 , el1 ])
→ (∀ (a : fst (KLP ⟅ el1 ⟆)) → γ-ob el2 ((KLP ⟪ f' ⟫) a) ≡ (P ⟪ f' ⟫) (γ-ob el1 a))
γ-homFunExt {d , y} {c , x} f'@(f , comm) a@((x' , X') , eq) i
= comp (λ j → fst (P ⟅ d , eq' j ⟆)) (λ j → λ { (i = i0) → left j
; (i = i1) → right j }) ((P ⟪ f , refl ⟫) X')
where
eq' = snd ((KLP ⟪ f' ⟫) a)
right : PathP (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X') ((P ⟪ f , comm ⟫) (subst _ eq X'))
right i = (P ⟪ f , refl≡comm i ⟫) (X'≡subst i)
where
refl≡comm : PathP (λ i → (F ⟪ f ⟫) (eq i) ≡ (eq' i)) refl comm
refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) ((F ⟪ f ⟫) w) v) refl comm λ i → (eq' i , eq i)
X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst (λ v → fst (P ⟅ c , v ⟆)) eq X')
X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X'
left : PathP (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X') (subst (λ v → fst (P ⟅ d , v ⟆)) eq' ((P ⟪ f , refl ⟫) X'))
left = transport-filler (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X')
εTrans .N-hom {P} {Q} α = makeNatTransPath (funExt λ cx → funExt λ xX' → ε-homFunExt cx xX')
where
KLP = K ⟅ L ⟅ P ⟆ ⟆
ε-homFunExt : ∀ (cx@(c , x) : (∫ᴾ F) .ob) (xX'@((x' , X') , eq) : fst (KLP ⟅ cx ⟆))
→ subst (λ v → fst (Q ⟅ c , v ⟆)) (snd ((K ⟪ L ⟪ α ⟫ ⟫ ⟦ cx ⟧) xX')) ((α ⟦ c , x' ⟧) X')
≡ (α ⟦ c , x ⟧) (subst _ eq X')
ε-homFunExt cx@(c , x) xX'@((x' , X') , eq) i
= comp (λ j → fst (Q ⟅ c , eq j ⟆)) (λ j → λ { (i = i0) → left j
; (i = i1) → right j }) ((α ⟦ c , x' ⟧) X')
where
eq' : x' ≡ x
eq' = snd ((K ⟪ L ⟪ α ⟫ ⟫ ⟦ cx ⟧) xX')
right : PathP (λ i → fst (Q ⟅ c , eq i ⟆)) ((α ⟦ c , x' ⟧) X') ((α ⟦ c , x ⟧) (subst _ eq X'))
right i = (α ⟦ c , eq i ⟧) (X'≡subst i)
where
X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst (λ v → fst (P ⟅ c , v ⟆)) eq X')
X'≡subst = transport-filler _ _
leftTy : (x' ≡ x) → Type _
leftTy eq* = PathP (λ i → fst (Q ⟅ c , eq* i ⟆)) ((α ⟦ c , x' ⟧) X') (subst (λ v → fst (Q ⟅ c , v ⟆)) eq' ((α ⟦ c , x' ⟧) X'))
left : leftTy eq
left = subst
(λ eq* → leftTy eq*)
eq'≡eq
(transport-filler _ _)
where
eq'≡eq : eq' ≡ eq
eq'≡eq = snd (F ⟅ c ⟆) _ _ eq' eq
εIso : ∀ (P : PresheafCategory (∫ᴾ F) ℓS .ob)
→ isIsoC (PresheafCategory (∫ᴾ F) ℓS) (εTrans ⟦ P ⟧)
εIso P = FUNCTORIso _ _ _ isIsoC'
where
isIsoC' : ∀ (cx : (∫ᴾ F) .ob)
→ isIsoC (SET _) ((εTrans ⟦ P ⟧) ⟦ cx ⟧)
isIsoC' cx@(c , _) = Morphism.CatIso→isIso (Iso→CatIso (invIso (typeFiberIso {isSetA = snd (F ⟅ c ⟆)} _)))
preshSlice≃preshElem : SliceCat ≃ᶜ PresheafCategory (∫ᴾ F) ℓS
preshSlice≃preshElem .func = K
preshSlice≃preshElem .isEquiv = ∣ w-inv ∣₁
where
w-inv : WeakInverse K
w-inv .invFunc = L
w-inv .η .trans = ηTrans
w-inv .η .nIso = ηIso
w-inv .ε .trans = εTrans
w-inv .ε .nIso = εIso
PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) (Q : Presheaf C ℓS') → Type _
PshIso {ℓS = ℓS}{ℓS' = ℓS'} C P Q =
NatIso (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P) (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q)