Prove step 3 in proof of unvivalence for hSet without ua

src/Cat/Categories/Fam.agda

@@ -8,7 +8,7 @@ open import Cat.Category
 
 module _ (ℓa ℓb : Level) where
   private
-    Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb})
+    Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb)
     Arr : Object → Object → Set (ℓa ⊔ ℓb)
     Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
     𝟙 : {A : Object} → Arr A A

src/Cat/Categories/Sets.agda

@@ -147,26 +147,47 @@ module _ (ℓ : Level) where
         Q→P : ∀ {a} → Q a ≡ P a
         Q→P = sym P→Q
         f : Σ A P → Σ A Q
-        f (a , pA) = a , coe P→Q pA
+        f (a , pA) = a , _≃_.eqv (eA a) pA
         g : Σ A Q → Σ A P
-        g (a , qA) = a , coe Q→P qA
+        g (a , qA) = a , g' qA
+          where
+          module E = Equivalence (eA a)
+          k : Eqv.Isomorphism _
+          k = E.toIso (_≃_.isEqv (eA a))
+          open Σ k renaming (proj₁ to g')
         ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
         ve-re x i = proj₁ x , eq i
           where
           eq : proj₂ ((g ∘ f) x) ≡ proj₂ x
           eq = begin
             proj₂ ((g ∘ f) x) ≡⟨⟩
-            coe Q→P (proj₂ (f x))        ≡⟨⟩
-            coe Q→P (coe P→Q (proj₂ x))  ≡⟨ inv-coe P→Q ⟩
-            proj₂ x ∎
+            proj₂ (g (f (a , pA))) ≡⟨⟩
+            g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
+            pA ∎
+            where
+            open Σ x renaming (proj₁ to a ; proj₂ to pA)
+            module E = Equivalence (eA a)
+            k : Eqv.Isomorphism _
+            k = E.toIso (_≃_.isEqv (eA a))
+            open Σ k renaming (proj₁ to g' ; proj₂ to inv)
+            module A = AreInverses inv
+            -- anti-funExt
+            lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
+            lem i = A.verso-recto i pA
         re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
         re-ve x i = proj₁ x , eq i
           where
+          open Σ x renaming (proj₁ to a ; proj₂ to qA)
           eq = begin
             proj₂ ((f ∘ g) x)                 ≡⟨⟩
-            coe P→Q (coe Q→P (proj₂ x))       ≡⟨⟩
-            coe P→Q (coe (sym P→Q) (proj₂ x)) ≡⟨ inv-coe' P→Q ⟩
-            proj₂ x                           ∎
+            _≃_.eqv (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
+            qA                                ∎
+            where
+            module E = Equivalence (eA a)
+            k : Eqv.Isomorphism _
+            k = E.toIso (_≃_.isEqv (eA a))
+            open Σ k renaming (proj₁ to g' ; proj₂ to inv)
+            module A = AreInverses inv
         inv : AreInverses f g
         inv = record
           { verso-recto = funExt ve-re
@@ -279,15 +300,11 @@ module _ (ℓ : Level) where
       --
       -- is contractible, which implies univalence.
 
-    univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
-    univalent' hA = {!!} , {!!}
+    univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
+    univalent[Contr] hA = {!!} , {!!}
 
-    module _ {hA hB : hSet ℓ} where
-
-      -- Thierry: `thr0` implies univalence.
-      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
-      univalent = univalent'→univalent univalent'
-      -- let k = _≃_.isEqv (sym≃ conclusion) in {! k!}
+    univalent : Univalent
+    univalent = from[Contr] univalent[Contr]
 
     SetsIsCategory : IsCategory SetsRaw
     IsCategory.isAssociative SetsIsCategory = refl

src/Cat/Category.agda

@@ -120,18 +120,16 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
-    -- Alternative formulation of univalence which is easier to prove in the
-    -- case of the functor category.
+
+    -- | Equivalent formulation of univalence.
+    Univalent[Contr] : Set _
+    Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
+
+    -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
+    -- Date: Wed, Mar 21, 2018 at 3:12 PM
     --
-    --     ∀ A → isContr (Σ[ X ∈ Object ] iso A X)
-
-    -- future work ideas: compile to CAM
-    Univalent' : Set _
-    Univalent' = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
-
-    module _ (univalent' : Univalent') where
-      univalent'→univalent : Univalent
-      univalent'→univalent = {!!}
+    -- This is not so straight-forward so you can assume it
+    postulate from[Contr] : Univalent[Contr] → Univalent
 
 -- | The mere proposition of being a category.
 --
@@ -208,6 +206,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
         hh = arrowsAreSets _ _ (snd x) (snd y)
       in h i , hh i
 
+    module _ {A B : Object} {p q : A ≅ B} where
+      open Σ p       renaming (proj₁ to pf)
+      open Σ (snd p) renaming (proj₁ to pg ; proj₂ to pAreInv)
+      open Σ q       renaming (proj₁ to qf)
+      open Σ (snd q) renaming (proj₁ to qg ; proj₂ to qAreInv)
+      module _ (a : pf ≡ qf) (b : pg ≡ qg) where
+        private
+          open import Cubical.Sigma
+          open import Cubical.NType.Properties
+          -- Problem: How do I apply lempPropF twice?
+          cc : (λ i → IsInverseOf (a i) pg) [ pAreInv ≡ _ ]
+          cc = lemPropF (λ x → propIsInverseOf {A} {B} {x}) a
+          c : (λ i → IsInverseOf (a i) (b i)) [ pAreInv ≡ qAreInv ]
+          c = lemPropF (λ x → propIsInverseOf {A} {B} {{!!}}) {!cc!}
+
+        ≅-equality : p ≡ q
+        ≅-equality i = a i , b i , c i
+
     module _ {A B : Object} {f : Arrow A B} where
       isoIsProp : isProp (Isomorphism f)
       isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =

src/Cat/Category/Functor.agda

@@ -78,8 +78,8 @@ EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _
 EndoFunctor ℂ = Functor ℂ ℂ
 
 module _
-    {ℓa ℓb : Level}
-    {ℂ 𝔻 : Category ℓa ℓb}
+    {ℓc ℓc' ℓd ℓd' : Level}
+    {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'}
     (F : RawFunctor ℂ 𝔻)
     where
   private
@@ -96,8 +96,7 @@ module _
 
 -- Alternate version of above where `F` is indexed by an interval
 module _
-    {ℓa ℓb : Level}
-    {ℂ 𝔻 : Category ℓa ℓb}
+    {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'}
     {F : I → RawFunctor ℂ 𝔻}
     where
   private
@@ -109,7 +108,7 @@ module _
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
     (\ F → propIsFunctor F) (\ i → F i)
 
-module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
+module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
   open Functor
   Functor≡ : {F G : Functor ℂ 𝔻}
     → Functor.raw F ≡ Functor.raw G