Stuff about univalence in the category of sets

libs/cubical

@@ -1 +1 @@
-Subproject commit a487c76a5f3ecf2752dabc9e5c3a8866fda28a19
+Subproject commit 3a125a0cb010903e6aa80569a0ca5339424eaf86

src/Cat/Categories/Sets.agda

@@ -4,10 +4,15 @@ module Cat.Categories.Sets where
 
 open import Agda.Primitive
 open import Data.Product
-import Function
+open import Function using (_∘_)
 
-open import Cubical hiding (inverse ; _≃_ {- ; obverse ; recto-verso ; verso-recto -} )
+open import Cubical hiding (_≃_ ; inverse)
-open import Cubical.Univalence using (_≃_ ; ua)
+open import Cubical.Equivalence
+  renaming
+    ( _≅_ to _A≅_ )
+  using
+    (_≃_ ; con ; AreInverses)
+open import Cubical.Univalence
 open import Cubical.GradLemma
 
 open import Cat.Category
@@ -27,7 +32,7 @@ module _ (ℓ : Level) where
     RawCategory.𝟙      SetsRaw = Function.id
     RawCategory._∘_    SetsRaw = Function._∘′_
 
-    open RawCategory SetsRaw
+    open RawCategory SetsRaw hiding (_∘_)
     open Univalence  SetsRaw
 
     isIdentity : IsIdentity Function.id
@@ -62,48 +67,100 @@ module _ (ℓ : Level) where
           -- ordering should be swapped.
           areInverses : IsInverseOf {A = hA} {hB} obverse inverse
           areInverses = proj₂ (proj₂ iso)
-          verso-recto : ∀ a → (inverse Function.∘ obverse) a ≡ a
+          verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a
           verso-recto a i = proj₁ areInverses i a
           recto-verso : ∀ b → (obverse Function.∘ inverse) b ≡ b
           recto-verso b i = proj₂ areInverses i b
 
-      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
+      private
-      univalent = gradLemma obverse inverse verso-recto recto-verso
+        univIso : (A ≡ B) A≅ (A ≃ B)
+        univIso = _≃_.toIsomorphism univalence
+        obverse' : A ≡ B → A ≃ B
+        obverse' = proj₁ univIso
+        inverse' : A ≃ B → A ≡ B
+        inverse' = proj₁ (proj₂ univIso)
+        -- Drop proof of being a set from both sides of an equality.
+        dropP : hA ≡ hB → A ≡ B
+        dropP eq i = proj₁ (eq i)
+        -- Add proof of being a set to both sides of a set-theoretic equivalence
+        -- returning a category-theoretic equivalence.
+        addE : A A≅ B → hA ≅ hB
+        addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair
           where
+          areeqv = proj₂ (proj₂ eqv)
+          asPair =
+            let module Inv = AreInverses areeqv
+            in Inv.verso-recto , Inv.recto-verso
+
         obverse : hA ≡ hB → hA ≅ hB
-        obverse eq = {!res!}
+        obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
-          where
-          -- Problem: How do I extract this equality from `eq`?
-          eqq : A ≡ B
-          eqq = {!!}
-          eq' : A ≃ B
-          eq' = fromEquality eqq
-          -- Problem: Why does this not satisfy the goal?
-          res : hA ≅ hB
-          res = toIsomorphism eq'
 
+        -- Drop proof of being a set form both sides of a category-theoretic
+        -- equivalence returning a set-theoretic equivalence.
+        dropE : hA ≅ hB → A A≅ B
+        dropE eqv = obv , inv , asAreInverses
+          where
+          obv = proj₁ eqv
+          inv = proj₁ (proj₂ eqv)
+          areEq = proj₂ (proj₂ eqv)
+          asAreInverses : AreInverses A B obv inv
+          asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq }
+
+        -- Dunno if this is a thing.
+        isoToEquiv : A A≅ B → A ≃ B
+        isoToEquiv = {!!}
+        -- Add proof of being a set to both sides of an equality.
+        addP : A ≡ B → hA ≡ hB
+        addP p = lemSig (λ X → propPi λ x → propPi (λ y → propIsProp)) hA hB p
         inverse : hA ≅ hB → hA ≡ hB
-        inverse iso = res
+        inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE
-          where
-          eq : A ≡ B
-          eq = ua (fromIsomorphism iso)
 
-          -- Use the fact that being an h-level level is a mere proposition.
+        -- open AreInverses (proj₂ (proj₂ univIso)) renaming
+        --   ( verso-recto to verso-recto'
+        --   ; recto-verso to recto-verso'
+        --   )
+        -- I can just open them but I wanna be able to see the type annotations.
+        verso-recto' : inverse' ∘ obverse' ≡ Function.id
+        verso-recto' = AreInverses.verso-recto (proj₂ (proj₂ univIso))
+        recto-verso' : obverse' ∘ inverse' ≡ Function.id
+        recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso))
+        verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso
+        verso-recto iso = begin
+          obverse (inverse iso) ≡⟨⟩
+          ( addE ∘ _≃_.toIsomorphism
+          ∘ obverse' ∘ dropP ∘ addP
+          ∘ inverse' ∘ isoToEquiv
+          ∘ dropE) iso
+            ≡⟨⟩
+          ( addE ∘ _≃_.toIsomorphism
+          ∘ obverse'
+          ∘ inverse' ∘ isoToEquiv
+          ∘ dropE) iso
+            ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses
+          ( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso
+            ≡⟨ {!!} ⟩ -- should be easy to prove
+                      -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id
+          (addE ∘ dropE) iso
+            ≡⟨⟩
+          iso ∎
+
+        -- Similar to above.
+        recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq
+        recto-verso eq = begin
+          inverse (obverse eq) ≡⟨ {!!} ⟩
+          eq ∎
+
+        -- Use the fact that being an h-level is a mere proposition.
         -- This is almost provable using `Wishlist.isSetIsProp` - although
         -- this creates homogenous paths.
-          isSetEq : (λ i → isSet (eq i)) [ isSetA ≡ isSetB ]
+        isSetEq : (p : A ≡ B) → (λ i → isSet (p i)) [ isSetA ≡ isSetB ]
         isSetEq = {!!}
 
         res : hA ≡ hB
-          proj₁ (res i) = eq i
+        proj₁ (res i) = {!!}
-          proj₂ (res i) = isSetEq i
+        proj₂ (res i) = isSetEq {!!} i
-
+      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
-        -- FIXME Either the name of inverse/obverse is flipped or
+      univalent = {!gradLemma obverse inverse verso-recto recto-verso!}
-        -- recto-verso/verso-recto is flipped.
-        recto-verso : ∀ y → (inverse Function.∘ obverse) y ≡ y
-        recto-verso x = {!!}
-        verso-recto : ∀ x → (obverse Function.∘ inverse) x ≡ x
-        verso-recto x = {!!}
 
     SetsIsCategory : IsCategory SetsRaw
     IsCategory.isAssociative SetsIsCategory = refl

src/Cat/Category.agda

@@ -129,7 +129,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal : Set (ℓa ⊔ ℓb)
   Terminal = Σ Object IsTerminal
 
--- Univalence is indexed by a raw category as well as an identity proof.
+-- | Univalence is indexed by a raw category as well as an identity proof.
+--
+-- FIXME Put this in `RawCategory` and index it on the witness to `isIdentity`.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
   module _ (isIdentity : IsIdentity 𝟙) where
@@ -150,6 +152,8 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 --     iso-is-epi  : Isomorphism f → Epimorphism {X = X} f
 --     iso-is-mono : Isomorphism f → Monomorphism {X = X} f
 --
+-- Sans `univalent` this would be what is referred to as a pre-category in
+-- [HoTT].
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ public
   open Univalence  ℂ public
@@ -248,23 +252,24 @@ module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       -- adverse effects this may have.
       isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
       isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
-      done : x ≡ y
       U : ∀ {a : IsIdentity 𝟙}
         → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
         → (b : Univalent a)
         → Set _
-      U eqwal bbb =
+      U eqwal univ =
         (λ i → Univalent (eqwal i))
-        [ X.univalent ≡ bbb ]
+        [ X.univalent ≡ univ ]
       P : (y : IsIdentity 𝟙)
         → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
-      P y eq = ∀ (b' : Univalent y) → U eq b'
+      P y eq = ∀ (univ : Univalent y) → U eq univ
-      helper : ∀ (b' : Univalent X.isIdentity)
+      p : ∀ (b' : Univalent X.isIdentity)
         → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
-      helper univ = propUnivalent x X.univalent univ
+      p univ = propUnivalent x X.univalent univ
-      foo = pathJ P helper Y.isIdentity isIdentity
+      helper : P Y.isIdentity isIdentity
+      helper = pathJ P p Y.isIdentity isIdentity
       eqUni : U isIdentity Y.univalent
-      eqUni = foo Y.univalent
+      eqUni = helper Y.univalent
+      done : x ≡ y
       IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
       IC.isIdentity    (done i) = isIdentity i
       IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
@@ -275,7 +280,7 @@ module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
 
 -- | Univalent categories
 --
--- Just bundles up the data with witnesses inhabting the propositions.
+-- Just bundles up the data with witnesses inhabiting the propositions.
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     raw            : RawCategory ℓa ℓb
@@ -283,16 +288,30 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
   open IsCategory isCategory public
 
-Category≡ : {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} → Category.raw ℂ ≡ Category.raw 𝔻 → ℂ ≡ 𝔻
+-- The fact that being a category is a mere proposition gives rise to this
-Category≡ {ℂ = ℂ} {𝔻} eq i = record
+-- equality principle for categories.
-  { raw        = eq i
+module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where
+  private
+    module ℂ = Category ℂ
+    module 𝔻 = Category 𝔻
+
+  module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where
+    private
+      P : (target : RawCategory ℓa ℓb) → ({!!} ≡ target) → Set _
+      P _ eq = ∀ isCategory' → (λ i → IsCategory (eq i)) [ ℂ.isCategory ≡ isCategory' ]
+
+      p : P ℂ.raw refl
+      p isCategory' = Propositionality.propIsCategory {!!} {!!}
+
+      -- TODO Make and use heterogeneous version of Category≡
+      isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ]
+      isCategoryEq = {!!}
+
+    Category≡ : ℂ ≡ 𝔻
+    Category≡ i = record
+      { raw        = rawEq i
       ; isCategory = isCategoryEq i
       }
-  where
-  open Category
-  module ℂ = Category ℂ
-  isCategoryEq : (λ i → IsCategory (eq i)) [ isCategory ℂ ≡ isCategory 𝔻 ]
-  isCategoryEq = {!!}
 
 -- | Syntax for arrows- and composition in a given category.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where

src/Cat/Category/Monad.agda

@@ -735,7 +735,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         m ∎
         where
         lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
-        lem = verso-recto Monoidal≃Kleisli
+        lem = {!!} -- verso-recto Monoidal≃Kleisli
         t : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _}
           → a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b ≡ a ∘ b
         t {a = a} {b} = cong (λ φ → a ∘ φ ∘ b) lem
@@ -763,7 +763,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
         m ∎
         where
-        t = cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli)
+        t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli)
 
       voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth
       voe-isEquiv = gradLemma forth back forthEq backEq

src/Cat/Category/Yoneda.agda

@@ -29,7 +29,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
     --
     -- In stead we'll use an ad-hoc definition -- which is definitionally
     -- equivalent to that other one.
-    _⇑_ = CatExponential.prodObj
+    _⇑_ = CatExponential.object
 
     module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
       fmap : Transformation (prshf A) (prshf B)

src/Cat/Wishlist.agda

@@ -4,12 +4,13 @@ open import Level
 open import Cubical.NType
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
+open import Cubical.NType.Properties public using (propHasLevel)
+
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
 
 module _ {ℓ : Level} {A : Set ℓ} where
-  -- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I
-  -- can't find it.
-  postulate propHasLevel : ∀ n → isProp (HasLevel n A)
-
   isSetIsProp : isProp (isSet A)
   isSetIsProp = propHasLevel (S (S ⟨-2⟩))
+
+  propIsProp : isProp (isProp A)
+  propIsProp = propHasLevel (S ⟨-2⟩)