diff --git a/Cubical.Categories.Constructions.Elements.html b/Cubical.Categories.Constructions.Elements.html index a31f16a788..49a04d9d4a 100644 --- a/Cubical.Categories.Constructions.Elements.html +++ b/Cubical.Categories.Constructions.Elements.html @@ -3,106 +3,112 @@ -- The Category of Elements -open import Cubical.Categories.Category - -module Cubical.Categories.Constructions.Elements where - -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Functor -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma - -import Cubical.Categories.Morphism as Morphism -import Cubical.Categories.Constructions.Slice.Base as Slice - --- some issues --- * always need to specify objects during composition because can't infer isSet -open Category -open Functor - -module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where - getIsSet : ∀ {ℓS} {C : Category ℓ ℓ'} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆)) - getIsSet F c = snd (F ⟅ c ⟆) - - Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS) - Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆) - - infix 50 ∫_ - ∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS) - -- objects are (c , x) pairs where c ∈ C and x ∈ F c - (∫ F) .ob = Element F - -- morphisms are f : c → c' which take x to x' - (∫ F) .Hom[_,_] (c , x) (c' , x') = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x - (∫ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl) - (∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q) - = (f ⋆⟨ C ⟩ g) , (x₂ - ≡⟨ q ⟩ - (F ⟪ g ⟫) x₁ -- basically expanding out function composition - ≡⟨ cong (F ⟪ g ⟫) p ⟩ - (F ⟪ g ⟫) ((F ⟪ f ⟫) x) - ≡⟨ funExt⁻ (sym (F .F-seq _ _)) _ ⟩ - (F ⟪ f ⋆⟨ C ⟩ g ⟫) x - ∎) - (∫ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i - = (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdL i - where - isS = getIsSet F c - isS' = getIsSet F c' - cIdL = C .⋆IdL f - - -- proof from composition with id - p' : x' ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x - p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f') - (∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i - = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdR i - where - cIdR = C .⋆IdR f - isS' = getIsSet F c' - - p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x - p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id)) - (∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i - = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ x₃ ((F ⟪ a ⟫) x)) p1 p2 cAssoc i - where - cAssoc = C .⋆Assoc f g h - isS₃ = getIsSet F c₃ - - p1 : x₃ ≡ (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x - p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h') - - p2 : x₃ ≡ (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x - p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h')) - (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _ - - ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C - F-ob (ForgetElements F) = fst - F-hom (ForgetElements F) = fst - F-id (ForgetElements F) = refl - F-seq (ForgetElements F) _ _ = refl - -module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where - open Covariant {C = C ^op} - - -- same thing but for presheaves - ∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS) - ∫ᴾ F = (∫ F) ^op - - Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS) - Elementᴾ F = (∫ᴾ F) .ob - - -- helpful results - - module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where - - -- morphisms are equal as long as the morphisms in C are equal - ∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ]) - → (p : o1 ≡ o1') (q : o2 ≡ o2') - → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g)) - → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g - ∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _) - - ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ]) - → fst f ≡ fst g → f ≡ g - ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Path +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category +import Cubical.Categories.Constructions.Slice.Base as Slice +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Isomorphism +import Cubical.Categories.Morphism as Morphism + + + +module Cubical.Categories.Constructions.Elements where + +-- some issues +-- * always need to specify objects during composition because can't infer isSet +open Category +open Functor + +module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where + getIsSet : ∀ {ℓS} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆)) + getIsSet F c = snd (F ⟅ c ⟆) + + Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS) + Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆) + + infix 50 ∫_ + ∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS) + -- objects are (c , x) pairs where c ∈ C and x ∈ F c + (∫ F) .ob = Element F + -- morphisms are f : c → c' which take x to x' + (∫ F) .Hom[_,_] (c , x) (c' , x') = fiber (λ (f : C [ c , c' ]) → (F ⟪ f ⟫) x) x' + (∫ F) .id {x = (c , x)} = C .id , funExt⁻ (F .F-id) x + (∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q) + = (f ⋆⟨ C ⟩ g) , ((F ⟪ f ⋆⟨ C ⟩ g ⟫) x + ≡⟨ funExt⁻ (F .F-seq _ _) _ ⟩ + (F ⟪ g ⟫) ((F ⟪ f ⟫) x) + ≡⟨ cong (F ⟪ g ⟫) p ⟩ + (F ⟪ g ⟫) x₁ + ≡⟨ q ⟩ + x₂ + ∎) + (∫ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i + = (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdL i + where + isS = getIsSet F c + isS' = getIsSet F c' + cIdL = C .⋆IdL f + + -- proof from composition with id + p' : (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x ≡ x' + p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f') + (∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i + = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdR i + where + cIdR = C .⋆IdR f + isS' = getIsSet F c' + + p' : (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x ≡ x' + p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id)) + (∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i + = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ ((F ⟪ a ⟫) x) x₃) p1 p2 cAssoc i + where + cAssoc = C .⋆Assoc f g h + isS₃ = getIsSet F c₃ + + p1 : (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x ≡ x₃ + p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h') + + p2 : (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x ≡ x₃ + p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h')) + (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _ + + ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C + F-ob (ForgetElements F) = fst + F-hom (ForgetElements F) = fst + F-id (ForgetElements F) = refl + F-seq (ForgetElements F) _ _ = refl + +module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where + open Covariant {C = C ^op} + + -- same thing but for presheaves + ∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS) + ∫ᴾ F = (∫ F) ^op + + Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS) + Elementᴾ F = (∫ᴾ F) .ob + + -- helpful results + + module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where + + -- morphisms are equal as long as the morphisms in C are equal + ∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ]) + → (p : o1 ≡ o1') (q : o2 ≡ o2') + → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g)) + → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g + ∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _) + + ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ]) + → fst f ≡ fst g → f ≡ g + ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p \ No newline at end of file diff --git a/Cubical.Categories.Constructions.Slice.Properties.html b/Cubical.Categories.Constructions.Slice.Properties.html index 8ece224da5..3646b9dc93 100644 --- a/Cubical.Categories.Constructions.Slice.Properties.html +++ b/Cubical.Categories.Constructions.Slice.Properties.html @@ -24,43 +24,43 @@ (c : C .ob) where -open Elements.Contravariant {C = C} +open Elements.Contravariant {C = C} open _≃ᶜ_ open Functor open WeakInverse -slice→el : Functor (SliceCat C c) (∫ᴾ (C [-, c ])) +slice→el : Functor (SliceCat C c) (∫ᴾ (C [-, c ])) slice→el .F-ob s = s .S-ob , s .S-arr -slice→el .F-hom f = f .S-hom , sym (f .S-comm) -slice→el .F-id = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)) -slice→el .F-seq _ _ = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)) +slice→el .F-hom f = f .S-hom , f .S-comm +slice→el .F-id = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)) +slice→el .F-seq _ _ = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)) -el→slice : Functor (∫ᴾ (C [-, c ])) (SliceCat C c) -el→slice .F-ob (_ , s) = sliceob s -el→slice .F-hom (f , comm) = slicehom f (sym comm) -el→slice .F-id = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _) -el→slice .F-seq _ _ = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _) +el→slice : Functor (∫ᴾ (C [-, c ])) (SliceCat C c) +el→slice .F-ob (_ , s) = sliceob s +el→slice .F-hom (f , comm) = slicehom f comm +el→slice .F-id = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _) +el→slice .F-seq _ _ = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _) -open NatTrans -open NatIso +open NatTrans +open NatIso -sliceIsElementsOfRep : SliceCat C c ≃ᶜ (∫ᴾ (C [-, c ])) -sliceIsElementsOfRep .func = slice→el -sliceIsElementsOfRep .isEquiv = ∣ w-inv ∣₁ - where - w-inv : WeakInverse slice→el - w-inv .invFunc = el→slice - w-inv .η .trans .N-ob s = SliceCat C c .id - w-inv .η .trans .N-hom f = (SliceCat C c .⋆IdR f) - ∙ sym (SliceCat C c .⋆IdL f) - w-inv .η .nIso x = isiso (SliceCat C c .id) - (SliceCat C c .⋆IdR _) - (SliceCat C c .⋆IdR _) - w-inv .ε .trans .N-ob s = (∫ᴾ (C [-, c ])) .id - w-inv .ε .trans .N-hom f = ((∫ᴾ (C [-, c ])) .⋆IdR f) - ∙ sym ((∫ᴾ (C [-, c ])) .⋆IdL f) - w-inv .ε .nIso x = isiso ((∫ᴾ (C [-, c ])) .id) - ((∫ᴾ (C [-, c ])) .⋆IdR _) - ((∫ᴾ (C [-, c ])) .⋆IdR _) +sliceIsElementsOfRep : SliceCat C c ≃ᶜ (∫ᴾ (C [-, c ])) +sliceIsElementsOfRep .func = slice→el +sliceIsElementsOfRep .isEquiv = ∣ w-inv ∣₁ + where + w-inv : WeakInverse slice→el + w-inv .invFunc = el→slice + w-inv .η .trans .N-ob s = SliceCat C c .id + w-inv .η .trans .N-hom f = (SliceCat C c .⋆IdR f) + ∙ sym (SliceCat C c .⋆IdL f) + w-inv .η .nIso x = isiso (SliceCat C c .id) + (SliceCat C c .⋆IdR _) + (SliceCat C c .⋆IdR _) + w-inv .ε .trans .N-ob s = (∫ᴾ (C [-, c ])) .id + w-inv .ε .trans .N-hom f = ((∫ᴾ (C [-, c ])) .⋆IdR f) + ∙ sym ((∫ᴾ (C [-, c ])) .⋆IdL f) + w-inv .ε .nIso x = isiso ((∫ᴾ (C [-, c ])) .id) + ((∫ᴾ (C [-, c ])) .⋆IdR _) + ((∫ᴾ (C [-, c ])) .⋆IdR _) \ No newline at end of file diff --git a/Cubical.Categories.Constructions.TwistedArrow.html b/Cubical.Categories.Constructions.TwistedArrow.html index 57b2a1db95..149a269ea7 100644 --- a/Cubical.Categories.Constructions.TwistedArrow.html +++ b/Cubical.Categories.Constructions.TwistedArrow.html @@ -10,7 +10,7 @@ open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor.Base open import Cubical.Categories.Constructions.Elements -open Covariant +open Covariant open import Cubical.Categories.Functors.HomFunctor open import Cubical.Categories.Constructions.BinProduct @@ -18,14 +18,14 @@ variable ℓ ℓ' : Level TwistedArrowCategory : (C : Category ℓ ℓ') → Category (ℓ-max ℓ ℓ') ℓ' -TwistedArrowCategory C = ∫ HomFunctor C +TwistedArrowCategory C = ∫ HomFunctor C TwistedEnds : (C : Category ℓ ℓ') → Functor (TwistedArrowCategory C) (C ^op ×C C) -TwistedEnds C = ForgetElements (HomFunctor C) +TwistedEnds C = ForgetElements (HomFunctor C) TwistedDom : (C : Category ℓ ℓ') → Functor ((TwistedArrowCategory C) ^op) C -TwistedDom C = ((Fst (C ^op) C) ^opF) ∘F (ForgetElements (HomFunctor C) ^opF) +TwistedDom C = ((Fst (C ^op) C) ^opF) ∘F (ForgetElements (HomFunctor C) ^opF) TwistedCod : (C : Category ℓ ℓ') → Functor (TwistedArrowCategory C) C -TwistedCod C = (Snd (C ^op) C) ∘F ForgetElements (HomFunctor C) +TwistedCod C = (Snd (C ^op) C) ∘F ForgetElements (HomFunctor C) \ No newline at end of file diff --git a/Cubical.Categories.Presheaf.Morphism.html b/Cubical.Categories.Presheaf.Morphism.html index c6395fa72f..f539be7f1d 100644 --- a/Cubical.Categories.Presheaf.Morphism.html +++ b/Cubical.Categories.Presheaf.Morphism.html @@ -38,7 +38,7 @@ ℓc ℓc' ℓd ℓd' ℓp ℓq : Level open Category -open Contravariant +open Contravariant open Functor open NatTrans open UniversalElement @@ -54,45 +54,46 @@ module _ (h : PshHom) where -- This should define a functor on the category of elements - pushElt : Elementᴾ {C = C} P → Elementᴾ {C = D} Q + pushElt : Elementᴾ {C = C} P → Elementᴾ {C = D} Q pushElt (A , η) = (F ⟅ A ⟆) , (h .N-ob A (lift η) .lower) - pushEltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ]) + pushEltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ]) → (pushElt η .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f) ≡ pushElt (B , η .snd ∘ᴾ⟨ C , P ⟩ f) .snd pushEltNat η f i = h .N-hom f (~ i) (lift (η .snd)) .lower - pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q) + pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q) pushEltF .F-ob = pushElt - pushEltF .F-hom {x}{y} (f , commutes) = F .F-hom f , sym ( - pushElt _ .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f - ≡⟨ pushEltNat y f ⟩ - pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd - ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , (sym commutes))) ⟩ - pushElt x .snd ∎) - pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id) - pushEltF .F-seq f g = - Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst)) - - preservesRepresentation : ∀ (η : UniversalElement C P) - → Type (ℓ-max (ℓ-max ℓd ℓd') ℓq) - preservesRepresentation η = isUniversal D Q (η' .fst) (η' .snd) - where η' = pushElt (η .vertex , η .element) - - preservesRepresentations : Type _ - preservesRepresentations = ∀ η → preservesRepresentation η - - -- If C and D are univalent then this follows by representability - -- being a Prop. But even in non-univalent categories it follows - -- by uniqueness of representables up to unique isomorphism - preservesAnyRepresentation→preservesAllRepresentations : - ∀ η → preservesRepresentation η → preservesRepresentations - preservesAnyRepresentation→preservesAllRepresentations η preserves-η η' = - isTerminalToIsUniversal D Q - (preserveAnyTerminal→PreservesTerminals (∫ᴾ_ {C = C} P) - (∫ᴾ_ {C = D} Q) - pushEltF - (universalElementToTerminalElement C P η) - (isUniversalToIsTerminal D Q _ _ preserves-η) - (universalElementToTerminalElement C P η')) + pushEltF .F-hom {x}{y} (f , commutes) .fst = F .F-hom f + pushEltF .F-hom {x}{y} (f , commutes) .snd = + pushElt _ .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f + ≡⟨ pushEltNat y f ⟩ + pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd + ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , commutes)) ⟩ + pushElt x .snd ∎ + pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id) + pushEltF .F-seq f g = + Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst)) + + preservesRepresentation : ∀ (η : UniversalElement C P) + → Type (ℓ-max (ℓ-max ℓd ℓd') ℓq) + preservesRepresentation η = isUniversal D Q (η' .fst) (η' .snd) + where η' = pushElt (η .vertex , η .element) + + preservesRepresentations : Type _ + preservesRepresentations = ∀ η → preservesRepresentation η + + -- If C and D are univalent then this follows by representability + -- being a Prop. But even in non-univalent categories it follows + -- by uniqueness of representables up to unique isomorphism + preservesAnyRepresentation→preservesAllRepresentations : + ∀ η → preservesRepresentation η → preservesRepresentations + preservesAnyRepresentation→preservesAllRepresentations η preserves-η η' = + isTerminalToIsUniversal D Q + (preserveAnyTerminal→PreservesTerminals (∫ᴾ_ {C = C} P) + (∫ᴾ_ {C = D} Q) + pushEltF + (universalElementToTerminalElement C P η) + (isUniversalToIsTerminal D Q _ _ preserves-η) + (universalElementToTerminalElement C P η')) \ No newline at end of file diff --git a/Cubical.Categories.Presheaf.Properties.html b/Cubical.Categories.Presheaf.Properties.html index e6f210687b..24f9ef9777 100644 --- a/Cubical.Categories.Presheaf.Properties.html +++ b/Cubical.Categories.Presheaf.Properties.html @@ -40,7 +40,7 @@ open NatTrans open NatIso open Slice (PresheafCategory C ℓS) F - open Elements.Contravariant {C = C} + open Elements.Contravariant {C = C} open Fibration.ForSets @@ -56,7 +56,7 @@ -- ======================================== -- action on (slice) objects - K-ob : (s : SliceCat .ob) → (PresheafCategory (∫ᴾ F) ℓS .ob) + K-ob : (s : SliceCat .ob) → (PresheafCategory (∫ᴾ F) ℓS .ob) -- we take (c , x) to the fiber in A of ϕ over x K-ob (sliceob {A} ϕ) .F-ob (c , x) = (fiber (ϕ ⟦ c ⟧) x) @@ -69,333 +69,333 @@ (F ⟪ h ⟫) ((ϕ ⟦ d ⟧) b) ≡[ i ]⟨ (F ⟪ h ⟫) (eq i) ⟩ (F ⟪ h ⟫) y - ≡⟨ sym com ⟩ - x - ∎) - -- functoriality follows from functoriality of A - 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) } - - - -- action on morphisms (in this case, natural transformation) - 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 - - -- just apply the natural transformation (ε) we're given - -- this ensures that we stay in the fiber over x due to the commutativity given by slicenesss - η-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 : PresheafCategory → Slice - -- ======================================== - - -- action on objects (presheaves) - L-ob : (P : PresheafCategory (∫ᴾ F) ℓS .ob) - → SliceCat .ob - L-ob P = sliceob {S-ob = L-ob-ob} L-ob-hom - where - -- sends c to the disjoint union of all the images under P - 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 ⟆)) - - -- defines a function piecewise over the fibers by applying P - 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 - -- the id morphism in (∫ᴾ F) - ∫id = C .id , sym (funExt⁻ (F .F-id) x ∙ refl) - - -- functoriality of P gives us close to what we want - right : (P ⟪ ∫id ⟫) X ≡ X - right i = P .F-id i X - - -- but need to do more work to show that (C .id , refl) ≡ ∫id - 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 - -- the left component is comparing the action of F on x - -- equality follows from functoriality of F - -- leftEq : fst (LF-hom (g ⋆⟨ C ⟩ f) un) ≡ fst ((LF-hom g) (LF-hom f un)) - leftEq : (F ⟪ g ⋆⟨ C ⟩ f ⟫) x ≡ (F ⟪ g ⟫) ((F ⟪ f ⟫) x) - leftEq i = F .F-seq f g i x - - -- on the right, equality also follows from functoriality of P - -- but it's more complicated because of heterogeneity - -- since leftEq is not a definitional equality - 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 - -- functoriality of P only gets us to this weird composition on the left - 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 - - -- so we need to show that this composition is actually equal to the one we want - 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 - - -- action on morphisms (aka natural transformations between presheaves) - -- is essentially the identity (plus equality proofs for naturality and slice commutativity) - 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)) - - -- ======================================== - -- η : 𝟙 ≅ LK - -- ======================================== - - module _ where - open Iso - -- the iso we need - -- a type is isomorphic to the disjoint union of all its fibers - 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 - - -- the natural transformation - -- just applies typeSectionIso - η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) - - -- isomorphism follows from typeSectionIso - η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 ⟧))) - - - -- ======================================== - -- ε : KL ≅ 𝟙 - -- ======================================== - - module _ where - open Iso - -- the iso we deserve - -- says that a type family at x is isomorphic to the fiber over x of that type family packaged up - 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) - - -- the natural isomorphism - -- applies typeFiberIso (inv) - ε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 - - -- naturality - -- the annoying part is all the substs - γ-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 - -- fiber equality proof that we get from an application of KLP - eq' = snd ((KLP ⟪ f' ⟫) a) - - -- top right of the commuting diagram - -- "remove" the subst from the inside - 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 → (eq' i) ≡ (F ⟪ f ⟫) (eq i)) refl comm - refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) v ((F ⟪ f ⟫) w)) refl comm λ i → (eq' i , eq i) - - X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X') - X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X' - - -- bottom left of the commuting diagram - -- "remove" the subst from the outside - 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 ⟆ ⟆ - - -- naturality of the above construction applies a similar argument as in `γ-homFunExt` - ε-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 - -- this is exactly the same as the one from before, can refactor? - X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X') - X'≡subst = transport-filler _ _ - - -- extracted out type since need to use in in 'left' body as well - 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 ⟆)} _))) - - - -- putting it all together - - 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 - --- Isomorphism between presheaves of different levels -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) + ≡⟨ com ⟩ + x + ∎) + -- functoriality follows from functoriality of A + 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) } + + + -- action on morphisms (in this case, natural transformation) + 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 + + -- just apply the natural transformation (ε) we're given + -- this ensures that we stay in the fiber over x due to the commutativity given by slicenesss + η-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 : PresheafCategory → Slice + -- ======================================== + + -- action on objects (presheaves) + L-ob : (P : PresheafCategory (∫ᴾ F) ℓS .ob) + → SliceCat .ob + L-ob P = sliceob {S-ob = L-ob-ob} L-ob-hom + where + -- sends c to the disjoint union of all the images under P + 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 ⟆)) + + -- defines a function piecewise over the fibers by applying P + 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 + -- the id morphism in (∫ᴾ F) + ∫id = C .id , funExt⁻ (F .F-id) x + + -- functoriality of P gives us close to what we want + right : (P ⟪ ∫id ⟫) X ≡ X + right i = P .F-id i X + + -- but need to do more work to show that (C .id , refl) ≡ ∫id + 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 + -- the left component is comparing the action of F on x + -- equality follows from functoriality of F + -- leftEq : fst (LF-hom (g ⋆⟨ C ⟩ f) un) ≡ fst ((LF-hom g) (LF-hom f un)) + leftEq : (F ⟪ g ⋆⟨ C ⟩ f ⟫) x ≡ (F ⟪ g ⟫) ((F ⟪ f ⟫) x) + leftEq i = F .F-seq f g i x + + -- on the right, equality also follows from functoriality of P + -- but it's more complicated because of heterogeneity + -- since leftEq is not a definitional equality + 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 + -- functoriality of P only gets us to this weird composition on the left + 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 + + -- so we need to show that this composition is actually equal to the one we want + 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 + + -- action on morphisms (aka natural transformations between presheaves) + -- is essentially the identity (plus equality proofs for naturality and slice commutativity) + 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)) + + -- ======================================== + -- η : 𝟙 ≅ LK + -- ======================================== + + module _ where + open Iso + -- the iso we need + -- a type is isomorphic to the disjoint union of all its fibers + 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 + + -- the natural transformation + -- just applies typeSectionIso + η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) + + -- isomorphism follows from typeSectionIso + η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 ⟧))) + + + -- ======================================== + -- ε : KL ≅ 𝟙 + -- ======================================== + + module _ where + open Iso + -- the iso we deserve + -- says that a type family at x is isomorphic to the fiber over x of that type family packaged up + 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) + + -- the natural isomorphism + -- applies typeFiberIso (inv) + ε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 + + -- naturality + -- the annoying part is all the substs + γ-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 + -- fiber equality proof that we get from an application of KLP + eq' = snd ((KLP ⟪ f' ⟫) a) + + -- top right of the commuting diagram + -- "remove" the subst from the inside + 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 _ eq X') + X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X' + + -- bottom left of the commuting diagram + -- "remove" the subst from the outside + 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 ⟆ ⟆ + + -- naturality of the above construction applies a similar argument as in `γ-homFunExt` + ε-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 + -- this is exactly the same as the one from before, can refactor? + X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X') + X'≡subst = transport-filler _ _ + + -- extracted out type since need to use in in 'left' body as well + 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 ⟆)} _))) + + + -- putting it all together + + 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 + +-- Isomorphism between presheaves of different levels +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) \ No newline at end of file diff --git a/Cubical.Categories.Presheaf.Representable.html b/Cubical.Categories.Presheaf.Representable.html index b14fcb6d3e..8d49ed7049 100644 --- a/Cubical.Categories.Presheaf.Representable.html +++ b/Cubical.Categories.Presheaf.Representable.html @@ -47,7 +47,7 @@ variable ℓ ℓ' : Level open Category -open Contravariant +open Contravariant open NatIso open isIsoC @@ -59,12 +59,12 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where Representation : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) Representation = - Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P + Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P Representable : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) Representable = ∥ Representation ∥₁ - Elements = ∫ᴾ_ {C = C} P + Elements = ∫ᴾ_ {C = C} P TerminalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) TerminalElement = Terminal Elements @@ -146,53 +146,53 @@ (NatIso≡ (cong NatTrans.N-ob (yonedaᴾ* {C = C} P (repr .fst) .Iso.leftInv (repr .snd .trans))))) - isTerminalToIsUniversal : ∀ {η : Elementᴾ {C = C} P} + isTerminalToIsUniversal : ∀ {η : Elementᴾ {C = C} P} → isTerminal Elements η → isUniversal (η .fst) (η .snd) isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .fst = term (_ , ϕ) .fst .fst isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .snd = - sym (term (_ , ϕ) .fst .snd) - isTerminalToIsUniversal {η} term A .equiv-proof ϕ .snd (f , commutes) = - Σ≡Prop (λ _ → (P ⟅ A ⟆) .snd _ _) - (cong fst (term (A , ϕ) .snd (f , sym commutes))) - - isUniversalToIsTerminal : - ∀ (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst) - → isUniversal vertex element - → isTerminal Elements (vertex , element) - isUniversalToIsTerminal vertex element universal ϕ .fst .fst = - universal _ .equiv-proof (ϕ .snd) .fst .fst - isUniversalToIsTerminal vertex element universal ϕ .fst .snd = - sym (universal _ .equiv-proof (ϕ .snd) .fst .snd) - isUniversalToIsTerminal vertex element universal ϕ .snd (f , commutes) = - Σ≡Prop - (λ _ → (P ⟅ _ ⟆) .snd _ _) - (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , sym commutes))) - - terminalElementToUniversalElement : TerminalElement → UniversalElement - terminalElementToUniversalElement η .vertex = η .fst .fst - terminalElementToUniversalElement η .element = η .fst .snd - terminalElementToUniversalElement η .universal = - isTerminalToIsUniversal (η .snd) - - universalElementToTerminalElement : UniversalElement → TerminalElement - universalElementToTerminalElement η .fst .fst = η .vertex - universalElementToTerminalElement η .fst .snd = η .element - universalElementToTerminalElement η .snd = - isUniversalToIsTerminal (η .vertex) (η .element) (η .universal) - - TerminalElement≅UniversalElement : Iso TerminalElement UniversalElement - TerminalElement≅UniversalElement .Iso.fun = terminalElementToUniversalElement - TerminalElement≅UniversalElement .Iso.inv = universalElementToTerminalElement - TerminalElement≅UniversalElement .Iso.rightInv η = - isoFunInjective UniversalElementIsoΣ _ _ - (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) refl))) - TerminalElement≅UniversalElement .Iso.leftInv η = - Σ≡Prop (isPropIsTerminal Elements) refl - - Representation≅TerminalElement : Iso Representation TerminalElement - Representation≅TerminalElement = - compIso - Representation≅UniversalElement - (invIso TerminalElement≅UniversalElement) + term (_ , ϕ) .fst .snd + isTerminalToIsUniversal {η} term A .equiv-proof ϕ .snd (f , commutes) = + Σ≡Prop (λ _ → (P ⟅ A ⟆) .snd _ _) + (cong fst (term (A , ϕ) .snd (f , commutes))) + + isUniversalToIsTerminal : + ∀ (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst) + → isUniversal vertex element + → isTerminal Elements (vertex , element) + isUniversalToIsTerminal vertex element universal ϕ .fst .fst = + universal _ .equiv-proof (ϕ .snd) .fst .fst + isUniversalToIsTerminal vertex element universal ϕ .fst .snd = + universal _ .equiv-proof (ϕ .snd) .fst .snd + isUniversalToIsTerminal vertex element universal ϕ .snd (f , commutes) = + Σ≡Prop + (λ _ → (P ⟅ _ ⟆) .snd _ _) + (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , commutes))) + + terminalElementToUniversalElement : TerminalElement → UniversalElement + terminalElementToUniversalElement η .vertex = η .fst .fst + terminalElementToUniversalElement η .element = η .fst .snd + terminalElementToUniversalElement η .universal = + isTerminalToIsUniversal (η .snd) + + universalElementToTerminalElement : UniversalElement → TerminalElement + universalElementToTerminalElement η .fst .fst = η .vertex + universalElementToTerminalElement η .fst .snd = η .element + universalElementToTerminalElement η .snd = + isUniversalToIsTerminal (η .vertex) (η .element) (η .universal) + + TerminalElement≅UniversalElement : Iso TerminalElement UniversalElement + TerminalElement≅UniversalElement .Iso.fun = terminalElementToUniversalElement + TerminalElement≅UniversalElement .Iso.inv = universalElementToTerminalElement + TerminalElement≅UniversalElement .Iso.rightInv η = + isoFunInjective UniversalElementIsoΣ _ _ + (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) refl))) + TerminalElement≅UniversalElement .Iso.leftInv η = + Σ≡Prop (isPropIsTerminal Elements) refl + + Representation≅TerminalElement : Iso Representation TerminalElement + Representation≅TerminalElement = + compIso + Representation≅UniversalElement + (invIso TerminalElement≅UniversalElement) \ No newline at end of file