diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda
index f411fffa29..ee86bf91ea 100644
--- 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
index fce7c195fd..a9737470c3 100644
--- 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)
diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda
index ac14f51b41..98facb7741 100644
--- a/Cubical/Categories/Presheaf/Representable.agda
+++ b/Cubical/Categories/Presheaf/Representable.agda
@@ -1,14 +1,37 @@
 {-# OPTIONS --safe #-}
+{-
+
+    This file defines 3 equivalent formulations of when a presheaf P is
+    representable:
+
+    1. When there is a natural isomorphism with some representable C [-, A ]
+
+    2. When there is a terminal element of the category of elements of P
+
+    3. When there is a universal element η ∈ P A, i.e., that composing with
+       η is an equivalence between P B and C [ B , A ].
+
+    The equivalence between 2 and 3 is mostly currying/symmetry of
+    equations. The equivalence between 1 and 3 follows from the Yoneda
+    lemma.
+
+    3 is the most convenient to construct in applications and so is
+    implemented with a custom record type UniversalElement and is
+    generally preferable when formulating universal properties.
+
+-}
 module Cubical.Categories.Presheaf.Representable where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.Reflection.RecordEquiv
 
-open import Cubical.Categories.Category
+open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Constructions.Elements
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Functors
@@ -24,6 +47,8 @@ private
 
 open Category
 open Contravariant
+open NatIso
+open isIsoC
 
 -- | A representation of a presheaf is an object whose image under the
 -- | Yoneda embedding is isomorphic to P
@@ -31,200 +56,174 @@ open Contravariant
 -- | Lifts don't appear in practice because we usually use universal
 -- | elements instead
 module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
-  Representation : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  Representation : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp))
   Representation =
     Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P
 
-  Representable : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  Representable : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp))
   Representable = ∥ Representation ∥₁
 
   Elements = ∫ᴾ_ {C = C} P
-  -- | By the Yoneda lemma, the data of a representation is equivalent
-  -- | to just specifying a universal element of the presheaf
-  UniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
-  UniversalElement = Terminal Elements
 
-  hasUniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
-  hasUniversalElement = ∥ UniversalElement ∥₁
+  TerminalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  TerminalElement = Terminal Elements
 
-  -- A packaged record version that is easier to use
-  record isUniversal (η : Elementᴾ {C = C} P) : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
-         where
-    private
-      vertex = η .fst
-      element = η .snd
-    field
-      coinduction : ∀ {b} → (P ⟅ b ⟆) .fst → C [ b , vertex ]
-      commutes : ∀ {b} (ϕ : (P ⟅ b ⟆) .fst)
-               → element ∘ᴾ⟨ C , P ⟩ coinduction ϕ ≡ ϕ
-      is-uniq : ∀ {b} (ϕ : (P ⟅ b ⟆) .fst) f
-              → (element ∘ᴾ⟨ C , P ⟩ f ≡ ϕ)
-              → f ≡ coinduction ϕ
-
-  record UnivElt : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) where
+  hasTerminalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  hasTerminalElement = ∥ TerminalElement ∥₁
+
+  isUniversal : (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst)
+              → Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  isUniversal vertex element =
+    ∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ C , P ⟩ f
+
+  isPropIsUniversal : ∀ vertex element → isProp (isUniversal vertex element)
+  isPropIsUniversal vertex element = isPropΠ (λ _ → isPropIsEquiv _)
+
+  record UniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) where
     field
       vertex : C .ob
       element : (P ⟅ vertex ⟆) .fst
-      universal : isUniversal (vertex , element)
-
-  open UnivElt
-  open isUniversal
-
-  elementᴾ : UnivElt → Elementᴾ {C = C} P
-  elementᴾ η = (η .vertex , η .element)
-
-  private
-    univEltMor : ∀ η {η' : Elementᴾ {C = C} P}
-               → (η'-univ : isUniversal η')
-               → C [ η .fst , η' .fst ]
-    univEltMor η η'-univ = η'-univ .coinduction (η .snd)
-
-    univEltLemma : ∀ {η η' : Elementᴾ {C = C} P}
-                 → (η-univ : isUniversal η)
-                 → (η'-univ : isUniversal η')
-                 → univEltMor η η'-univ ∘⟨ C ⟩ univEltMor η' η-univ ≡ C .id
-    univEltLemma {η}{η'} η-univ η'-univ =
-      η'-univ .coinduction (η .snd) ∘⟨ C ⟩ η-univ .coinduction (η' .snd)
-        ≡⟨ η'-univ .is-uniq (η' .snd) _ lem ⟩
-      η'-univ .coinduction (η' .snd)
-        ≡⟨ sym (η'-univ .is-uniq _ (C .id) (∘ᴾId C P (η' .snd))) ⟩
-      C .id ∎ where
-
-      lem : (η' .snd
-               ∘ᴾ⟨ C , P ⟩ (η'-univ .coinduction (η .snd)
-               ∘⟨ C ⟩ η-univ .coinduction (η' .snd)))
-            ≡ η' .snd
-      lem =
-        ∘ᴾAssoc C P _ _ _
-        ∙ (λ i → η'-univ .commutes (η .snd) i ∘ᴾ⟨ C , P ⟩ η-univ .coinduction (η' .snd))
-        ∙ η-univ .commutes _
-
-  univEltIso : ∀ {η η' : Elementᴾ {C = C} P} → isUniversal η → isUniversal η'
-             → CatIso C (η .fst) (η' .fst)
-  univEltIso {η}{η'} η-univ η'-univ .fst = univEltMor η η'-univ
-  univEltIso {η}{η'} η-univ η'-univ .snd .isIso.inv = univEltMor η' η-univ
-  univEltIso {η}{η'} η-univ η'-univ .snd .isIso.sec = univEltLemma η-univ η'-univ
-  univEltIso {η}{η'} η-univ η'-univ .snd .isIso.ret = univEltLemma η'-univ η-univ
-
-  -- First the logical equivalence
-  isTerminalElement→isUniversal : ∀ {η : Elementᴾ {C = C} P}
-                                → isTerminal Elements η → isUniversal η
-  isTerminalElement→isUniversal {η} term .coinduction ϕ = term (_ , ϕ) .fst .fst
-  isTerminalElement→isUniversal term .commutes ϕ = sym (term (_ , ϕ) .fst .snd)
-  isTerminalElement→isUniversal term .is-uniq ϕ f commutes i =
-    term (_ , ϕ) .snd (f , sym commutes) (~ i) .fst
-
-  isUniversal→isTerminalElement : ∀ {η : Elementᴾ {C = C} P} → isUniversal η
-                                → isTerminal Elements η
-  isUniversal→isTerminalElement η-univ ϕ .fst .fst =
-    η-univ .coinduction (ϕ .snd)
-  isUniversal→isTerminalElement η-univ ϕ .fst .snd =
-    sym (η-univ .commutes (ϕ .snd))
-  isUniversal→isTerminalElement η-univ ϕ .snd f =
-    Σ≡Prop (λ x → (P ⟅ _ ⟆) .snd _ _)
-           (sym (η-univ .is-uniq (ϕ .snd) (f .fst) (sym (f .snd))))
-
-  isPropIsUniversal : ∀ η → isProp (isUniversal η)
-  isPropIsUniversal η =
-    isPropRetract isUniversal→isTerminalElement
-                  isTerminalElement→isUniversal
-                  reason
-                  (isPropIsTerminal Elements η) where
-    reason : (x : isUniversal (η .fst , η .snd))
-           → isTerminalElement→isUniversal (isUniversal→isTerminalElement x) ≡ x
-    reason η-univ i .coinduction ϕ = η-univ .coinduction ϕ
-    reason η-univ i .commutes ϕ = η-univ .commutes ϕ
-    reason η-univ i .is-uniq ϕ f commutes = η-univ .is-uniq ϕ f commutes
-
-  UniversalElement→UnivElt : UniversalElement → UnivElt
-  UniversalElement→UnivElt η .vertex = η .fst .fst
-  UniversalElement→UnivElt η .element = η .fst .snd
-  UniversalElement→UnivElt η .universal = isTerminalElement→isUniversal (η .snd)
-
-  UnivElt→UniversalElement : UnivElt → UniversalElement
-  UnivElt→UniversalElement η .fst .fst = η .vertex
-  UnivElt→UniversalElement η .fst .snd = η .element
-  UnivElt→UniversalElement η .snd = isUniversal→isTerminalElement (η .universal)
-
-  UniversalElement≅UnivElt : Iso UniversalElement UnivElt
-  UniversalElement≅UnivElt .Iso.fun = UniversalElement→UnivElt
-  UniversalElement≅UnivElt .Iso.inv = UnivElt→UniversalElement
-  UniversalElement≅UnivElt .Iso.rightInv η = refl
-  UniversalElement≅UnivElt .Iso.leftInv η =
-    Σ≡Prop (isPropIsTerminal Elements) refl
+      universal : isUniversal vertex element
+
+  unquoteDecl UniversalElementIsoΣ =
+    declareRecordIsoΣ UniversalElementIsoΣ (quote UniversalElement)
 
-  open NatTrans
-  isTerminalElement→YoIso : (η : Terminal Elements)
-    → Cubical.Categories.Category.isIso
-       (PresheafCategory C (ℓ-max ℓh ℓp))
-       (Iso.inv (yonedaᴾ* {C = C} P (η .fst .fst)) (η .fst .snd))
-  isTerminalElement→YoIso ((A , η) , η-univ) =
-    FUNCTORIso (C ^op) (SET (ℓ-max ℓh ℓp)) _ pointwise where
-    pointwise : ∀ c →
-      Cubical.Categories.Category.isIso (SET (ℓ-max ℓh ℓp))
-        (Iso.inv (yonedaᴾ* {C = C} P A) η ⟦ c ⟧)
-    pointwise c .isIso.inv ϕ = lift (η-univ (_ , ϕ .lower) .fst .fst)
-    pointwise c .isIso.sec =
-      funExt (λ ϕ i → lift (η-univ (_ , ϕ .lower) .fst .snd (~ i)))
-    pointwise c .isIso.ret =
-      funExt (λ f i →
-        lift (η-univ (_ , η ∘ᴾ⟨ C , P ⟩ f .lower)
-              .snd (f .lower , refl) i .fst))
-
-  YoIso→isTerminalElement :
-    ∀ A
-    → (i : PshIso C (C [-, A ]) P)
-    → isTerminal Elements (A , (i .fst .N-ob A (lift (C .id)) .lower))
-  YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret) (B , ϕ) .fst .fst =
-    P→YoA .N-ob B (lift ϕ) .lower
-  YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret) (B , ϕ) .fst .snd =
-    (λ i → (sec (~ i) .N-ob B (lift ϕ)) .lower)
-    ∙ (λ i → YoA→P .N-ob B (lift (C .⋆IdR (P→YoA .N-ob B (lift ϕ) .lower) (~ i))) .lower)
-    ∙ λ i → YoA→P .N-hom (P→YoA .N-ob B (lift ϕ) .lower) i (lift (C .id)) .lower
-  YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret)
-                            (B , ϕ) .snd
-                            f+ @ (f , ϕ=η∘f)
-    = ∫ᴾhomEqSimpl {C = C}{F = P} ((P→YoA .N-ob B (lift ϕ) .lower) , _) f+
-    (P→YoA .N-ob B (lift ϕ) .lower
-      ≡[ i ]⟨ P→YoA .N-ob B (lift (ϕ=η∘f i)) .lower ⟩
-    P→YoA .N-ob B (lift (YoA→P .N-ob A (lift (C .id)) .lower ∘ᴾ⟨ C , P ⟩ f ))
-      .lower
-      ≡[ i ]⟨ P→YoA .N-hom f i (YoA→P .N-ob A (lift (C .id))) .lower ⟩
-    P→YoA .N-ob A (YoA→P .N-ob A (lift (C .id))) .lower ∘⟨ C ⟩ f
-      ≡[ i ]⟨ ret i .N-ob A (lift (C .id)) .lower ∘⟨ C ⟩ f ⟩
-    C .id ∘⟨ C ⟩ f
-      ≡⟨ C .⋆IdR f ⟩
-    f ∎)
-
-  RepresentationToUniversalElement : Representation → UniversalElement
-  RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .fst .fst = A
-  RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .fst .snd =
-    Iso.fun (yonedaᴾ* P A) YoA→P
-  RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .snd =
-    YoIso→isTerminalElement A (YoA→P , YoA→P-isIso)
-
-  UniversalElementToRepresentation : UniversalElement → Representation
-  UniversalElementToRepresentation ((A , η) , η-univ) .fst = A
-  UniversalElementToRepresentation η-terminal @ ((A , η) , η-univ) .snd =
-    (Iso.inv (yonedaᴾ* P A) η) , isTerminalElement→YoIso η-terminal
+  hasUniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
+  hasUniversalElement = ∥ UniversalElement ∥₁
+
+  open UniversalElement
+
+  -- private
+  --   univEltMor : ∀ η {η' : Elementᴾ {C = C} P}
+  --              → (η'-univ : isUniversal η')
+  --              → C [ η .fst , η' .fst ]
+  --   univEltMor η η'-univ = η'-univ .coinduction (η .snd)
+
+  --   univEltLemma : ∀ {η η' : Elementᴾ {C = C} P}
+  --                → (η-univ : isUniversal η)
+  --                → (η'-univ : isUniversal η')
+  --                → univEltMor η η'-univ ∘⟨ C ⟩ univEltMor η' η-univ ≡ C .id
+  --   univEltLemma {η}{η'} η-univ η'-univ =
+  --     η'-univ .coinduction (η .snd) ∘⟨ C ⟩ η-univ .coinduction (η' .snd)
+  --       ≡⟨ η'-univ .is-uniq (η' .snd) _ lem ⟩
+  --     η'-univ .coinduction (η' .snd)
+  --       ≡⟨ sym (η'-univ .is-uniq _ (C .id) (∘ᴾId C P (η' .snd))) ⟩
+  --     C .id ∎ where
+
+  --     lem : (η' .snd
+  --              ∘ᴾ⟨ C , P ⟩ (η'-univ .coinduction (η .snd)
+  --              ∘⟨ C ⟩ η-univ .coinduction (η' .snd)))
+  --           ≡ η' .snd
+  --     lem =
+  --       ∘ᴾAssoc C P _ _ _
+  --       ∙ (λ i → η'-univ .commutes (η .snd) i ∘ᴾ⟨ C , P ⟩ η-univ .coinduction (η' .snd))
+  --       ∙ η-univ .commutes _
+
+  -- univEltIso : ∀ {η η' : Elementᴾ {C = C} P} → isUniversal η → isUniversal η'
+  --            → CatIso C (η .fst) (η' .fst)
+  -- univEltIso {η}{η'} η-univ η'-univ .fst = univEltMor η η'-univ
+  -- univEltIso {η}{η'} η-univ η'-univ .snd .isIso.inv = univEltMor η' η-univ
+  -- univEltIso {η}{η'} η-univ η'-univ .snd .isIso.sec = univEltLemma η-univ η'-univ
+  -- univEltIso {η}{η'} η-univ η'-univ .snd .isIso.ret = univEltLemma η'-univ η-univ
+
+  -- | The equivalence between Representation and UniversalElement is
+  -- | a corollary of the Yoneda lemma
+  representationToUniversalElement : Representation → UniversalElement
+  representationToUniversalElement repr .vertex = repr .fst
+  representationToUniversalElement repr .element =
+    Iso.fun (yonedaᴾ* {C = C} P (repr .fst)) (repr .snd .trans)
+  representationToUniversalElement repr .universal A =
+    transport (λ i → isEquiv (lem i)) (isoToIsEquiv anIso)
+    where
+    lem :
+      Path (C [ A , repr .fst ] → _)
+      (λ f → (repr .snd .trans ⟦ A ⟧) (lift f) .lower)
+      (λ f → (Iso.inv (yonedaᴾ* {C = C} P (repr .fst))
+             (Iso.fun (yonedaᴾ* P (repr .fst))
+                      (repr .snd .trans)) ⟦ A ⟧)
+             (lift f) .lower)
+    lem = funExt (λ f i →
+      (yonedaᴾ* {C = C} P (repr .fst)
+        .Iso.leftInv (repr .snd .trans) (~ i) ⟦ A ⟧)
+      (lift f) .lower)
+
+    anIso : Iso (C [ A , repr .fst ]) (fst (Functor.F-ob P A))
+    anIso .Iso.fun f = (repr .snd .trans ⟦ A ⟧) (lift f) .lower
+    anIso .Iso.inv p = repr .snd .nIso A .inv (lift p) .lower
+    anIso .Iso.rightInv b =
+      cong lower (funExt⁻ (repr .snd .nIso A .sec) (lift b))
+    anIso .Iso.leftInv a =
+      cong lower (funExt⁻ (repr .snd .nIso A .ret) (lift a))
+
+  universalElementToRepresentation : UniversalElement → Representation
+  universalElementToRepresentation η .fst = η .vertex
+  universalElementToRepresentation η .snd .trans =
+    yonedaᴾ* {C = C} P (η .vertex) .Iso.inv (η .element)
+  universalElementToRepresentation η .snd .nIso A .inv ϕ =
+    lift (invIsEq (η .universal A) (ϕ .lower))
+  universalElementToRepresentation η .snd .nIso A .sec = funExt (λ ϕ →
+    cong lift (secIsEq (η .universal A) (ϕ .lower)))
+  universalElementToRepresentation η .snd .nIso A .ret = funExt (λ f →
+    cong lift (retIsEq (η .universal A) (f .lower)))
 
   Representation≅UniversalElement : Iso Representation UniversalElement
-  Representation≅UniversalElement .Iso.fun = RepresentationToUniversalElement
-  Representation≅UniversalElement .Iso.inv = UniversalElementToRepresentation
-  Representation≅UniversalElement .Iso.rightInv ((A , η) , _) =
-    Σ≡Prop (isPropIsTerminal Elements)
-           (ΣPathP (refl , yonedaᴾ* {C = C} P A .rightInv η))
-    where open Iso
-  Representation≅UniversalElement .Iso.leftInv (A , YoA→P , _) =
-    ΣPathP (refl , (Σ≡Prop isPropIsIso (yonedaᴾ* {C = C} P A .leftInv YoA→P)))
-    where open Iso
-
-  Representation≅UnivElt : Iso Representation UnivElt
-  Representation≅UnivElt =
-    compIso Representation≅UniversalElement UniversalElement≅UnivElt
-
-  RepresentationToUnivElt : Representation → UnivElt
-  RepresentationToUnivElt = Iso.fun Representation≅UnivElt
-
-  UnivEltToRepresentation : UnivElt → Representation
-  UnivEltToRepresentation = Iso.inv Representation≅UnivElt
+  Representation≅UniversalElement .Iso.fun = representationToUniversalElement
+  Representation≅UniversalElement .Iso.inv = universalElementToRepresentation
+  Representation≅UniversalElement .Iso.rightInv η =
+    isoFunInjective UniversalElementIsoΣ _ _
+      (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _)
+      (yonedaᴾ* {C = C} P (η .vertex) .Iso.rightInv (η .element)))))
+  Representation≅UniversalElement .Iso.leftInv repr =
+    ΣPathP (refl ,
+    (NatIso≡ (cong NatTrans.N-ob
+      (yonedaᴾ* {C = C} P (repr .fst) .Iso.leftInv (repr .snd .trans)))))
+
+  isTerminalToIsUniversal : ∀ {η : Elementᴾ {C = C} P}
+    → isTerminal Elements η → isUniversal (η .fst) (η .snd)
+  isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .fst =
+    term (_ , ϕ) .fst .fst
+  isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .snd =
+    sym (term (_ , ϕ) .fst .snd)
+  isTerminalToIsUniversal {η} term A .equiv-proof ϕ .snd (f , commutes) =
+    Σ≡Prop (λ _ → (P ⟅ A ⟆) .snd _ _)
+           (cong fst (term (A , ϕ) .snd (f , sym commutes)))
+
+  isUniversalToIsTerminal :
+    ∀ (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst)
+    → isUniversal vertex element
+    → isTerminal Elements (vertex , element)
+  isUniversalToIsTerminal vertex element universal ϕ .fst .fst =
+    universal _ .equiv-proof (ϕ .snd) .fst .fst
+  isUniversalToIsTerminal vertex element universal ϕ .fst .snd =
+    sym (universal _ .equiv-proof (ϕ .snd) .fst .snd)
+  isUniversalToIsTerminal vertex element universal ϕ .snd (f , commutes) =
+    Σ≡Prop
+      (λ _ → (P ⟅ _ ⟆) .snd _ _)
+      (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , sym commutes)))
+
+  terminalElementToUniversalElement : TerminalElement → UniversalElement
+  terminalElementToUniversalElement η .vertex = η .fst .fst
+  terminalElementToUniversalElement η .element = η .fst .snd
+  terminalElementToUniversalElement η .universal =
+    isTerminalToIsUniversal (η .snd)
+
+  universalElementToTerminalElement : UniversalElement → TerminalElement
+  universalElementToTerminalElement η .fst .fst = η .vertex
+  universalElementToTerminalElement η .fst .snd = η .element
+  universalElementToTerminalElement η .snd =
+    isUniversalToIsTerminal (η .vertex) (η .element) (η .universal)
+
+  TerminalElement≅UniversalElement : Iso TerminalElement UniversalElement
+  TerminalElement≅UniversalElement .Iso.fun = terminalElementToUniversalElement
+  TerminalElement≅UniversalElement .Iso.inv = universalElementToTerminalElement
+  TerminalElement≅UniversalElement .Iso.rightInv η =
+    isoFunInjective UniversalElementIsoΣ _ _
+    (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) refl)))
+  TerminalElement≅UniversalElement .Iso.leftInv η =
+    Σ≡Prop (isPropIsTerminal Elements) refl
+
+  Representation≅TerminalElement : Iso Representation TerminalElement
+  Representation≅TerminalElement =
+    compIso
+      Representation≅UniversalElement
+      (invIso TerminalElement≅UniversalElement)