Prove Universal elements is prop for univalent cats (#40)

* prove functoriality "commutes" with isoToPath * prove univalence on SET behaves as expected * Univalence of Opposite Cats, Cat of Elements, UnivElt is a Prop
maxsnew · Jul 19, 2023 · 4dc8429 · 4dc8429
1 parent d7a0db1
commit 4dc8429
Show file tree

Hide file tree

Showing 4 changed files with 134 additions and 0 deletions.
diff --git a/Cubical/Categories/Constructions/Elements/More.agda b/Cubical/Categories/Constructions/Elements/More.agda
@@ -0,0 +1,53 @@
+{-# OPTIONS --safe #-}
+
+-- The Category of Elements
+
+module Cubical.Categories.Constructions.Elements.More where
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Isomorphism
+
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Categories.Functor
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Constructions.Elements
+
+import Cubical.Categories.Morphism as Morphism
+import Cubical.Categories.Constructions.Slice as Slice
+
+open import Cubical.Foundations.Isomorphism.More
+open import Cubical.Categories.Isomorphism.More
+open import Cubical.Categories.Instances.Sets.More
+
+open Category
+open Functor
+open isUnivalent
+module _ {ℓ ℓ'} {C : Category ℓ ℓ'} {ℓS}
+                (isUnivC : isUnivalent C) (F : Functor C (SET ℓS)) where
+  open Covariant {C = C}
+
+  isUnivalent∫ : isUnivalent (∫ F)
+  isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
+    ( isoToPath∫
+    , (λ f≅f' → CatIso≡ _ _
+        (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd f' _)
+          (cong fst
+          (secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
+    , λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
+      ( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
+      ∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
+
+    isoToPath∫ : ∀ {c c' f f'}
+               → CatIso (∫ F) (c , f) (c' , f')
+               → (c , f) ≡ (c' , f')
+    isoToPath∫ {f = f} f≅f' = ΣPathP
+      ( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
+      , toPathP ( (λ j → transport (λ i → fst
+                  (F-isoToPath {F = F} isUnivC isUnivalentSET
+                    (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
+                ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
+                ∙ sym (f≅f' .fst .snd)))
diff --git a/Cubical/Categories/Instances/Sets/More.agda b/Cubical/Categories/Instances/Sets/More.agda
@@ -4,7 +4,10 @@ module Cubical.Categories.Instances.Sets.More where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Univalence
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
@@ -13,6 +16,8 @@ open import Cubical.Categories.Bifunctor.Redundant
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Constructions.BinProduct
 
+open import Cubical.Foundations.Isomorphism.More
+
 private
   variable
     ℓ ℓ' : Level
@@ -33,3 +38,12 @@ open Functor
 
 ×Sets : Functor ((SET ℓ) ×C (SET ℓ)) (SET ℓ)
 ×Sets = BifunctorToParFunctor ×SetsBif
+
+module _ {A}{B} (f : CatIso (SET ℓ) A B) a where
+  open isUnivalent
+  univSetβ : transport (cong fst (CatIsoToPath isUnivalentSET f)) a
+             ≡ f .fst a
+  univSetβ = (transportRefl _
+    ∙ transportRefl _
+    ∙ transportRefl _
+    ∙ cong (f .fst) (transportRefl _ ∙ transportRefl _ ))
diff --git a/Cubical/Categories/Isomorphism/More.agda b/Cubical/Categories/Isomorphism/More.agda
@@ -0,0 +1,54 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Isomorphism.More where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.Categories.Isomorphism
+open import Cubical.Foundations.Isomorphism.More
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+
+open Category
+open Functor
+open isUnivalent
+module _ {C : Category ℓC ℓC'} (isUnivC : isUnivalent C) where
+  op-Iso-pathToIso : ∀ {x y : C .ob} (p : x ≡ y)
+                   → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p
+  op-Iso-pathToIso =
+    J (λ y p → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p)
+      (CatIso≡ _ _ refl)
+
+  op-Iso-pathToIso' : ∀ {x y : C .ob} (p : x ≡ y)
+                   → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p
+  op-Iso-pathToIso' =
+    J (λ y p → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p)
+      (CatIso≡ _ _ refl)
+
+  isUnivalentOp : isUnivalent (C ^op)
+  isUnivalentOp .univ x y = isIsoToIsEquiv
+    ( (λ f^op → CatIsoToPath isUnivC (op-Iso f^op))
+    , (λ f^op → CatIso≡ _ _
+        (cong fst
+        (cong op-Iso ((secEq (univEquiv isUnivC _ _) (op-Iso f^op))))))
+    , λ p → cong (CatIsoToPath isUnivC) (op-Iso-pathToIso' p)
+        ∙ retEq (univEquiv isUnivC _ _) p)
+
+module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where
+  module _ (isUnivC : isUnivalent C) (isUnivD : isUnivalent D) where
+    isoToPathC = CatIsoToPath isUnivC
+    isoToPathD = CatIsoToPath isUnivD
+
+    F-isoToPath : {x y : C .ob} → (f : CatIso C x y) →
+      isoToPathD (F-Iso {F = F} f) ≡ cong (F .F-ob) (isoToPathC f)
+    F-isoToPath f = isoFunInjective (equivToIso (univEquiv isUnivD _ _)) _ _
+      ( secEq (univEquiv isUnivD _ _) _
+      ∙ sym (sym (F-pathToIso {F = F} (isoToPathC f))
+      ∙ cong (F-Iso {F = F}) (secEq (univEquiv isUnivC _ _) f)))
diff --git a/Cubical/Categories/Presheaf/More.agda b/Cubical/Categories/Presheaf/More.agda
@@ -3,18 +3,23 @@ module Cubical.Categories.Presheaf.More where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Structure
 
 open import Cubical.Categories.Category
+open import Cubical.Categories.Limits.Terminal
 open import Cubical.Categories.Constructions.Lift
+open import Cubical.Categories.Constructions.Elements
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Presheaf.Base
 open import Cubical.Categories.Presheaf.Representable
 
 open import Cubical.Categories.Instances.Sets.More
+open import Cubical.Categories.Isomorphism.More
+open import Cubical.Categories.Constructions.Elements.More
 
 open Category
 open Functor
@@ -80,3 +85,11 @@ module UniversalElementNotation {ℓo}{ℓh}
     ( (∘ᴾAssoc C P _ _ _
     ∙ cong (action C P _) β)
     ∙ sym β)
+
+module _ {C : Category ℓ ℓ'} (isUnivC : isUnivalent C) (P : Presheaf C ℓS) where
+  open Contravariant
+  isPropUniversalElement : isProp (UniversalElement C P)
+  isPropUniversalElement = isOfHLevelRetractFromIso 1
+    (invIso (TerminalElement≅UniversalElement C P))
+    (isPropTerminal (∫ᴾ_ {C = C} P)
+    (isUnivalentOp (isUnivalent∫ (isUnivalentOp isUnivC) P)))