Isomorphisms between hSets, isUnivalent SET

Cubical/Categories/Category/Base.agda

@@ -60,10 +60,30 @@ record CatIso (C : Category ℓ ℓ') (x y : C .ob) : Type ℓ' where
     sec : inv ⋆⟨ C ⟩ mor ≡ C .id
     ret : mor ⋆⟨ C ⟩ inv ≡ C .id
 
-pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y
-pathToIso {C = C} p = J (λ z _ → CatIso _ _ z) (catiso idx idx (C .⋆IdL idx) (C .⋆IdL idx)) p
+idCatIso : {C : Category ℓ ℓ'} {x : C .ob} → CatIso C x x
+idCatIso {C = C} = (catiso (C .id) (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id)))
+
+isSet-CatIso : {C : Category ℓ ℓ'} → ∀ x y → isSet (CatIso C x y)
+isSet-CatIso {C = C} x y F G p q = w
   where
-    idx = C .id
+    w : _
+    CatIso.mor (w i j) = isSetHom C _ _ (cong CatIso.mor p) (cong CatIso.mor q) i j
+    CatIso.inv (w i j) = isSetHom C _ _ (cong CatIso.inv p) (cong CatIso.inv q) i j
+    CatIso.sec (w i j) =
+       isSet→SquareP
+       (λ i j → isProp→isSet {A = CatIso.inv (w i j) ⋆⟨ C ⟩ CatIso.mor (w i j) ≡ C .id} (isSetHom C _ _))
+       (cong CatIso.sec p) (cong CatIso.sec q) (λ _ → CatIso.sec F) (λ _ → CatIso.sec G) i j
+    CatIso.ret (w i j) =
+       isSet→SquareP
+       (λ i j → isProp→isSet {A = CatIso.mor (w i j) ⋆⟨ C ⟩ CatIso.inv (w i j) ≡ C .id} (isSetHom C _ _))
+       (cong CatIso.ret p) (cong CatIso.ret q) (λ _ → CatIso.ret F) (λ _ → CatIso.ret G) i j
+
+
+pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y
+pathToIso {C = C} p = J (λ z _ → CatIso _ _ z) idCatIso p
+
+pathToIso-refl : {C : Category ℓ ℓ'} {x : C .ob} → pathToIso {C = C} {x} refl ≡ idCatIso
+pathToIso-refl {C = C} {x} = JRefl (λ z _ → CatIso C x z) (idCatIso)
 
 -- Univalent Categories
 record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
@@ -79,6 +99,9 @@ record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
   CatIsoToPath {x = x} {y = y} p =
     equivFun (invEquiv (univEquiv x y)) p
 
+  isGroupoid-ob : isGroupoid (C .ob)
+  isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _))
+
 -- Opposite category
 _^op : Category ℓ ℓ' → Category ℓ ℓ'
 ob (C ^op)           = ob C

Cubical/Categories/Functor/Properties.agda

@@ -5,9 +5,11 @@ module Cubical.Categories.Functor.Properties where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function renaming (_∘_ to _◍_)
 open import Cubical.Foundations.GroupoidLaws using (lUnit; rUnit; assoc; cong-∙)
+open import Cubical.Foundations.HLevels
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor.Base
 
+
 private
   variable
     ℓ ℓ' ℓ'' : Level
@@ -114,3 +116,25 @@ module _ {F : Functor C D} where
         g = F ⟪ f ⟫
         g⁻¹ : D [ y' , x' ]
         g⁻¹ = F ⟪ f⁻¹ ⟫
+
+
+isSet-Functor : isSet (D .ob) → isSet (Functor C D)
+isSet-Functor {D = D} {C = C} isSet-D-ob F G p q = w
+  where
+    w : _
+    F-ob (w i i₁) = isSetΠ (λ _ → isSet-D-ob) _ _ (cong F-ob p) (cong F-ob q) i i₁
+    F-hom (w i i₁) z =
+     isSet→SquareP
+       (λ i i₁ → D .isSetHom {(F-ob (w i i₁) _)} {(F-ob (w i i₁) _)})
+        (λ i₁ → F-hom (p i₁) z) (λ i₁ → F-hom (q i₁) z) refl refl i i₁
+
+    F-id (w i i₁) =
+       isSet→SquareP
+       (λ i i₁ → isProp→isSet (D .isSetHom (F-hom (w i i₁) _) (D .id)))
+       (λ i₁ → F-id (p i₁)) (λ i₁ → F-id (q i₁)) refl refl i i₁
+
+    F-seq (w i i₁) _ _ =
+     isSet→SquareP
+       (λ i i₁ → isProp→isSet (D .isSetHom (F-hom (w i i₁) _) ((F-hom (w i i₁) _) ⋆⟨ D ⟩ (F-hom (w i i₁) _))))
+       (λ i₁ → F-seq (p i₁) _ _) (λ i₁ → F-seq (q i₁) _ _) refl refl i i₁
+

Cubical/Categories/Instances/Sets.agda

@@ -4,6 +4,8 @@ module Cubical.Categories.Instances.Sets where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Unit
 open import Cubical.Data.Sigma
@@ -67,13 +69,49 @@ module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where
 open CatIso renaming (inv to cInv)
 open Iso
 
-Iso→CatIso : ∀ {A B : (SET ℓ) .ob}
-           → Iso (fst A) (fst B)
-           → CatIso (SET ℓ) A B
-Iso→CatIso is .mor = is .fun
-Iso→CatIso is .cInv = is .inv
-Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
-Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv
+module _ {A B : (SET ℓ) .ob } where
+
+  Iso→CatIso : Iso (fst A) (fst B)
+             → CatIso (SET ℓ) A B
+  Iso→CatIso is .mor = is .fun
+  Iso→CatIso is .cInv = is .inv
+  Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
+  Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv
+
+  CatIso→Iso : CatIso (SET ℓ) A B
+             → Iso (fst A) (fst B)
+  CatIso→Iso cis .fun = cis .mor
+  CatIso→Iso cis .inv = cis .cInv
+  CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .sec b
+  CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .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-≡ _ _)
+
+-- SET is univalent
+
+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 .mor  (transp (λ _ → A) i x)))
+            (λ x i → transp (λ _ → A) i (ci .cInv (transp (λ _ → B) i x))))
 
 -- SET is complete
 

Cubical/Foundations/Equiv.agda

@@ -298,6 +298,14 @@ composesToId→Equiv f g id iseqf =
                 ∙∙ λ i → equiv-proof iseqf (f b) .snd (b , refl) i .fst)
          λ a i → id i a)
 
+precomposesToId→Equiv : (f : A → B) (g : B → A) → f ∘ g ≡ idfun B → isEquiv g → isEquiv f
+precomposesToId→Equiv f g id iseqg =  subst isEquiv (sym f-≡-g⁻) (snd (invEquiv (_ , iseqg)))
+  where
+     g⁻ = invEq (g , iseqg)
+
+     f-≡-g⁻ : _
+     f-≡-g⁻ = cong (f ∘_ ) (cong fst (sym (invEquiv-is-linv (g , iseqg)))) ∙ cong (_∘ g⁻) id
+
 -- equivalence between isEquiv and isEquiv'
 
 isEquiv-isEquiv'-Iso : (f : A → B) → Iso (isEquiv f) (isEquiv' f)

Cubical/Foundations/Equiv/Properties.agda

@@ -29,7 +29,7 @@ open import Cubical.Functions.FunExtEquiv
 
 private
   variable
-    ℓ ℓ′ : Level
+    ℓ ℓ′ ℓ′′ : Level
     A B C : Type ℓ
 
 isEquivInvEquiv : isEquiv (λ (e : A ≃ B) → invEquiv e)
@@ -198,3 +198,10 @@ isEquivFromIsContr : {A : Type ℓ} {B : Type ℓ′}
 isEquivFromIsContr f isContrA isContrB =
   subst isEquiv (λ i x → isContr→isProp isContrB (fst B≃A x) (f x) i) (snd B≃A)
   where B≃A = isContr→Equiv isContrA isContrB
+
+isEquiv[f∘equivFunA≃B]→isEquiv[f] : {A : Type ℓ} {B : Type ℓ′} {C : Type ℓ′′}
+                 → (f : B → C) (A≃B : A ≃ B)
+                 → isEquiv (f ∘ equivFun A≃B)
+                 → isEquiv f
+isEquiv[f∘equivFunA≃B]→isEquiv[f] f (g , gIsEquiv) f∘gIsEquiv  =
+  precomposesToId→Equiv f _  (cong fst (invEquiv-is-linv (_ , f∘gIsEquiv))) (snd (compEquiv (invEquiv (_ , f∘gIsEquiv) ) (_ , gIsEquiv)))

Cubical/Foundations/HLevels.agda

@@ -30,7 +30,8 @@ HLevel = ℕ
 private
   variable
     ℓ ℓ' ℓ'' ℓ''' ℓ'''' ℓ''''' : Level
-    A : Type ℓ
+    A A′ : Type ℓ
+    A' : Type ℓ'
     B : A → Type ℓ
     C : (x : A) → B x → Type ℓ
     D : (x : A) (y : B x) → C x y → Type ℓ
@@ -457,6 +458,9 @@ isSetΠ = isOfHLevelΠ 2
 isSetImplicitΠ : (h : (x : A) → isSet (B x)) → isSet ({x : A} → B x)
 isSetImplicitΠ h f g F G i j {x} = h x (f {x}) (g {x}) (λ i → F i {x}) (λ i → G i {x}) i j
 
+isSet→ : isSet A' → isSet (A → A')
+isSet→ isSet-A' = isOfHLevelΠ 2 (λ _ → isSet-A')
+
 isSetΠ2 : (h : (x : A) (y : B x) → isSet (C x y))
         → isSet ((x : A) (y : B x) → C x y)
 isSetΠ2 h = isSetΠ λ x → isSetΠ λ y → h x y
@@ -558,6 +562,10 @@ isOfHLevelTypeOfHLevel (suc n) (X , a) (Y , b) =
 isSetHProp : isSet (hProp ℓ)
 isSetHProp = isOfHLevelTypeOfHLevel 1
 
+isGroupoidHSet : isGroupoid (hSet ℓ)
+isGroupoidHSet = isOfHLevelTypeOfHLevel 2
+
+
 -- h-level of lifted type
 
 isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
@@ -671,3 +679,94 @@ snd (ΣSquareSet {B = B} pB {p = p} {q = q} {r = r} {s = s} sq i j) = lem i j
   lem : SquareP (λ i j → B (sq i j))
           (cong snd p) (cong snd r) (cong snd s) (cong snd q)
   lem = toPathP (isOfHLevelPathP' 1 (pB _) _ _ _ _)
+
+module _ (isSet-A : isSet A) (isSet-A' : isSet A') where
+
+
+  isSet-SetsIso : isSet (Iso A A')
+  isSet-SetsIso x y p₀ p₁ = h
+    where
+
+     module X = Iso x
+     module Y = Iso y
+
+     f-p : ∀ i₁ → (Iso.fun (p₀ i₁) , Iso.inv (p₀ i₁)) ≡
+                  (Iso.fun (p₁ i₁) , Iso.inv (p₁ i₁))
+     fst (f-p i₁ i) a  = isSet-A' (X.fun a ) (Y.fun a ) (cong _ p₀) (cong _ p₁) i i₁
+     snd (f-p i₁ i) a' = isSet-A  (X.inv a') (Y.inv a') (cong _ p₀) (cong _ p₁) i i₁
+
+     s-p : ∀ b → _
+     s-p b =
+       isSet→SquareP (λ i j → isProp→isSet (isSet-A' _ _))
+         refl refl (λ i₁ → (Iso.rightInv (p₀ i₁) b)) (λ i₁ → (Iso.rightInv (p₁ i₁) b))
+
+     r-p : ∀ a → _
+     r-p a =
+       isSet→SquareP (λ i j → isProp→isSet (isSet-A _ _))
+         refl refl (λ i₁ → (Iso.leftInv (p₀ i₁) a)) (λ i₁ → (Iso.leftInv (p₁ i₁) a))
+
+
+     h : p₀ ≡ p₁
+     Iso.fun (h i i₁) = fst (f-p i₁ i)
+     Iso.inv (h i i₁) = snd (f-p i₁ i)
+     Iso.rightInv (h i i₁) b = s-p b i₁ i
+     Iso.leftInv  (h i i₁) a = r-p a i₁ i
+
+
+  SetsIso≡-ext : ∀ {a b : Iso A A'}
+            → (∀ x → Iso.fun a x ≡ Iso.fun b x)
+            → (∀ x → Iso.inv a x ≡ Iso.inv b x)
+            → a ≡ b
+  Iso.fun (SetsIso≡-ext {a} {b} fun≡ inv≡ i) x = fun≡ x i
+  Iso.inv (SetsIso≡-ext {a} {b} fun≡ inv≡ i) x = inv≡ x i
+  Iso.rightInv (SetsIso≡-ext {a} {b} fun≡ inv≡ i) b₁ =
+     isSet→SquareP (λ _ _ → isSet-A')
+       (Iso.rightInv a b₁)
+       (Iso.rightInv b b₁)
+       (λ i → fun≡ (inv≡ b₁ i) i)
+       refl i
+  Iso.leftInv (SetsIso≡-ext {a} {b} fun≡ inv≡ i) a₁ =
+     isSet→SquareP (λ _ _ → isSet-A)
+       (Iso.leftInv a a₁)
+       (Iso.leftInv b a₁)
+       (λ i → inv≡ (fun≡ a₁ i) i )
+       refl i
+
+  SetsIso≡ : ∀ {a b : Iso A A'}
+            → (Iso.fun a ≡ Iso.fun b)
+            → (Iso.inv a ≡ Iso.inv b)
+            → a ≡ b
+  SetsIso≡ p q =
+    SetsIso≡-ext (funExt⁻ p) (funExt⁻ q)
+
+  isSet→Iso-Iso-≃ : Iso (Iso A A') (A ≃ A')
+  isSet→Iso-Iso-≃ = ww
+    where
+      open Iso
+
+      ww : Iso _ _
+      fun ww = isoToEquiv
+      inv ww = equivToIso
+      rightInv ww b = equivEq refl
+      leftInv ww a = SetsIso≡ refl refl
+
+
+  isSet→isEquiv-isoToPath : isEquiv isoToEquiv
+  isSet→isEquiv-isoToPath = isoToIsEquiv isSet→Iso-Iso-≃
+
+
+
+isSet→Iso-Iso-≡ : (isSet-A : isSet A) → (isSet-A′ : isSet A′) →  Iso (Iso A A′) (A ≡ A′)
+isSet→Iso-Iso-≡ isSet-A isSet-A′ = ww
+  where
+    open Iso
+
+    ww : Iso _ _
+    fun ww = isoToPath
+    inv ww = pathToIso
+    rightInv ww b = isInjectiveTransport (funExt λ _ → transportRefl _)
+    leftInv ww a = SetsIso≡-ext isSet-A isSet-A′ (λ _ → transportRefl (fun a _)) λ _ → cong (inv a) (transportRefl _)
+
+hSet-Iso-Iso-≡ : (A : hSet ℓ) → (A' : hSet ℓ) → Iso (Iso (fst A) (fst A')) (A ≡ A')
+hSet-Iso-Iso-≡ A A' = compIso (isSet→Iso-Iso-≡ (snd A) (snd A')) (equivToIso (_ , isEquiv-Σ≡Prop λ _ → isPropIsSet))
+