[WIP] Univalence in ad-hoc category in product

src/Cat/Category.agda

@@ -136,12 +136,25 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Univalent[Contr] : Set _
     Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
 
+    Univalent[Andrea] : Set _
+    Univalent[Andrea] = ∀ A B → (A ≅ B) ≃ (A ≡ B)
+
     -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
     -- Date: Wed, Mar 21, 2018 at 3:12 PM
     --
     -- This is not so straight-forward so you can assume it
     postulate from[Contr] : Univalent[Contr] → Univalent
 
+    from[Andrea] : Univalent[Andrea] → Univalent
+    from[Andrea] = from[Contr] Function.∘ step
+      where
+      module _ (f : Univalent[Andrea]) (A : Object) where
+        aux : isContr (Σ[ B ∈ Object ] A ≡ B)
+        aux = ?
+
+        step : isContr (Σ Object (A ≅_))
+        step = {!subst {P = isContr} {!!} aux!}
+
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i
 
@@ -205,9 +218,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
     propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ → arrowsAreSets _ _)
 
-    module _ {A B : Object} {f : Arrow A B} where
+    module _ {A B : Object} (f : Arrow A B) where
-      isoIsProp : isProp (Isomorphism f)
+      propIsomorphism : isProp (Isomorphism f)
-      isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
+      propIsomorphism a@(g , η , ε) a'@(g' , η' , ε') =
         lemSig (λ g → propIsInverseOf) a a' geq
           where
             geq : g ≡ g'
@@ -303,12 +316,19 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     univalent≃ = _ , univalent
 
     module _ {A B : Object} where
-      iso-to-id : (A ≅ B) → (A ≡ B)
+      private
-      iso-to-id = fst (toIso _ _ univalent)
+        iso : TypeIsomorphism (idToIso A B)
+        iso = toIso _ _ univalent
+
+      isoToId : (A ≅ B) → (A ≡ B)
+      isoToId = fst iso
 
       asTypeIso : TypeIsomorphism (idToIso A B)
       asTypeIso = toIso _ _ univalent
 
+      inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
+      inverse-from-to-iso' = snd iso
+
     -- | All projections are propositions.
     module Propositionality where
       -- | Terminal objects are propositional - a.k.a uniqueness of terminal
@@ -338,7 +358,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         iso : X ≅ Y
         iso = X→Y , Y→X , left , right
         p0 : X ≡ Y
-        p0 = iso-to-id iso
+        p0 = isoToId iso
         p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ]
         p1 = lemPropF propIsTerminal p0
         res : Xt ≡ Yt
@@ -368,7 +388,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         iso : X ≅ Y
         iso = Y→X , X→Y , right , left
         res : Xi ≡ Yi
-        res = lemSig propIsInitial _ _ (iso-to-id iso)
+        res = lemSig propIsInitial _ _ (isoToId iso)
 
 module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ

src/Cat/Category/Product.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
 module Cat.Category.Product where
 
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
@@ -183,7 +183,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       --     ; _∎ to _∎! )
       -- lawl
       --   : ((X , xa , xb) ≡ (Y , ya , yb))
-      --   ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.iso-to-id iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+      --   ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.isoToId iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
       -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!}
       -- Problem with the above approach: Preorders only work for heterogeneous equaluties.
 
@@ -192,7 +192,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)
       -- ≅
       -- Σ (X ℂ.≅ Y) (λ iso
-      --   → let p = ℂ.iso-to-id iso
+      --   → let p = ℂ.isoToId iso
       --   in
       --   ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
       --   × PathP (λ i → ℂ.Arrow (p i) B) xb yb
@@ -207,33 +207,18 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
         , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
         , record
-          { verso-recto = {!!}
+          { verso-recto = funExt (λ{ p → refl})
-          ; recto-verso = {!!}
+          ; recto-verso = funExt (λ{ (p , q , r) → refl})
           }
           where
           open import Function renaming (_∘_ to _⊙_)
-      step1
+
-        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+      -- Should follow from c being univalent
-        ≈ Σ (X ℂ.≅ Y) (λ iso
+      iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)
-          → let p = ℂ.iso-to-id iso
+      iso-id-inv {p} = sym (λ i → AreInverses.verso-recto ℂ.inverse-from-to-iso' i p)
-          in
+      id-iso-inv : {iso : X ℂ.≅ Y} → iso ≡ ℂ.idToIso X Y (ℂ.isoToId iso)
-          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
+      id-iso-inv {iso} = sym (λ i → AreInverses.recto-verso ℂ.inverse-from-to-iso' i iso)
-          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+
-          )
-      step1
-        = (λ{ (p , x) → (ℂ.idToIso _ _ p) , {!snd x!}})
-        -- Goal is:
-        --
-        --     φ x
-        --
-        -- where `x` is
-        --
-        --   ℂ.iso-to-id (ℂ.idToIso _ _ p)
-        --
-        -- I have `φ p` in scope, but surely `p` and `x` are the same - though
-        -- perhaps not definitonally.
-        , (λ{ (iso , x) → ℂ.iso-to-id iso , x})
-        , record { verso-recto = {!!} ; recto-verso = {!!} }
       lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g
       lemA {A} {B} {f = f} {g} p i = p i , h i
          where
@@ -245,25 +230,81 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
            (ℂ.arrowsAreSets (ℂ [ fst (snd B) ∘ a ]) (fst (snd A)))
            λ _ → ℂ.arrowsAreSets (ℂ [ snd (snd B) ∘ a ]) (snd (snd A)))
            p
+
+      step1
+        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+        ≈ Σ (X ℂ.≅ Y) (λ iso
+          → let p = ℂ.isoToId iso
+          in
+          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
+          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+          )
+      step1
+        = (λ{ (p , x)
+          → (ℂ.idToIso _ _ p)
+          , let
+             P-l : (p : X ≡ Y) → Set _
+             P-l φ = PathP (λ i → ℂ.Arrow (φ i) A) xa ya
+             P-r : (p : X ≡ Y) → Set _
+             P-r φ = PathP (λ i → ℂ.Arrow (φ i) B) xb yb
+             left  : P-l p
+             left = fst x
+             right : P-r p
+             right = snd x
+           in subst {P = P-l} iso-id-inv left , subst {P = P-r} iso-id-inv right
+          })
+        -- Goal is:
+        --
+        --     φ x
+        --
+        -- where `x` is
+        --
+        --   ℂ.isoToId (ℂ.idToIso _ _ p)
+        --
+        -- I have `φ p` in scope, but surely `p` and `x` are the same - though
+        -- perhaps not definitonally.
+        , (λ{ (iso , x) → ℂ.isoToId iso , x})
+        , record
+          { verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) (toPathP {A = λ i → {!!}} {!!})})
+          -- { verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}})
+          ; recto-verso = funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
+          }
       step2
         : Σ (X ℂ.≅ Y) (λ iso
-          → let p = ℂ.iso-to-id iso
+          → let p = ℂ.isoToId iso
           in
           ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
           × PathP (λ i → ℂ.Arrow (p i) B) xb yb
           )
         ≈ ((X , xa , xb) ≅ (Y , ya , yb))
       step2
-        = ( λ{ ((f , f~ , inv-f) , x)
+        = ( λ{ ((f , f~ , inv-f) , p , q)
-            → ( f , {!!})
+          → ( f , (let r = fromPathP p in {!r!}) , {!!})
-            , ( (f~ , {!!})
+            , ( (f~ , {!!} , {!!})
-              , lemA {!!}
+              , lemA (fst inv-f)
-              , lemA {!!}
+              , lemA (snd inv-f)
               )
             }
           )
-        , (λ x → {!!})
+        , (λ{ (f , f~ , inv-f , inv-f~) →
-        , {!!}
+          let
+            iso : X ℂ.≅ Y
+            iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
+            helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId ? i) A) xa ya
+            helper = {!!}
+          in iso , helper , {!!}})
+        , record
+          { verso-recto = funExt (λ x → lemSig
+            (λ x → propSig prop0 (λ _ → prop1))
+            _ _
+            (Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
+          ; recto-verso = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
+          }
+          where
+          prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya)
+          prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) A) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
+          prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) B) xb yb)
+          prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) B) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb
       -- One thing to watch out for here is that the isomorphisms going forwards
       -- must compose to give idToIso
       iso
@@ -273,8 +314,16 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         where
         infixl 5 _⊙_
         _⊙_ = composeIso
+      equiv1
+        : ((X , xa , xb) ≡ (Y , ya , yb))
+        ≃ ((X , xa , xb) ≅ (Y , ya , yb))
+      equiv1 = _ , fromIso _ _ (snd iso)
+
       res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb))
-      res = {!snd iso!}
+      res = {!snd equiv1!}
+
+    univalent2 : ∀ X Y → (X ≅ Y) ≃ (X ≡ Y)
+    univalent2 = {!!}
 
     isCat : IsCategory raw
     IsCategory.isPreCategory isCat = isPreCat