rename UnivElt to UniversalElement, redefine in terms of isEquiv

agda · Jul 5, 2023 · a3bdc90 · a3bdc90
1 parent 8d05e25
commit a3bdc90
Show file tree

Hide file tree

Showing 3 changed files with 192 additions and 195 deletions.
diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda
@@ -40,8 +40,7 @@ open Category
 open Contravariant
 open Functor
 open NatTrans
-open UnivElt
-open isUniversal
+open UniversalElement
 
 module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
          (F : Functor C D)
@@ -74,9 +73,10 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
     pushEltF .F-seq f g =
       Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst))
 
-    preservesRepresentation : ∀ (η : UnivElt C P)
+    preservesRepresentation : ∀ (η : UniversalElement C P)
                             → Type (ℓ-max (ℓ-max ℓd ℓd') ℓq)
-    preservesRepresentation η = isUniversal D Q (pushElt (elementᴾ _ _ η))
+    preservesRepresentation η = isUniversal D Q (η' .fst) (η' .snd)
+      where η' = pushElt (η .vertex , η .element)
 
     preservesRepresentations : Type _
     preservesRepresentations = ∀ η → preservesRepresentation η
@@ -87,10 +87,10 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
     preservesAnyRepresentation→preservesAllRepresentations :
       ∀ η → preservesRepresentation η → preservesRepresentations
     preservesAnyRepresentation→preservesAllRepresentations η preserves-η η' =
-      isTerminalElement→isUniversal D Q
+      isTerminalToIsUniversal D Q
         (preserveAnyTerminal→PreservesTerminals (∫ᴾ_ {C = C} P)
                                  (∫ᴾ_ {C = D} Q)
                                  pushEltF
-                                 (UnivElt→UniversalElement C P η)
-                                 (isUniversal→isTerminalElement D Q preserves-η)
-                                 (UnivElt→UniversalElement C P η'))
+                                 (universalElementToTerminalElement C P η)
+                                 (isUniversalToIsTerminal D Q _ _ preserves-η)
+                                 (universalElementToTerminalElement C P η'))
diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda
@@ -392,6 +392,4 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
 -- Isomorphism between presheaves of different levels
 PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) (Q : Presheaf C ℓS') → Type _
 PshIso {ℓS = ℓS}{ℓS' = ℓS'} C P Q =
-  CatIso (FUNCTOR (C ^op) (SET (ℓ-max ℓS ℓS')))
-    (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P)
-    (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q)
+  NatIso (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P) (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q)