diff --git a/Cubical.Categories.Instances.CommAlgebras.html b/Cubical.Categories.Instances.CommAlgebras.html
index adde9a99ed..ca8d0d7dc1 100644
--- a/Cubical.Categories.Instances.CommAlgebras.html
+++ b/Cubical.Categories.Instances.CommAlgebras.html
@@ -87,7 +87,7 @@
open IsAlgebraHom
LimitsCommAlgebrasCategory : Limits {ℓ-max ℓ ℓJ} {ℓJ'} (CommAlgebrasCategory {ℓ' = theℓ})
- fst (lim (LimitsCommAlgebrasCategory J D)) = lim (completeSET J (ffA→SET ∘F D)) .fst
+ fst (lim (LimitsCommAlgebrasCategory J D)) = lim (completeSET J (ffA→SET ∘F D)) .fst
0a (snd (lim (LimitsCommAlgebrasCategory J D))) =
cone (λ v _ → 0a (snd (F-ob D v)))
(λ e → funExt (λ _ → F-hom D e .snd .pres0))
@@ -127,7 +127,7 @@
(λ _ → cone≡ (λ v → funExt (λ _ → ⋆IdL (snd (F-ob D v)) _)))
λ _ _ _ → cone≡ λ v → funExt λ _ → ⋆AssocL (snd (F-ob D v)) _ _ _
fst (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v) =
- coneOut (limCone (completeSET J (funcComp ffA→SET D))) v
+ coneOut (limCone (completeSET J (funcComp ffA→SET D))) v
pres0 (snd (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v)) = refl
pres1 (snd (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v)) = refl
pres+ (snd (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v)) = λ _ _ → refl
@@ -135,9 +135,9 @@
pres- (snd (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v)) = λ _ → refl
pres⋆ (snd (coneOut (limCone (LimitsCommAlgebrasCategory J D)) v)) = λ _ _ → refl
coneOutCommutes (limCone (LimitsCommAlgebrasCategory J D)) e =
- AlgebraHom≡ (coneOutCommutes (limCone (completeSET J (funcComp ffA→SET D))) e)
+ AlgebraHom≡ (coneOutCommutes (limCone (completeSET J (funcComp ffA→SET D))) e)
univProp (LimitsCommAlgebrasCategory J D) c cc = uniqueExists
- ( ( λ x → limArrow (completeSET J (funcComp ffA→SET D))
+ ( ( λ x → limArrow (completeSET J (funcComp ffA→SET D))
(fst c , snd c .is-set)
(cone (λ v _ → coneOut cc v .fst x)
(λ e → funExt (λ _ → funExt⁻ (cong fst (coneOutCommutes cc e)) x))) x)
diff --git a/Cubical.Categories.Instances.CommRings.html b/Cubical.Categories.Instances.CommRings.html
index 187e9e5ce5..2bd351b0e7 100644
--- a/Cubical.Categories.Instances.CommRings.html
+++ b/Cubical.Categories.Instances.CommRings.html
@@ -134,7 +134,7 @@
LimitsCommRingsCategory : Limits {ℓJ} {ℓJ'} (CommRingsCategory {ℓ = ℓ-max ℓJ ℓJ'})
fst (lim (LimitsCommRingsCategory J D)) =
- lim {J = J} (completeSET J (funcComp ForgetfulCommRing→Set D)) .fst
+ lim {J = J} (completeSET J (funcComp ForgetfulCommRing→Set D)) .fst
0r (snd (lim (LimitsCommRingsCategory J D))) =
cone (λ v _ → 0r (snd (F-ob D v)))
(λ e → funExt (λ _ → F-hom D e .snd .pres0))
@@ -165,17 +165,17 @@
(λ _ _ _ → cone≡ (λ v → funExt (λ _ → ·DistR+ (snd (F-ob D v)) _ _ _)))
(λ _ _ → cone≡ (λ v → funExt (λ _ → snd (F-ob D v) .·Comm _ _)))
fst (coneOut (limCone (LimitsCommRingsCategory J D)) v) =
- coneOut (limCone (completeSET J (funcComp ForgetfulCommRing→Set D))) v
+ coneOut (limCone (completeSET J (funcComp ForgetfulCommRing→Set D))) v
pres0 (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = refl
pres1 (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = refl
pres+ (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ _ → refl
pres· (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ _ → refl
pres- (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ → refl
coneOutCommutes (limCone (LimitsCommRingsCategory J D)) e =
- RingHom≡ (coneOutCommutes (limCone (completeSET J (funcComp ForgetfulCommRing→Set D))) e)
+ RingHom≡ (coneOutCommutes (limCone (completeSET J (funcComp ForgetfulCommRing→Set D))) e)
univProp (LimitsCommRingsCategory J D) c cc =
uniqueExists
- ( (λ x → limArrow (completeSET J (funcComp ForgetfulCommRing→Set D))
+ ( (λ x → limArrow (completeSET J (funcComp ForgetfulCommRing→Set D))
(fst c , snd c .is-set)
(cone (λ v _ → coneOut cc v .fst x)
(λ e → funExt (λ _ → funExt⁻ (cong fst (coneOutCommutes cc e)) x))) x)
diff --git a/Cubical.Categories.Instances.Sets.html b/Cubical.Categories.Instances.Sets.html
index 9b3e13d969..994d5d9db4 100644
--- a/Cubical.Categories.Instances.Sets.html
+++ b/Cubical.Categories.Instances.Sets.html
@@ -55,85 +55,141 @@
LiftF .F-id = refl
LiftF .F-seq f g = funExt λ x → refl
-module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where
- open NatTrans
-
-
- preComp : {x y : C .ob}
- → (f : C [ x , y ])
- → C [ x ,-] ⇒ F
- → C [ y ,-] ⇒ F
- preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
- preComp f α .N-hom {x = c} {d} k
- = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
- ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
- (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
- ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
- (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
- ∎
-
-
-
-open isIso renaming (inv to cInv)
-open Iso
-
-module _ {A B : (SET ℓ) .ob } where
-
- Iso→CatIso : Iso (fst A) (fst B)
- → CatIso (SET ℓ) A B
- Iso→CatIso is .fst = is .fun
- Iso→CatIso is .snd .cInv = is .inv
- Iso→CatIso is .snd .sec = funExt λ b → is .rightInv b
- Iso→CatIso is .snd .ret = funExt λ b → is .leftInv b
-
- CatIso→Iso : CatIso (SET ℓ) A B
- → Iso (fst A) (fst B)
- CatIso→Iso cis .fun = cis .fst
- CatIso→Iso cis .inv = cis .snd .cInv
- CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .snd .sec b
- CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .snd .ret b
-
-
- Iso-Iso-CatIso : Iso (Iso (fst A) (fst B)) (CatIso (SET ℓ) A B)
- fun Iso-Iso-CatIso = Iso→CatIso
- inv Iso-Iso-CatIso = CatIso→Iso
- rightInv Iso-Iso-CatIso b = refl
- fun (leftInv Iso-Iso-CatIso a i) = fun a
- inv (leftInv Iso-Iso-CatIso a i) = inv a
- rightInv (leftInv Iso-Iso-CatIso a i) = rightInv a
- leftInv (leftInv Iso-Iso-CatIso a i) = leftInv a
-
- Iso-CatIso-≡ : Iso (CatIso (SET ℓ) A B) (A ≡ B)
- Iso-CatIso-≡ = compIso (invIso Iso-Iso-CatIso) (hSet-Iso-Iso-≡ _ _)
-
-
-
-isUnivalentSET : isUnivalent {ℓ' = ℓ} (SET _)
-isUnivalent.univ isUnivalentSET (A , isSet-A) (B , isSet-B) =
- precomposesToId→Equiv
- pathToIso _ (funExt w) (isoToIsEquiv Iso-CatIso-≡)
- where
- w : _
- w ci =
- invEq
- (congEquiv (isoToEquiv (invIso Iso-Iso-CatIso)))
- (SetsIso≡-ext isSet-A isSet-B
- (λ x i → transp (λ _ → B) i (ci .fst (transp (λ _ → A) i x)))
- (λ x i → transp (λ _ → A) i (ci .snd .cInv (transp (λ _ → B) i x))))
-
-
-
-open LimCone
-open Cone
-
-completeSET : ∀ {ℓJ ℓJ'} → Limits {ℓJ} {ℓJ'} (SET (ℓ-max ℓJ ℓJ'))
-lim (completeSET J D) = Cone D (Unit* , isOfHLevelLift 2 isSetUnit) , isSetCone D _
-coneOut (limCone (completeSET J D)) j e = coneOut e j tt*
-coneOutCommutes (limCone (completeSET J D)) j i e = coneOutCommutes e j i tt*
-univProp (completeSET J D) c cc =
- uniqueExists
- (λ x → cone (λ v _ → coneOut cc v x) (λ e i _ → coneOutCommutes cc e i x))
- (λ _ → funExt (λ _ → refl))
- (λ x → isPropIsConeMor cc (limCone (completeSET J D)) x)
- (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d))))
+module _ {ℓ ℓ' : Level} where
+ isFullyFaithfulLiftF : isFullyFaithful (LiftF {ℓ} {ℓ'})
+ isFullyFaithfulLiftF X Y = isoToIsEquiv LiftFIso
+ where
+ open Iso
+ LiftFIso : Iso (X .fst → Y .fst)
+ (Lift {ℓ}{ℓ'} (X .fst) → Lift {ℓ}{ℓ'} (Y .fst))
+ fun LiftFIso = LiftF .F-hom {X} {Y}
+ inv LiftFIso = λ f x → f (lift x) .lower
+ rightInv LiftFIso = λ _ → funExt λ _ → refl
+ leftInv LiftFIso = λ _ → funExt λ _ → refl
+
+module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where
+ open NatTrans
+
+
+ preComp : {x y : C .ob}
+ → (f : C [ x , y ])
+ → C [ x ,-] ⇒ F
+ → C [ y ,-] ⇒ F
+ preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
+ preComp f α .N-hom {x = c} {d} k
+ = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
+ ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
+ (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
+ ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
+ (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
+ ∎
+
+
+
+open isIso renaming (inv to cInv)
+open Iso
+
+module _ {A B : (SET ℓ) .ob } where
+
+ Iso→CatIso : Iso (fst A) (fst B)
+ → CatIso (SET ℓ) A B
+ Iso→CatIso is .fst = is .fun
+ Iso→CatIso is .snd .cInv = is .inv
+ Iso→CatIso is .snd .sec = funExt λ b → is .rightInv b
+ Iso→CatIso is .snd .ret = funExt λ b → is .leftInv b
+
+ CatIso→Iso : CatIso (SET ℓ) A B
+ → Iso (fst A) (fst B)
+ CatIso→Iso cis .fun = cis .fst
+ CatIso→Iso cis .inv = cis .snd .cInv
+ CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .snd .sec b
+ CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .snd .ret b
+
+
+ Iso-Iso-CatIso : Iso (Iso (fst A) (fst B)) (CatIso (SET ℓ) A B)
+ fun Iso-Iso-CatIso = Iso→CatIso
+ inv Iso-Iso-CatIso = CatIso→Iso
+ rightInv Iso-Iso-CatIso b = refl
+ fun (leftInv Iso-Iso-CatIso a i) = fun a
+ inv (leftInv Iso-Iso-CatIso a i) = inv a
+ rightInv (leftInv Iso-Iso-CatIso a i) = rightInv a
+ leftInv (leftInv Iso-Iso-CatIso a i) = leftInv a
+
+ Iso-CatIso-≡ : Iso (CatIso (SET ℓ) A B) (A ≡ B)
+ Iso-CatIso-≡ = compIso (invIso Iso-Iso-CatIso) (hSet-Iso-Iso-≡ _ _)
+
+
+
+isUnivalentSET : isUnivalent {ℓ' = ℓ} (SET _)
+isUnivalent.univ isUnivalentSET (A , isSet-A) (B , isSet-B) =
+ precomposesToId→Equiv
+ pathToIso _ (funExt w) (isoToIsEquiv Iso-CatIso-≡)
+ where
+ w : _
+ w ci =
+ invEq
+ (congEquiv (isoToEquiv (invIso Iso-Iso-CatIso)))
+ (SetsIso≡-ext isSet-A isSet-B
+ (λ x i → transp (λ _ → B) i (ci .fst (transp (λ _ → A) i x)))
+ (λ x i → transp (λ _ → A) i (ci .snd .cInv (transp (λ _ → B) i x))))
+
+
+open LimCone
+open Cone
+
+completeSET : ∀ {ℓJ ℓJ'} → Limits {ℓJ} {ℓJ'} (SET (ℓ-max ℓJ ℓJ'))
+lim (completeSET J D) = Cone D (Unit* , isOfHLevelLift 2 isSetUnit) , isSetCone D _
+coneOut (limCone (completeSET J D)) j e = coneOut e j tt*
+coneOutCommutes (limCone (completeSET J D)) j i e = coneOutCommutes e j i tt*
+univProp (completeSET J D) c cc =
+ uniqueExists
+ (λ x → cone (λ v _ → coneOut cc v x) (λ e i _ → coneOutCommutes cc e i x))
+ (λ _ → funExt (λ _ → refl))
+ (λ x → isPropIsConeMor cc (limCone (completeSET J D)) x)
+ (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d))))
+
+
+
+
+module _ {ℓ : Level} where
+ preservesLimitsLiftF : preservesLimits {ℓJ = ℓ} {ℓJ' = ℓ} (LiftF {ℓ} {ℓ-suc ℓ})
+ preservesLimitsLiftF = preservesLimitsChar _
+ completeSET
+ completeSETSuc
+ limSetIso
+ λ _ _ _ → refl
+ where
+
+ completeSETSuc : Limits {ℓJ = ℓ} {ℓJ' = ℓ} (SET (ℓ-suc ℓ))
+ lim (completeSETSuc J D) = Cone D (Unit* , isOfHLevelLift 2 isSetUnit) , isSetCone D _
+ coneOut (limCone (completeSETSuc J D)) j e = coneOut e j tt*
+ coneOutCommutes (limCone (completeSETSuc J D)) j i e = coneOutCommutes e j i tt*
+ univProp (completeSETSuc J D) c cc =
+ uniqueExists
+ (λ x → cone (λ v _ → coneOut cc v x) (λ e i _ → coneOutCommutes cc e i x))
+ (λ _ → funExt (λ _ → refl))
+ (λ x → isPropIsConeMor cc (limCone (completeSETSuc J D)) x)
+ (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d))))
+
+ lowerCone : ∀ J D
+ → Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
+ → Cone D (Unit* , isOfHLevelLift 2 isSetUnit)
+ coneOut (lowerCone J D cc) v tt* = cc .coneOut v tt* .lower
+ coneOutCommutes (lowerCone J D cc) e =
+ funExt λ { tt* → cong lower (funExt⁻ (cc .coneOutCommutes e) tt*) }
+
+ liftCone : ∀ J D
+ → Cone D (Unit* , isOfHLevelLift 2 isSetUnit)
+ → Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
+ coneOut (liftCone J D cc) v tt* = lift (cc .coneOut v tt*)
+ coneOutCommutes (liftCone J D cc) e =
+ funExt λ { tt* → cong lift (funExt⁻ (cc .coneOutCommutes e) tt*) }
+
+ limSetIso : ∀ J D → CatIso (SET (ℓ-suc ℓ))
+ (completeSETSuc J (LiftF ∘F D) .lim)
+ (LiftF .F-ob (completeSET J D .lim))
+ fst (limSetIso J D) cc = lift (lowerCone J D cc)
+ cInv (snd (limSetIso J D)) cc = liftCone J D (cc .lower)
+ sec (snd (limSetIso J D)) = funExt (λ _ → liftExt (cone≡ λ _ → refl))
+ ret (snd (limSetIso J D)) = funExt (λ _ → cone≡ λ _ → refl)