diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda
index 1dc25f1605..da80ea1b07 100644
--- a/Cubical/Categories/Constructions/BinProduct.agda
+++ b/Cubical/Categories/Constructions/BinProduct.agda
@@ -65,6 +65,12 @@ module _ where
   _×F_ : Functor A C → Functor B D → Functor (A ×C B) (C ×C D)
   _×F_ {A = A} {B = B} G H = G ∘F Fst A B ,F H ∘F Snd A B
 
+Δ : ∀ (C : Category ℓC ℓC') → Functor C (C ×C C)
+Δ C = Id ,F Id
+
+Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C)
+Sym {C = C}{D = D} = Snd C D ,F Fst C D
+
 -- Some useful functors
 module _ (C : Category ℓC ℓC')
          (D : Category ℓD ℓD') where
diff --git a/Cubical/Categories/Constructions/DisplayOverTerminal.agda b/Cubical/Categories/Constructions/DisplayOverTerminal.agda
new file mode 100644
index 0000000000..4c16306266
--- /dev/null
+++ b/Cubical/Categories/Constructions/DisplayOverTerminal.agda
@@ -0,0 +1,31 @@
+{-
+  A category displayed over the terminal category is isomorphic to
+  just a category.
+-}
+
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.DisplayOverTerminal where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Instances.Terminal
+
+
+private
+  variable
+    ℓC ℓ'C ℓD ℓ'D ℓCᴰ ℓ'Cᴰ ℓDᴰ ℓ'Dᴰ : Level
+module _ {ℓ* : Level} (Cᴰ : Categoryᴰ (TerminalCategory {ℓ*}) ℓCᴰ ℓ'Cᴰ) where
+  open Categoryᴰ Cᴰ
+  open Category
+
+  DispOverTerminal→Category : Category ℓCᴰ ℓ'Cᴰ
+  DispOverTerminal→Category .ob = ob[ tt* ]
+  DispOverTerminal→Category .Hom[_,_] = Hom[ refl ][_,_]
+  DispOverTerminal→Category .id = idᴰ
+  DispOverTerminal→Category ._⋆_ = _⋆ᴰ_
+  DispOverTerminal→Category .⋆IdL = ⋆IdLᴰ
+  DispOverTerminal→Category .⋆IdR = ⋆IdRᴰ
+  DispOverTerminal→Category .⋆Assoc = ⋆Assocᴰ
+  DispOverTerminal→Category .isSetHom = isSetHomᴰ
diff --git a/Cubical/Categories/Constructions/Elements.agda b/Cubical/Categories/Constructions/Elements.agda
index e57816682d..c5e1c27c3c 100644
--- a/Cubical/Categories/Constructions/Elements.agda
+++ b/Cubical/Categories/Constructions/Elements.agda
@@ -1,8 +1,9 @@
 {-# OPTIONS --safe #-}
 
--- The Category of Elements
+-- The category of elements of a functor to Set
 
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Path
@@ -86,6 +87,31 @@ module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     F-id (ForgetElements F) = refl
     F-seq (ForgetElements F) _ _ = refl
 
+    module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
+      open isUnivalent
+      isUnivalent∫ : isUnivalent (∫ F)
+      isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
+        ( isoToPath∫
+        , (λ f≅f' → CatIso≡ _ _
+            (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
+              (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 isUnivC isUnivalentSET F
+                        (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
+                    ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
+                    ∙ f≅f' .fst .snd))
+
+
 module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     open Covariant {C = C ^op}
 
diff --git a/Cubical/Categories/Constructions/Free/Category/Quiver.agda b/Cubical/Categories/Constructions/Free/Category/Quiver.agda
new file mode 100644
index 0000000000..cdb3801b20
--- /dev/null
+++ b/Cubical/Categories/Constructions/Free/Category/Quiver.agda
@@ -0,0 +1,162 @@
+-- Free category generated from base objects and generators
+
+-- This time using a "quiver" as the presentation of the generators,
+-- which is better in some applications
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Free.Category.Quiver where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Quiver.Base as Quiver
+open import Cubical.Data.Graph.Base as Graph
+open import Cubical.Data.Graph.Displayed as Graph hiding (Section)
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.BinProduct as BP
+open import Cubical.Categories.UnderlyingGraph hiding (Interp)
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Instances.Path
+open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
+
+open import Cubical.Categories.Displayed.Section.Base as Cat
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' ℓj ℓ : Level
+    ℓC ℓC' ℓCᴰ ℓCᴰ' : Level
+
+open Category
+open Functor
+open QuiverOver
+
+module _ (Q : Quiver ℓg ℓg') where
+  data Exp : Q .fst → Q .fst → Type (ℓ-max ℓg ℓg') where
+    ↑_   : ∀ g → Exp (Q .snd .dom g) (Q .snd .cod g)
+    idₑ  : ∀ {A} → Exp A A
+    _⋆ₑ_ : ∀ {A B C} → (e : Exp A B) → (e' : Exp B C) → Exp A C
+    ⋆ₑIdL : ∀ {A B} (e : Exp A B) → idₑ ⋆ₑ e ≡ e
+    ⋆ₑIdR : ∀ {A B} (e : Exp A B) → e ⋆ₑ idₑ ≡ e
+    ⋆ₑAssoc : ∀ {A B C D} (e : Exp A B)(f : Exp B C)(g : Exp C D)
+            → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g)
+    isSetExp : ∀ {A B} → isSet (Exp A B)
+
+  FreeCat : Category _ _
+  FreeCat .ob = Q .fst
+  FreeCat .Hom[_,_] = Exp
+  FreeCat .id = idₑ
+  FreeCat ._⋆_ = _⋆ₑ_
+  FreeCat .⋆IdL = ⋆ₑIdL
+  FreeCat .⋆IdR = ⋆ₑIdR
+  FreeCat .⋆Assoc = ⋆ₑAssoc
+  FreeCat .isSetHom = isSetExp
+
+  Interp : (𝓒 : Category ℓc ℓc') → Type (ℓ-max (ℓ-max (ℓ-max ℓg ℓg') ℓc) ℓc')
+  Interp 𝓒 = HetQG Q (Cat→Graph 𝓒)
+
+  η : Interp FreeCat
+  η HetQG.$g x = x
+  η HetQG.<$g> e = ↑ e
+
+  module _ {C : Category ℓC ℓC'}
+           (ı : Interp C)
+           (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
+    Interpᴰ : Type _
+    Interpᴰ = HetSection ı (Categoryᴰ→Graphᴰ Cᴰ)
+
+  -- the eliminator constructs a *global* section. Use reindexing if
+  -- you want a local section
+  module _ (Cᴰ : Categoryᴰ FreeCat ℓCᴰ ℓCᴰ')
+           (ıᴰ : Interpᴰ η Cᴰ)
+           where
+    open HetSection
+    open Section
+    private module Cᴰ = Categoryᴰ Cᴰ
+
+    elim-F-homᴰ : ∀ {d d'} → (f : FreeCat .Hom[_,_] d d') →
+      Cᴰ.Hom[ f ][ ıᴰ $gᴰ d , (ıᴰ $gᴰ d') ]
+    elim-F-homᴰ (↑ g) = ıᴰ <$g>ᴰ g
+    elim-F-homᴰ idₑ = Cᴰ.idᴰ
+    elim-F-homᴰ (f ⋆ₑ g) = elim-F-homᴰ f Cᴰ.⋆ᴰ elim-F-homᴰ g
+    elim-F-homᴰ (⋆ₑIdL f i) = Cᴰ.⋆IdLᴰ (elim-F-homᴰ f) i
+    elim-F-homᴰ (⋆ₑIdR f i) = Cᴰ.⋆IdRᴰ (elim-F-homᴰ f) i
+    elim-F-homᴰ (⋆ₑAssoc f f₁ f₂ i) =
+      Cᴰ.⋆Assocᴰ (elim-F-homᴰ f) (elim-F-homᴰ f₁) (elim-F-homᴰ f₂) i
+    elim-F-homᴰ (isSetExp f g p q i j) = isOfHLevel→isOfHLevelDep 2
+      (λ x → Cᴰ.isSetHomᴰ)
+      (elim-F-homᴰ f) (elim-F-homᴰ g)
+      (cong elim-F-homᴰ p) (cong elim-F-homᴰ q)
+      (isSetExp f g p q)
+      i j
+
+    elim : GlobalSection Cᴰ
+    elim .F-obᴰ = ıᴰ $gᴰ_
+    elim .F-homᴰ = elim-F-homᴰ
+    elim .F-idᴰ = refl
+    elim .F-seqᴰ _ _ = refl
+
+  -- The elimination principle for global sections implies an
+  -- elimination principle for local sections, this requires reindex
+  -- so caveat utilitor
+  module _ {C : Category ℓC ℓC'}
+           (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+           (F : Functor FreeCat C)
+           (ıᴰ : Interpᴰ (compGrHomHetQG (Functor→GraphHom F) η) Cᴰ)
+           where
+    private
+      open HetSection
+      F*Cᴰ = Reindex.reindex Cᴰ F
+      ıᴰ' : Interpᴰ η F*Cᴰ
+      ıᴰ' ._$gᴰ_ = ıᴰ $gᴰ_
+      ıᴰ' ._<$g>ᴰ_ = ıᴰ <$g>ᴰ_
+
+    elimLocal : Section F Cᴰ
+    elimLocal = GlobalSectionReindex→Section Cᴰ F (elim F*Cᴰ ıᴰ')
+
+  -- Elimination principle implies the recursion principle, which
+  -- allows for non-dependent functors to be defined
+  module _ {C : Category ℓC ℓC'} (ı : Interp C) where
+    open HetQG
+    private
+      ıᴰ : Interpᴰ η (weaken FreeCat C)
+      ıᴰ .HetSection._$gᴰ_ = ı .HetQG._$g_
+      ıᴰ .HetSection._<$g>ᴰ_ = ı .HetQG._<$g>_
+
+    rec : Functor FreeCat C
+    rec = Wk.introS⁻ (elim (weaken FreeCat C) ıᴰ)
+
+  -- Elimination principle also implies the uniqueness principle,
+  -- i.e., η law for sections/functors out of the free category
+  -- this version is for functors
+  module _
+    {C : Category ℓC ℓC'}
+    (F G : Functor FreeCat C)
+    (agree-on-gen :
+      -- todo: some notation would simplify this considerably
+      Interpᴰ (compGrHomHetQG (Functor→GraphHom (F BP.,F G)) η) (PathC C))
+    where
+    FreeCatFunctor≡ : F ≡ G
+    FreeCatFunctor≡ = PathReflection (elimLocal (PathC C) _ agree-on-gen)
+
+  -- TODO: add analogous principle for Sections using PathCᴰ
+-- -- co-unit of the 2-adjunction
+module _ {𝓒 : Category ℓc ℓc'} where
+  private
+    Exp⟨𝓒⟩ = FreeCat (Cat→Quiver 𝓒)
+  ε : Functor Exp⟨𝓒⟩ 𝓒
+  ε = rec (Cat→Quiver 𝓒)
+    (record { _$g_ = λ z → z ; _<$g>_ = λ e → e .snd .snd })
+
+  ε-reasoning : {𝓓 : Category ℓd ℓd'}
+            → (𝓕 : Functor 𝓒 𝓓)
+            → 𝓕 ∘F ε ≡ rec (Cat→Quiver 𝓒)
+      (record { _$g_ = 𝓕 .F-ob ; _<$g>_ = λ e → 𝓕 .F-hom (e .snd .snd) })
+  ε-reasoning 𝓕 = FreeCatFunctor≡ _ _ _
+    (record { _$gᴰ_ = λ _ → refl ; _<$g>ᴰ_ = λ _ → refl })
diff --git a/Cubical/Categories/Constructions/Opposite.agda b/Cubical/Categories/Constructions/Opposite.agda
new file mode 100644
index 0000000000..4afa7e971c
--- /dev/null
+++ b/Cubical/Categories/Constructions/Opposite.agda
@@ -0,0 +1,40 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.Opposite where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.Categories.Isomorphism
+
+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)
diff --git a/Cubical/Categories/Constructions/TotalCategory.agda b/Cubical/Categories/Constructions/TotalCategory.agda
index 772c440599..6ffd24c31d 100644
--- a/Cubical/Categories/Constructions/TotalCategory.agda
+++ b/Cubical/Categories/Constructions/TotalCategory.agda
@@ -1,74 +1,5 @@
 {-# OPTIONS --safe #-}
 module Cubical.Categories.Constructions.TotalCategory where
 
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-
-open import Cubical.Data.Sigma
-
-open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Instances.Terminal
-
-private
-  variable
-    ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level
-
--- Total category of a displayed category
-module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
-
-  open Category
-  open Categoryᴰ Cᴰ
-  private
-    module C = Category C
-
-  ∫C : Category (ℓ-max ℓC ℓCᴰ) (ℓ-max ℓC' ℓCᴰ')
-  ∫C .ob = Σ _ ob[_]
-  ∫C .Hom[_,_] (_ , xᴰ) (_ , yᴰ) = Σ _ Hom[_][ xᴰ , yᴰ ]
-  ∫C .id = _ , idᴰ
-  ∫C ._⋆_ (_ , fᴰ) (_ , gᴰ) = _ , fᴰ ⋆ᴰ gᴰ
-  ∫C .⋆IdL _ = ΣPathP (_ , ⋆IdLᴰ _)
-  ∫C .⋆IdR _ = ΣPathP (_ , ⋆IdRᴰ _)
-  ∫C .⋆Assoc _ _ _ = ΣPathP (_ , ⋆Assocᴰ _ _ _)
-  ∫C .isSetHom = isSetΣ C.isSetHom (λ _ → isSetHomᴰ)
-
--- Total functor of a displayed functor
-module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
-  {F : Functor C D} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
-  (Fᴰ : Functorᴰ F Cᴰ Dᴰ)
-  where
-
-  open Functor
-  private
-    module Fᴰ = Functorᴰ Fᴰ
-
-  ∫F : Functor (∫C Cᴰ) (∫C Dᴰ)
-  ∫F .F-ob (x , xᴰ) = _ , Fᴰ.F-obᴰ xᴰ
-  ∫F .F-hom (_ , fᴰ) = _ , Fᴰ.F-homᴰ fᴰ
-  ∫F .F-id = ΣPathP (_ , Fᴰ.F-idᴰ)
-  ∫F .F-seq _ _ = ΣPathP (_ , (Fᴰ.F-seqᴰ _ _))
-
--- Projections out of the total category
-module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
-  open Functor
-  open Functorᴰ
-
-  Fst : Functor (∫C Cᴰ) C
-  Fst .F-ob = fst
-  Fst .F-hom = fst
-  Fst .F-id = refl
-  Fst .F-seq =
-    λ f g → cong {x = f ⋆⟨ ∫C Cᴰ ⟩ g} fst refl
-
-  -- Functor into the total category
-  module _ {D : Category ℓD ℓD'}
-           (F : Functor D C)
-           (Fᴰ : Functorᴰ F (Unitᴰ D) Cᴰ)
-           where
-    intro : Functor D (∫C Cᴰ)
-    intro .F-ob d = F ⟅ d ⟆ , Fᴰ .F-obᴰ _
-    intro .F-hom f = (F ⟪ f ⟫) , (Fᴰ .F-homᴰ _)
-    intro .F-id = ΣPathP (F .F-id , Fᴰ .F-idᴰ)
-    intro .F-seq f g = ΣPathP (F .F-seq f g , Fᴰ .F-seqᴰ _ _)
+open import Cubical.Categories.Constructions.TotalCategory.Base public
+open import Cubical.Categories.Constructions.TotalCategory.Properties public
diff --git a/Cubical/Categories/Constructions/TotalCategory/Base.agda b/Cubical/Categories/Constructions/TotalCategory/Base.agda
new file mode 100644
index 0000000000..10a8aaf141
--- /dev/null
+++ b/Cubical/Categories/Constructions/TotalCategory/Base.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.TotalCategory.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level
+
+-- Total category of a displayed category
+module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
+
+  open Category
+  open Categoryᴰ Cᴰ
+  private
+    module C = Category C
+
+  ∫C : Category (ℓ-max ℓC ℓCᴰ) (ℓ-max ℓC' ℓCᴰ')
+  ∫C .ob = Σ _ ob[_]
+  ∫C .Hom[_,_] (_ , xᴰ) (_ , yᴰ) = Σ _ Hom[_][ xᴰ , yᴰ ]
+  ∫C .id = _ , idᴰ
+  ∫C ._⋆_ (_ , fᴰ) (_ , gᴰ) = _ , fᴰ ⋆ᴰ gᴰ
+  ∫C .⋆IdL _ = ΣPathP (_ , ⋆IdLᴰ _)
+  ∫C .⋆IdR _ = ΣPathP (_ , ⋆IdRᴰ _)
+  ∫C .⋆Assoc _ _ _ = ΣPathP (_ , ⋆Assocᴰ _ _ _)
+  ∫C .isSetHom = isSetΣ C.isSetHom (λ _ → isSetHomᴰ)
+
+-- Total functor of a displayed functor
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  {F : Functor C D} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  (Fᴰ : Functorᴰ F Cᴰ Dᴰ)
+  where
+
+  open Functor
+  private
+    module Fᴰ = Functorᴰ Fᴰ
+
+  ∫F : Functor (∫C Cᴰ) (∫C Dᴰ)
+  ∫F .F-ob (x , xᴰ) = _ , Fᴰ.F-obᴰ xᴰ
+  ∫F .F-hom (_ , fᴰ) = _ , Fᴰ.F-homᴰ fᴰ
+  ∫F .F-id = ΣPathP (_ , Fᴰ.F-idᴰ)
+  ∫F .F-seq _ _ = ΣPathP (_ , (Fᴰ.F-seqᴰ _ _))
diff --git a/Cubical/Categories/Constructions/TotalCategory/Properties.agda b/Cubical/Categories/Constructions/TotalCategory/Properties.agda
new file mode 100644
index 0000000000..2c19d316b1
--- /dev/null
+++ b/Cubical/Categories/Constructions/TotalCategory/Properties.agda
@@ -0,0 +1,121 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.TotalCategory.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Constructions.TotalCategory.Base
+open import Cubical.Categories.Displayed.Instances.Terminal.Base
+import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level
+
+-- Projections out of the total category
+module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
+  open Functor
+  open Functorᴰ
+  open Section
+
+  Fst : Functor (∫C Cᴰ) C
+  Fst .F-ob = fst
+  Fst .F-hom = fst
+  Fst .F-id = refl
+  Fst .F-seq =
+    λ f g → cong {x = f ⋆⟨ ∫C Cᴰ ⟩ g} fst refl
+
+  Snd : Section Fst Cᴰ
+  Snd .F-obᴰ      = snd
+  Snd .F-homᴰ     = snd
+  Snd .F-idᴰ      = refl
+  Snd .F-seqᴰ _ _ = refl
+
+-- A section
+{-
+          Cᴰ
+        ↗ |
+       /  |
+   s  /   |
+     /    |
+    /     ↓
+   E ---→ C
+       F
+-}
+--
+-- is equivalent to a functor
+--    intro' F s
+-- E ------------→ ∫ C Cᴰ
+--
+  module _ {D : Category ℓD ℓD'}
+           (F : Functor D C)
+           (Fᴰ : Section F Cᴰ)
+           where
+    -- should this be "intro" or "corec"? style decision needed.
+    intro : Functor D (∫C Cᴰ)
+    intro .F-ob d = F ⟅ d ⟆ , Fᴰ .F-obᴰ _
+    intro .F-hom f = (F ⟪ f ⟫) , (Fᴰ .F-homᴰ _)
+    intro .F-id = ΣPathP (F .F-id , Fᴰ .F-idᴰ)
+    intro .F-seq f g = ΣPathP (F .F-seq f g , Fᴰ .F-seqᴰ _ _)
+
+  module _ {D : Category ℓD ℓD'}
+           {F : Functor C D}
+           {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+           (Fᴰ : Functorᴰ F Cᴰ Dᴰ)
+         where
+
+-- A displayed functor
+--
+--     Fᴰ
+-- Cᴰ -----→ Dᴰ
+-- |         |
+-- |         |
+-- ↓         ↓
+-- C ------→ D
+--     F
+--
+-- is equivalent to a section
+{-
+               Dᴰ
+             ↗ |
+            /  |
+   elim Fᴰ /   |
+          /    |
+         /     ↓
+   ∫ Cᴰ  ----→ D
+        F ∘F Fst
+-}
+    open Functorᴰ
+    private
+      module Dᴰ = Categoryᴰ Dᴰ
+      module R = HomᴰReasoning Dᴰ
+    elim : Section (F ∘F Fst) Dᴰ
+    elim = compFunctorᴰSection Fᴰ Snd
+
+  module _ {D : Category ℓD ℓD'}
+           (F : Functor C D)
+           (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ')
+           (Fᴰ : Section (F ∘F Fst) Dᴰ)
+         where
+    open Functorᴰ
+    private
+      module Dᴰ = Categoryᴰ Dᴰ
+      module R = HomᴰReasoning Dᴰ
+    -- this is a recursion principle for an *arbitrary* displayed
+    -- category Cᴰ.
+
+    -- this is a dependent uncurry
+    recᴰ : Functorᴰ F Cᴰ Dᴰ
+    recᴰ .F-obᴰ {x} xᴰ = Fᴰ .F-obᴰ (x , xᴰ)
+    recᴰ .F-homᴰ {f = f} fᴰ = Fᴰ .F-homᴰ (f , fᴰ)
+    recᴰ .F-idᴰ = R.≡[]-rectify (Fᴰ .F-idᴰ)
+    recᴰ .F-seqᴰ {x} {y} {z} {f} {g} {xᴰ} {yᴰ} {zᴰ} fᴰ gᴰ =
+      R.≡[]-rectify (Fᴰ .F-seqᴰ (f , fᴰ) (g , gᴰ))
+
diff --git a/Cubical/Categories/Constructions/Vertical.agda b/Cubical/Categories/Constructions/Vertical.agda
new file mode 100644
index 0000000000..5b189349cc
--- /dev/null
+++ b/Cubical/Categories/Constructions/Vertical.agda
@@ -0,0 +1,24 @@
+{-
+  The vertical category over an object from a displayed
+  category. Also sometimes called the "fiber"
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.Vertical where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Constructions.Reindex.Base
+open import Cubical.Categories.Constructions.DisplayOverTerminal
+open import Cubical.Categories.Instances.Terminal
+
+private
+  variable
+    ℓC ℓ'C ℓD ℓ'D ℓCᴰ ℓ'Cᴰ ℓDᴰ ℓ'Dᴰ : Level
+
+module _ {C : Category ℓC ℓ'C} (Cᴰ : Categoryᴰ C ℓCᴰ ℓ'Cᴰ) where
+  open Category C
+  open Categoryᴰ Cᴰ
+  VerticalCategory : ob → Category ℓCᴰ ℓ'Cᴰ
+  VerticalCategory c = DispOverTerminal→Category
+    (reindex Cᴰ (FunctorFromTerminal {ℓ* = ℓ-zero} c))
diff --git a/Cubical/Categories/Displayed/Cartesian.agda b/Cubical/Categories/Displayed/Cartesian.agda
index c8e3348f03..af997c155a 100644
--- a/Cubical/Categories/Displayed/Cartesian.agda
+++ b/Cubical/Categories/Displayed/Cartesian.agda
@@ -11,11 +11,11 @@ open import Cubical.HITs.PropositionalTruncation as PT
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Properties
 import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.Vertical
 
 module Cubical.Categories.Displayed.Cartesian where
 
diff --git a/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda b/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
index b65ceef930..bf150c4887 100644
--- a/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
+++ b/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
@@ -13,7 +13,7 @@ open import Cubical.Categories.Instances.Terminal
 open import Cubical.Categories.Functor
 
 open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Properties
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base
 open import Cubical.Categories.Constructions.TotalCategory
 
 private
@@ -123,4 +123,4 @@ private
 
       weaken' : Categoryᴰ C (ℓ-max (ℓ-max ℓ-zero ℓC) ℓD)
                  (ℓ-max (ℓ-max ℓ-zero ℓC') ℓD')
-      weaken' = ∃F (Category→DispOverTerminal D) F
+      weaken' = ∃F (weaken _ D) F
diff --git a/Cubical/Categories/Displayed/Constructions/PropertyOver.agda b/Cubical/Categories/Displayed/Constructions/PropertyOver.agda
index a1cd569ac8..43f78c9e66 100644
--- a/Cubical/Categories/Displayed/Constructions/PropertyOver.agda
+++ b/Cubical/Categories/Displayed/Constructions/PropertyOver.agda
@@ -8,10 +8,10 @@ open import Cubical.Data.Unit
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Functor
-open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Constructions.StructureOver
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Constructions.StructureOver.Base
 
 private
   variable
diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
new file mode 100644
index 0000000000..f1a292884d
--- /dev/null
+++ b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
@@ -0,0 +1,159 @@
+{-
+
+   Given any displayed cat and functor to the base
+
+           A
+           |
+           |
+           |
+           |
+           ↓
+   Δ ----→ Γ
+       γ
+
+
+   There is a universal displayed category over Δ equipped with a
+   displayed functor
+
+   γ* A ----→ A
+     |        |
+     |        |
+     |        |
+     |        |
+     ↓        ↓
+     Δ -----→ Γ
+        γ
+
+
+   We write γ* A as reindex A γ*
+
+   The universality says that a section
+
+          γ* A
+        ↗ |
+       /  |
+    M /   |
+     /    |
+    /     ↓
+   Θ ---→ Δ
+       δ
+
+   is equivalent to a section
+
+          A
+        ↗ |
+       /  |
+      /   |
+     /    |
+    /     ↓
+   Θ ---→ Γ
+      δγ
+
+   that factorizes through the universal displayed functor.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Constructions.Reindex.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Unit
+import      Cubical.Data.Equality as Eq
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Constructions.TotalCategory as TotalCat
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Instances.Terminal
+
+private
+  variable
+    ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓD ℓD' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level
+
+module _
+  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') (F : Functor C D)
+  where
+
+  private
+    module R = HomᴰReasoning Dᴰ
+    module C = Category C
+    module D = Category D
+
+  open Categoryᴰ Dᴰ
+  open Functor F
+  open Functorᴰ
+
+  reindex : Categoryᴰ C ℓDᴰ ℓDᴰ'
+  reindex .Categoryᴰ.ob[_] c = ob[ F-ob c ]
+  reindex .Categoryᴰ.Hom[_][_,_] f aᴰ bᴰ = Hom[ F-hom f ][ aᴰ , bᴰ ]
+  reindex .Categoryᴰ.idᴰ = R.reind (sym F-id) idᴰ
+  reindex .Categoryᴰ._⋆ᴰ_ fᴰ gᴰ = R.reind (sym $ F-seq _ _) (fᴰ ⋆ᴰ gᴰ)
+  reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.≡[]-rectify $
+    R.reind-filler-sym (F-seq _ _) _
+      R.[ _ ]∙[ _ ]
+    (R.reind-filler-sym F-id idᴰ R.[ _ ]⋆[ refl ] refl)
+      R.[ _ ]∙[ _ ]
+    ⋆IdLᴰ fᴰ
+  reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.≡[]-rectify $
+    R.reind-filler-sym (F-seq _ _) _
+      R.[ _ ]∙[ _ ]
+    (refl R.[ refl ]⋆[ _ ] R.reind-filler-sym F-id idᴰ)
+      R.[ _ ]∙[ _ ]
+    ⋆IdRᴰ fᴰ
+  reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.≡[]-rectify $
+    R.reind-filler-sym (F-seq _ _) _
+      R.[ _ ]∙[ _ ]
+    (R.reind-filler-sym (F-seq _ _) _ R.[ _ ]⋆[ refl ] refl)
+      R.[ _ ]∙[ _ ]
+    ⋆Assocᴰ fᴰ gᴰ hᴰ
+      R.[ _ ]∙[ _ ]
+    (refl R.[ refl ]⋆[ _ ] R.reind-filler (sym $ F-seq _ _) _)
+      R.[ _ ]∙[ _ ]
+    R.reind-filler (sym $ F-seq _ _) _
+  reindex .Categoryᴰ.isSetHomᴰ = isSetHomᴰ
+
+  π : Functorᴰ F reindex Dᴰ
+  π .F-obᴰ = λ z → z
+  π .F-homᴰ = λ z → z
+  π .F-idᴰ = symP (transport-filler _ _)
+  π .F-seqᴰ fᴰ gᴰ = symP (transport-filler _ _)
+
+  GlobalSectionReindex→Section : GlobalSection reindex → Section F Dᴰ
+  GlobalSectionReindex→Section Fᴰ = compFunctorᴰGlobalSection π Fᴰ
+
+module _
+  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  {F : Functor C D}
+  {B : Category ℓB ℓB'}
+  (G : Functor B C)
+  (FGᴰ : Section (F ∘F G) Dᴰ)
+  where
+  private
+    module R = HomᴰReasoning Dᴰ
+  open Functor
+  open Section
+
+  introS : Section G (reindex Dᴰ F)
+  introS .F-obᴰ = FGᴰ .F-obᴰ
+  introS .F-homᴰ = FGᴰ .F-homᴰ
+  introS .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-idᴰ) (R.reind-filler _ _))
+  introS .F-seqᴰ fᴰ gᴰ =
+    R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-seqᴰ fᴰ gᴰ) (R.reind-filler _ _))
+
+module _
+  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  {F : Functor C D}
+  {B : Category ℓB ℓB'} {Bᴰ : Categoryᴰ B ℓBᴰ ℓBᴰ'}
+  (G : Functor B C)
+  (FGᴰ : Functorᴰ (F ∘F G) Bᴰ Dᴰ)
+  where
+  introF : Functorᴰ G Bᴰ (reindex Dᴰ F)
+  introF = TotalCat.recᴰ _ _ (introS _
+    (reindS' (Eq.refl , Eq.refl) (TotalCat.elim FGᴰ)))
diff --git a/Cubical/Categories/Displayed/Constructions/StructureOver.agda b/Cubical/Categories/Displayed/Constructions/StructureOver.agda
index 7b38c0caaf..d7215cf8d7 100644
--- a/Cubical/Categories/Displayed/Constructions/StructureOver.agda
+++ b/Cubical/Categories/Displayed/Constructions/StructureOver.agda
@@ -2,57 +2,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Categories.Displayed.Constructions.StructureOver where
 
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-
-open import Cubical.Data.Sigma
-
-open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.HLevels
-open import Cubical.Categories.Constructions.TotalCategory
-
-private
-  variable
-    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
-
-record StructureOver (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' :
-  Type (ℓ-suc (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓCᴰ ℓCᴰ'))) where
-  open Category C
-  field
-    ob[_] : ob → Type ℓCᴰ
-    Hom[_][_,_] : {x y : ob} → Hom[ x , y ] → ob[ x ] → ob[ y ] → Type ℓCᴰ'
-    idᴰ : ∀ {x} {p : ob[ x ]} → Hom[ id ][ p , p ]
-    _⋆ᴰ_ : ∀ {x y z} {f : Hom[ x , y ]} {g : Hom[ y , z ]} {xᴰ yᴰ zᴰ}
-      → Hom[ f ][ xᴰ , yᴰ ] → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]
-    isPropHomᴰ : ∀ {x y} {f : Hom[ x , y ]} {xᴰ yᴰ} → isProp Hom[ f ][ xᴰ , yᴰ ]
-
-module _ {C : Category ℓC ℓC'} (Pᴰ : StructureOver C ℓCᴰ ℓCᴰ') where
-  open Category
-  open StructureOver
-  StructureOver→Catᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'
-  StructureOver→Catᴰ = record
-    { ob[_] = Pᴰ .ob[_]
-    ; Hom[_][_,_] = Pᴰ .Hom[_][_,_]
-    ; idᴰ = Pᴰ .idᴰ
-    ; _⋆ᴰ_ = Pᴰ ._⋆ᴰ_
-    ; ⋆IdLᴰ = λ _ →
-      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆IdL _) i)})) _ _
-    ; ⋆IdRᴰ = λ _ →
-      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆IdR _) i)})) _ _
-    ; ⋆Assocᴰ = λ _ _ _ →
-      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆Assoc _ _ _) i)})) _ _
-    ; isSetHomᴰ = isProp→isSet (Pᴰ .isPropHomᴰ)
-    }
-
-  hasPropHomsStructureOver : hasPropHoms StructureOver→Catᴰ
-  hasPropHomsStructureOver _ _ _ = Pᴰ .isPropHomᴰ
-
-  open Functor
-
-  isFaithfulFst : isFaithful (Fst {Cᴰ = StructureOver→Catᴰ})
-  isFaithfulFst x y f g p =
-    ΣPathP (p ,
-      isProp→PathP (λ i → Pᴰ .isPropHomᴰ {f = p i}) (f .snd) (g .snd))
+open import Cubical.Categories.Displayed.Constructions.StructureOver.Base public
+open import Cubical.Categories.Displayed.Constructions.StructureOver.Properties
+  public
diff --git a/Cubical/Categories/Displayed/Constructions/StructureOver/Base.agda b/Cubical/Categories/Displayed/Constructions/StructureOver/Base.agda
new file mode 100644
index 0000000000..664c6c2c88
--- /dev/null
+++ b/Cubical/Categories/Displayed/Constructions/StructureOver/Base.agda
@@ -0,0 +1,50 @@
+-- | Structure displayed over a category.
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Constructions.StructureOver.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.HLevels
+
+private
+  variable
+    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
+
+record StructureOver (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' :
+  Type (ℓ-suc (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓCᴰ ℓCᴰ'))) where
+  open Category C
+  field
+    ob[_] : ob → Type ℓCᴰ
+    Hom[_][_,_] : {x y : ob} → Hom[ x , y ] → ob[ x ] → ob[ y ] → Type ℓCᴰ'
+    idᴰ : ∀ {x} {p : ob[ x ]} → Hom[ id ][ p , p ]
+    _⋆ᴰ_ : ∀ {x y z} {f : Hom[ x , y ]} {g : Hom[ y , z ]} {xᴰ yᴰ zᴰ}
+      → Hom[ f ][ xᴰ , yᴰ ] → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]
+    isPropHomᴰ : ∀ {x y} {f : Hom[ x , y ]} {xᴰ yᴰ} → isProp Hom[ f ][ xᴰ , yᴰ ]
+
+module _ {C : Category ℓC ℓC'} (Pᴰ : StructureOver C ℓCᴰ ℓCᴰ') where
+  open Category
+  open StructureOver
+  StructureOver→Catᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'
+  StructureOver→Catᴰ = record
+    { ob[_] = Pᴰ .ob[_]
+    ; Hom[_][_,_] = Pᴰ .Hom[_][_,_]
+    ; idᴰ = Pᴰ .idᴰ
+    ; _⋆ᴰ_ = Pᴰ ._⋆ᴰ_
+    ; ⋆IdLᴰ = λ _ →
+      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆IdL _) i)})) _ _
+    ; ⋆IdRᴰ = λ _ →
+      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆IdR _) i)})) _ _
+    ; ⋆Assocᴰ = λ _ _ _ →
+      isProp→PathP ((λ i → Pᴰ .isPropHomᴰ {f = ((C .⋆Assoc _ _ _) i)})) _ _
+    ; isSetHomᴰ = isProp→isSet (Pᴰ .isPropHomᴰ)
+    }
+
+  hasPropHomsStructureOver : hasPropHoms StructureOver→Catᴰ
+  hasPropHomsStructureOver _ _ _ = Pᴰ .isPropHomᴰ
diff --git a/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda b/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda
new file mode 100644
index 0000000000..4d0948030a
--- /dev/null
+++ b/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda
@@ -0,0 +1,29 @@
+-- | Structure displayed over a category.
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Constructions.StructureOver.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Constructions.StructureOver.Base
+open import Cubical.Categories.Constructions.TotalCategory
+
+private
+  variable
+    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
+
+module _ {C : Category ℓC ℓC'} (Pᴰ : StructureOver C ℓCᴰ ℓCᴰ') where
+  open Functor
+  open StructureOver
+
+  isFaithfulFst : isFaithful (Fst {Cᴰ = StructureOver→Catᴰ Pᴰ})
+  isFaithfulFst x y f g p =
+    ΣPathP (p ,
+      isProp→PathP (λ i → Pᴰ .isPropHomᴰ {f = p i}) (f .snd) (g .snd))
diff --git a/Cubical/Categories/Displayed/Constructions/TotalCategory.agda b/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
index d4c6b9095d..24393f58ec 100644
--- a/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
+++ b/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
@@ -5,13 +5,16 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Sigma
+import      Cubical.Data.Equality as Eq
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Instances.Terminal
-open import Cubical.Categories.Constructions.TotalCategory hiding (intro)
+open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Instances.Terminal hiding (introF)
+open import Cubical.Categories.Constructions.TotalCategory as TC hiding (intro)
 
 private
   variable
@@ -57,10 +60,29 @@ module _ {C : Category ℓC ℓC'}
   (Dᴰ : Categoryᴰ (∫C Cᴰ) ℓDᴰ ℓDᴰ')
   where
 
-  open Functorᴰ
+  hasPropHoms∫Cᴰ : hasPropHoms Cᴰ → hasPropHoms Dᴰ → hasPropHoms (∫Cᴰ Cᴰ Dᴰ)
+  hasPropHoms∫Cᴰ ph-Cᴰ ph-Dᴰ f cᴰ cᴰ' = isPropΣ
+    (ph-Cᴰ f (cᴰ .fst) (cᴰ' .fst))
+    (λ fᴰ → ph-Dᴰ (f , fᴰ) (cᴰ .snd) (cᴰ' .snd))
+
   private
     module Cᴰ = Categoryᴰ Cᴰ
     module Dᴰ = Categoryᴰ Dᴰ
+    ∫∫Cᴰ = ∫C {C = C} (∫Cᴰ Cᴰ Dᴰ)
+  open Functor
+  open Functorᴰ
+
+  Assocᴰ : Functor ∫∫Cᴰ (∫C Dᴰ)
+  Assocᴰ .F-ob  x   = (x .fst , x .snd .fst) , x .snd .snd
+  Assocᴰ .F-hom f   = (f .fst , f .snd .fst) , f .snd .snd
+  Assocᴰ .F-id      = refl
+  Assocᴰ .F-seq _ _ = refl
+
+  Assocᴰ⁻ : Functor (∫C Dᴰ) ∫∫Cᴰ
+  Assocᴰ⁻ .F-ob  x   = x .fst .fst , x .fst .snd , x .snd
+  Assocᴰ⁻ .F-hom f   = f .fst .fst , f .fst .snd , f .snd
+  Assocᴰ⁻ .F-id      = refl
+  Assocᴰ⁻ .F-seq _ _ = refl
 
   Fstᴰ : Functorᴰ Id (∫Cᴰ Cᴰ Dᴰ) Cᴰ
   Fstᴰ .F-obᴰ = fst
@@ -68,15 +90,28 @@ module _ {C : Category ℓC ℓC'}
   Fstᴰ .F-idᴰ = refl
   Fstᴰ .F-seqᴰ _ _ = refl
 
-  -- Functor into the displayed total category
+  open Section
+  module _ {Eᴰ : Categoryᴰ ∫∫Cᴰ ℓEᴰ ℓEᴰ'} where
+    elimGlobal : Section Assocᴰ⁻ Eᴰ → GlobalSection Eᴰ
+    elimGlobal s .F-obᴰ d = s .F-obᴰ ((d .fst , d .snd .fst) , d .snd .snd)
+    elimGlobal s .F-homᴰ f =  s .F-homᴰ ((f .fst , f .snd .fst) , f .snd .snd)
+    elimGlobal s .F-idᴰ = s .F-idᴰ
+    elimGlobal s .F-seqᴰ _ _ = s .F-seqᴰ _ _
+
   module _ {E : Category ℓE ℓE'} (F : Functor E C)
-           {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'}
-           (Fᴰ : Functorᴰ F Eᴰ Cᴰ)
-           (Gᴰ : Functorᴰ (∫F Fᴰ) (Unitᴰ (∫C Eᴰ)) Dᴰ)
+           (Fᴰ : Section F Cᴰ)
+           (Gᴰ : Section (TC.intro F Fᴰ) Dᴰ)
            where
+    introS : Section F (∫Cᴰ Cᴰ Dᴰ)
+    introS .F-obᴰ  d   = Fᴰ .F-obᴰ d , Gᴰ .F-obᴰ d
+    introS .F-homᴰ f   = Fᴰ .F-homᴰ f , Gᴰ .F-homᴰ f
+    introS .F-idᴰ      = ΣPathP (Fᴰ .F-idᴰ , Gᴰ .F-idᴰ)
+    introS .F-seqᴰ f g = ΣPathP (Fᴰ .F-seqᴰ f g , Gᴰ .F-seqᴰ f g)
 
-    intro : Functorᴰ F Eᴰ (∫Cᴰ Cᴰ Dᴰ)
-    intro .F-obᴰ xᴰ = Fᴰ .F-obᴰ xᴰ , Gᴰ .F-obᴰ _
-    intro .F-homᴰ fᴰ = (Fᴰ .F-homᴰ fᴰ) , (Gᴰ .F-homᴰ _)
-    intro .F-idᴰ = ΣPathP (Fᴰ .F-idᴰ , Gᴰ .F-idᴰ)
-    intro .F-seqᴰ fᴰ gᴰ = ΣPathP (Fᴰ .F-seqᴰ fᴰ gᴰ , Gᴰ .F-seqᴰ _ _)
+  module _ {E : Category ℓE ℓE'} {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} (F : Functor E C)
+           (Fᴰ : Functorᴰ F Eᴰ Cᴰ)
+           (Gᴰ : Section (∫F Fᴰ) Dᴰ)
+           where
+    introF : Functorᴰ F Eᴰ (∫Cᴰ Cᴰ Dᴰ)
+    introF = TC.recᴰ _ _ (introS _ (elim Fᴰ)
+      (reindS' (Eq.refl , Eq.refl) Gᴰ))
diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
new file mode 100644
index 0000000000..e795f4b873
--- /dev/null
+++ b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
@@ -0,0 +1,98 @@
+{-
+  Weaken a category to be a displayed category.
+-}
+{-# OPTIONS --safe #-}
+--
+module Cubical.Categories.Displayed.Constructions.Weaken.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Constructions.TotalCategory as TC
+  hiding (intro)
+
+private
+  variable
+    ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
+
+open Categoryᴰ
+
+module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
+  open Category
+  weaken : Categoryᴰ C ℓD ℓD'
+  weaken .ob[_] x = D .ob
+  weaken .Hom[_][_,_] f d d' = D [ d , d' ]
+  weaken .idᴰ = D .id
+  weaken ._⋆ᴰ_ = D ._⋆_
+  weaken .⋆IdLᴰ = D .⋆IdL
+  weaken .⋆IdRᴰ = D .⋆IdR
+  weaken .⋆Assocᴰ = D .⋆Assoc
+  weaken .isSetHomᴰ = D .isSetHom
+
+  open Functor
+  weakenΠ : Functor (∫C weaken) D
+  weakenΠ .F-ob = snd
+  weakenΠ .F-hom = snd
+  weakenΠ .F-id = refl
+  weakenΠ .F-seq _ _ = refl
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {E : Category ℓE ℓE'}
+         (F : Functor E C)
+         (G : Functor E D)
+         where
+  open Category
+  open Functor
+  open Section
+  introS : Section F (weaken C D)
+  introS .F-obᴰ x = G .F-ob x
+  introS .F-homᴰ f = G .F-hom f
+  introS .F-idᴰ = G .F-id
+  introS .F-seqᴰ _ _ = G .F-seq _ _
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {E : Category ℓE ℓE'}
+         {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'}
+         (F : Functor E C)
+         (G : Functor E D)
+         where
+  open Category
+  open Functor
+  open Functorᴰ
+  introF : Functorᴰ F Eᴰ (weaken C D)
+  introF .F-obᴰ {x} _ = G .F-ob x
+  introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f
+  introF .F-idᴰ = G .F-id
+  introF .F-seqᴰ _ _ = G .F-seq _ _
+
+introS⁻ : {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {E : Category ℓE ℓE'}
+         {F : Functor E C}
+       → Section F (weaken C D)
+       → Functor E D
+introS⁻ {C = C}{D = D}{F = F} Fᴰ =
+  weakenΠ C D ∘F TC.intro F Fᴰ
+
+-- TODO: introS/introS⁻ is an Iso
+
+module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where
+  open Functor
+  open Functorᴰ
+
+  weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C}
+          → (G : Functor D E)
+          → Functorᴰ F (weaken B D) (weaken C E)
+  weakenF G .F-obᴰ = G .F-ob
+  weakenF G .F-homᴰ = G .F-hom
+  weakenF G .F-idᴰ = G .F-id
+  weakenF G .F-seqᴰ = G .F-seq
diff --git a/Cubical/Categories/Displayed/HLevels.agda b/Cubical/Categories/Displayed/HLevels.agda
index 839f525a7f..65c451b234 100644
--- a/Cubical/Categories/Displayed/HLevels.agda
+++ b/Cubical/Categories/Displayed/HLevels.agda
@@ -12,6 +12,7 @@ open import Cubical.Categories.Functor
 
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Section.Base
 
 private
   variable
@@ -76,3 +77,53 @@ module _
     mkContrHomsFunctor F-obᴰ =
       mkPropHomsFunctor (hasContrHoms→hasPropHoms Dᴰ contrHoms) F-obᴰ
       λ _ → contrHoms _ _ _ .fst
+module _
+       {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+       {F : Functor C D}
+       {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+       where
+  open Category
+  open Functor
+  private
+    module Dᴰ = Categoryᴰ Dᴰ
+  mkPropHomsSection :
+    (propHoms : hasPropHoms Dᴰ)
+      → (F-obᴰ  : (x : C .ob) → Dᴰ.ob[ F .F-ob x ])
+      → (F-homᴰ : {x y : C .ob}
+        (f : C [ x , y ]) → Dᴰ [ F .F-hom f ][ F-obᴰ x , F-obᴰ y ])
+      → Section F Dᴰ
+  mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-obᴰ = F-obᴰ
+  mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-homᴰ = F-homᴰ
+  mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-idᴰ =
+    isProp→PathP (λ i → propHoms _ _ _) _ _
+  mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-seqᴰ _ _ =
+    isProp→PathP (λ i → propHoms _ _ _) _ _
+
+  mkContrHomsSection :
+    (contrHoms : hasContrHoms Dᴰ)
+      → (F-obᴰ  : (x : C .ob) → Dᴰ.ob[ F .F-ob x ])
+      → Section F Dᴰ
+  mkContrHomsSection contrHoms F-obᴰ = mkPropHomsSection
+    (hasContrHoms→hasPropHoms Dᴰ contrHoms)
+    F-obᴰ
+      λ {x}{y} f → contrHoms (F .F-hom f) (F-obᴰ x) (F-obᴰ y) .fst
+
+  module _ {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
+    private
+      module Cᴰ = Categoryᴰ Cᴰ
+    -- Alternate version: maybe Dᴰ.Hom[_][_,_] isn't always
+    -- contractible, but it is in the image of F-obᴰ
+    mkContrHomsFunctor'
+      : (F-obᴰ  : {x : C .ob} → Cᴰ.ob[ x ] → Dᴰ.ob[ F .F-ob x ])
+      → (F-homᴰ : {x y : C .ob}
+        {f : C [ x , y ]} {xᴰ : Cᴰ.ob[ x ]} {yᴰ : Cᴰ.ob[ y ]}
+      → Cᴰ [ f ][ xᴰ , yᴰ ]
+      → isContr (Dᴰ [ F .F-hom f ][ F-obᴰ xᴰ , F-obᴰ yᴰ ]))
+      → Functorᴰ F Cᴰ Dᴰ
+    mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-obᴰ = F-obᴰ
+    mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-homᴰ fᴰ = F-homᴰ fᴰ .fst
+    mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-idᴰ =
+      symP (toPathP (isProp→PathP (λ i → isContr→isProp (F-homᴰ Cᴰ.idᴰ)) _ _))
+    mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-seqᴰ fᴰ gᴰ =
+      symP (toPathP (isProp→PathP
+        (λ i → isContr→isProp (F-homᴰ (fᴰ Cᴰ.⋆ᴰ gᴰ))) _ _))
diff --git a/Cubical/Categories/Displayed/Instances/Path.agda b/Cubical/Categories/Displayed/Instances/Path.agda
new file mode 100644
index 0000000000..dc1f1ffb38
--- /dev/null
+++ b/Cubical/Categories/Displayed/Instances/Path.agda
@@ -0,0 +1,73 @@
+{-
+  Paths between objects as a category displayed over C × C.
+
+  If C is univalent, this is equivalent to the IsoComma category.
+
+  Universal property: a section of the Path bundle is a path between
+  functors
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Instances.Path where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Unit
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Constructions.StructureOver
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓS ℓR : Level
+
+open Section
+open Functor
+
+module _  (C : Category ℓC ℓC') where
+  private
+    module C = Category C
+    open StructureOver
+    PathC' : StructureOver (C ×C C) _ _
+    PathC' .ob[_] (c , d) = c ≡ d
+    PathC' .Hom[_][_,_] (f , g) c≡c' d≡d' =
+      PathP (λ i → C.Hom[ c≡c' i , d≡d' i ]) f g
+    PathC' .idᴰ = λ i → C.id
+    PathC' ._⋆ᴰ_ f≡f' g≡g' = λ i → f≡f' i ⋆⟨ C ⟩ g≡g' i
+    PathC' .isPropHomᴰ = isOfHLevelPathP' 1 C.isSetHom _ _
+
+  PathC : Categoryᴰ (C ×C C) ℓC ℓC'
+  PathC = StructureOver→Catᴰ PathC'
+
+  hasPropHomsPathC : hasPropHoms PathC
+  hasPropHomsPathC = hasPropHomsStructureOver PathC'
+
+  -- The universal functor into PathC
+  Refl : Section (Δ C) PathC
+  Refl = mkPropHomsSection hasPropHomsPathC (λ _ → refl) λ _ → refl
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {F1 F2 : Functor D C}
+         where
+  -- "Equality/Path Reflection Rule"
+  PathReflection :
+    ∀ (Fᴰ : Section (F1 ,F F2) (PathC C)) → F1 ≡ F2
+  PathReflection Fᴰ = Functor≡ Fᴰ.F-obᴰ Fᴰ.F-homᴰ
+    where module Fᴰ = Section Fᴰ
+
+  -- Could also implement this using J and Refl, not sure which is
+  -- preferable
+  PathReflection⁻ :
+    F1 ≡ F2 → Section (F1 ,F F2) (PathC C)
+  PathReflection⁻ P = mkPropHomsSection (hasPropHomsPathC C)
+    (λ x i → P i .F-ob x)
+    λ f i → P i .F-hom f
+
+-- TODO: there should also be a "J"-style elimination principle.
diff --git a/Cubical/Categories/Displayed/Instances/Terminal.agda b/Cubical/Categories/Displayed/Instances/Terminal.agda
index 9f21f54a91..2328e25658 100644
--- a/Cubical/Categories/Displayed/Instances/Terminal.agda
+++ b/Cubical/Categories/Displayed/Instances/Terminal.agda
@@ -1,31 +1,5 @@
 {-# OPTIONS --safe #-}
 module Cubical.Categories.Displayed.Instances.Terminal where
 
-open import Cubical.Foundations.Prelude
-
-open import Cubical.Data.Unit
-
-open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Instances.Terminal
-open import Cubical.Categories.Displayed.Base
-
-private
-  variable
-    ℓC ℓC' ℓD ℓD' : Level
-
-open Category
-open Categoryᴰ
--- Terminal category over a base category
-Unitᴰ : (C : Category ℓC ℓC') → Categoryᴰ C ℓ-zero ℓ-zero
-Unitᴰ C .ob[_] x = Unit
-Unitᴰ C .Hom[_][_,_] f tt tt = Unit
-Unitᴰ C .idᴰ = tt
-Unitᴰ C ._⋆ᴰ_ = λ _ _ → tt
-Unitᴰ C .⋆IdLᴰ fᴰ i = tt
-Unitᴰ C .⋆IdRᴰ fᴰ i = tt
-Unitᴰ C .⋆Assocᴰ fᴰ gᴰ hᴰ i = tt
-Unitᴰ C .isSetHomᴰ x y x₁ y₁ i i₁ = tt
-
--- Terminal category over the terminal category
-UnitCᴰ : Categoryᴰ (TerminalCategory {ℓ-zero}) ℓ-zero ℓ-zero
-UnitCᴰ = Unitᴰ TerminalCategory
+open import Cubical.Categories.Displayed.Instances.Terminal.Base public
+open import Cubical.Categories.Displayed.Instances.Terminal.Properties public
diff --git a/Cubical/Categories/Displayed/Instances/Terminal/Base.agda b/Cubical/Categories/Displayed/Instances/Terminal/Base.agda
new file mode 100644
index 0000000000..9f203e6898
--- /dev/null
+++ b/Cubical/Categories/Displayed/Instances/Terminal/Base.agda
@@ -0,0 +1,48 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Instances.Terminal.Base where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Unit
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Instances.Terminal
+
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Constructions.PropertyOver
+open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Section.Base
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+
+open Category
+open Categoryᴰ
+open Section
+
+-- Terminal category over a base category
+Unitᴰ : (C : Category ℓC ℓC') → Categoryᴰ C ℓ-zero ℓ-zero
+Unitᴰ C .ob[_] x = Unit
+Unitᴰ C .Hom[_][_,_] f tt tt = Unit
+Unitᴰ C .idᴰ = tt
+Unitᴰ C ._⋆ᴰ_ = λ _ _ → tt
+Unitᴰ C .⋆IdLᴰ fᴰ i = tt
+Unitᴰ C .⋆IdRᴰ fᴰ i = tt
+Unitᴰ C .⋆Assocᴰ fᴰ gᴰ hᴰ i = tt
+Unitᴰ C .isSetHomᴰ x y x₁ y₁ i i₁ = tt
+
+-- Terminal category over the terminal category
+UnitCᴰ : Categoryᴰ (TerminalCategory {ℓ-zero}) ℓ-zero ℓ-zero
+UnitCᴰ = Unitᴰ TerminalCategory
+
+module _ {C : Category ℓC ℓC'} where
+  hasContrHomsUnitᴰ : hasContrHoms (Unitᴰ C)
+  hasContrHomsUnitᴰ = hasContrHomsPropertyOver C _
+
+  ttS : GlobalSection (Unitᴰ C)
+  ttS .F-obᴰ  = λ _ → tt
+  ttS .F-homᴰ = λ _ → tt
+  ttS .F-idᴰ  = refl
+  ttS .F-seqᴰ _ _ = refl
+
diff --git a/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda b/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda
new file mode 100644
index 0000000000..b6c358d5e0
--- /dev/null
+++ b/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda
@@ -0,0 +1,45 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Instances.Terminal.Properties where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Unit
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Instances.Terminal.Base
+open import Cubical.Categories.Displayed.HLevels
+open import Cubical.Categories.Displayed.Section.Base
+
+private
+  variable
+    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
+
+open Category
+open Categoryᴰ
+open Functorᴰ
+open Section
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+         {F : Functor C D}
+         where
+  recᴰ : (s : Section F Dᴰ) → Functorᴰ F (Unitᴰ C) Dᴰ
+  recᴰ s .F-obᴰ {x} _      = s .F-obᴰ x
+  recᴰ s .F-homᴰ {f = f} _ = s .F-homᴰ f
+  recᴰ s .F-idᴰ      = s .F-idᴰ
+  recᴰ s .F-seqᴰ _ _ = s .F-seqᴰ _ _
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         (F : Functor C D) where
+  introF : Functorᴰ F Cᴰ (Unitᴰ D)
+  introF .F-obᴰ = λ _ → tt
+  introF .F-homᴰ = λ _ → tt
+  introF .F-idᴰ = refl
+  introF .F-seqᴰ _ _ = refl
diff --git a/Cubical/Categories/Displayed/Properties.agda b/Cubical/Categories/Displayed/Properties.agda
deleted file mode 100644
index 089a3231a6..0000000000
--- a/Cubical/Categories/Displayed/Properties.agda
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# OPTIONS --safe #-}
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Function
-
-open import Cubical.Data.Unit
-
-open import Cubical.Categories.Category
-open import Cubical.Categories.Displayed.Base
-import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Instances.Terminal
-
-module Cubical.Categories.Displayed.Properties where
-
-private
-  variable
-    ℓC ℓ'C ℓD ℓ'D ℓCᴰ ℓ'Cᴰ ℓDᴰ ℓ'Dᴰ : Level
-
-module _
-  {C : Category ℓC ℓ'C} {D : Category ℓD ℓ'D}
-  (Dᴰ : Categoryᴰ D ℓDᴰ ℓ'Dᴰ) (F : Functor C D)
-  where
-
-  private
-    module R = HomᴰReasoning Dᴰ
-    module C = Category C
-    module D = Category D
-
-  open Categoryᴰ Dᴰ
-  open Functor F
-
-  reindex : Categoryᴰ C ℓDᴰ ℓ'Dᴰ
-  reindex .Categoryᴰ.ob[_] c = ob[ F-ob c ]
-  reindex .Categoryᴰ.Hom[_][_,_] f aᴰ bᴰ = Hom[ F-hom f ][ aᴰ , bᴰ ]
-  reindex .Categoryᴰ.idᴰ = R.reind (sym F-id) idᴰ
-  reindex .Categoryᴰ._⋆ᴰ_ fᴰ gᴰ = R.reind (sym $ F-seq _ _) (fᴰ ⋆ᴰ gᴰ)
-  reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (R.reind-filler-sym F-id idᴰ R.[ _ ]⋆[ refl ] refl)
-      R.[ _ ]∙[ _ ]
-    ⋆IdLᴰ fᴰ
-  reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (refl R.[ refl ]⋆[ _ ] R.reind-filler-sym F-id idᴰ)
-      R.[ _ ]∙[ _ ]
-    ⋆IdRᴰ fᴰ
-  reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (R.reind-filler-sym (F-seq _ _) _ R.[ _ ]⋆[ refl ] refl)
-      R.[ _ ]∙[ _ ]
-    ⋆Assocᴰ fᴰ gᴰ hᴰ
-      R.[ _ ]∙[ _ ]
-    (refl R.[ refl ]⋆[ _ ] R.reind-filler (sym $ F-seq _ _) _)
-      R.[ _ ]∙[ _ ]
-    R.reind-filler (sym $ F-seq _ _) _
-  reindex .Categoryᴰ.isSetHomᴰ = isSetHomᴰ
-
-
-module _ {ℓ* : Level} (Cᴰ : Categoryᴰ (TerminalCategory {ℓ*}) ℓCᴰ ℓ'Cᴰ) where
-  open Categoryᴰ Cᴰ
-  open Category hiding (_∘_)
-
-  DispOverTerminal→Category : Category ℓCᴰ ℓ'Cᴰ
-  DispOverTerminal→Category .ob = ob[ tt* ]
-  DispOverTerminal→Category .Hom[_,_] = Hom[ refl ][_,_]
-  DispOverTerminal→Category .id = idᴰ
-  DispOverTerminal→Category ._⋆_ = _⋆ᴰ_
-  DispOverTerminal→Category .⋆IdL = ⋆IdLᴰ
-  DispOverTerminal→Category .⋆IdR = ⋆IdRᴰ
-  DispOverTerminal→Category .⋆Assoc = ⋆Assocᴰ
-  DispOverTerminal→Category .isSetHom = isSetHomᴰ
-
-module _ (C : Category ℓC ℓ'C) where
-  open Categoryᴰ
-  open Category C hiding (_∘_)
-
-  Category→DispOverTerminal : {ℓ* : Level} → Categoryᴰ (TerminalCategory {ℓ*}) ℓC ℓ'C
-  Category→DispOverTerminal .ob[_] _ = ob
-  Category→DispOverTerminal .Hom[_][_,_] _ = Hom[_,_]
-  Category→DispOverTerminal .idᴰ = id
-  Category→DispOverTerminal ._⋆ᴰ_ = _⋆_
-  Category→DispOverTerminal .⋆IdLᴰ = ⋆IdL
-  Category→DispOverTerminal .⋆IdRᴰ = ⋆IdR
-  Category→DispOverTerminal .⋆Assocᴰ = ⋆Assoc
-  Category→DispOverTerminal .isSetHomᴰ = isSetHom
-
-module _ {C : Category ℓC ℓ'C} (Cᴰ : Categoryᴰ C ℓCᴰ ℓ'Cᴰ) where
-  open Category C
-  open Categoryᴰ Cᴰ
-  VerticalCategory : ob → Category ℓCᴰ ℓ'Cᴰ
-  VerticalCategory c = DispOverTerminal→Category (reindex Cᴰ (FunctorFromTerminal {ℓ* = ℓ-zero} c))
diff --git a/Cubical/Categories/Displayed/Section.agda b/Cubical/Categories/Displayed/Section.agda
new file mode 100644
index 0000000000..b5881e4bef
--- /dev/null
+++ b/Cubical/Categories/Displayed/Section.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Section where
+
+open import Cubical.Categories.Displayed.Section.Base public
diff --git a/Cubical/Categories/Displayed/Section/Base.agda b/Cubical/Categories/Displayed/Section/Base.agda
new file mode 100644
index 0000000000..07cd1a7a82
--- /dev/null
+++ b/Cubical/Categories/Displayed/Section/Base.agda
@@ -0,0 +1,318 @@
+{-
+   Local and Global Sections of a displayed category.
+
+   A local section of a displayed category Cᴰ over a functor F : D → C
+   is visualized as follows:
+
+          Cᴰ
+        ↗ |
+       /  |
+    s /   |
+     /    |
+    /     ↓
+   D ---→ C
+       F
+
+   We call this a *global* section if F is the identity functor.
+
+   Every Section can be implemented as a Functorᴰ out of Unitᴰ (see
+   Displayed.Instances.Terminal):
+
+       Fᴰ
+   D ----→ Cᴰ
+   ∥       |
+   ∥       |
+   ∥       |
+   ∥       |
+   ∥       ↓
+   D ----→ C
+       F
+
+   And vice-versa any Functorᴰ
+
+       Fᴰ
+   Dᴰ ----→ Cᴰ
+   |        |
+   |        |
+   |        |
+   |        |
+   ↓        ↓
+   D -----→ C
+       F
+
+   Can be implemented as a Section (see
+   Displayed.Constructions.TotalCategory)
+
+            Cᴰ
+          ↗ |
+         /  |
+      s /   |
+       /    |
+      /     ↓
+   ∫Dᴰ ---→ C
+        F
+
+   Both options are sometimes more ergonomic. One of the main
+   cosmetic differences is
+
+   1. When defining a Functorᴰ, the object of the base category is
+      implicit
+   2. When defining a Section, the object of the base category is
+      explicit
+
+   Definitionally, there is basically no difference as these are
+   definitional isomorphisms.
+
+   Elimination rules are naturally stated in terms of local sections
+   (and often global sections, see below). Intro rules can be
+   formulated as either constructing a Section or a Functorᴰ. Good
+   style is to offer both introS for Section and introF for Functorᴰ.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Section.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+import      Cubical.Data.Equality as Eq
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Equality
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
+
+private
+  variable
+    ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
+
+open Category
+open Categoryᴰ
+open Functor
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         (F : Functor D C)
+         (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+         where
+  private
+    module C = Category C
+    module D = Category D
+    module Cᴰ = Categoryᴰ Cᴰ
+    module F = Functor F
+
+  -- Section without a qualifier means *local* section.
+  record Section : Type (ℓ-max (ℓ-max ℓC ℓC')
+                        (ℓ-max (ℓ-max ℓD ℓD')
+                        (ℓ-max ℓCᴰ ℓCᴰ')))
+    where
+    field
+      F-obᴰ  : ∀ d → Cᴰ.ob[ F ⟅ d ⟆ ]
+      F-homᴰ : ∀ {d d'} (f : D.Hom[ d , d' ])
+        → Cᴰ.Hom[ F ⟪ f ⟫ ][ F-obᴰ d , F-obᴰ d' ]
+      F-idᴰ : ∀ {d} → F-homᴰ (D.id {d}) Cᴰ.≡[ F .F-id ] Cᴰ.idᴰ
+      F-seqᴰ : ∀ {d d' d''}
+            → (f : D.Hom[ d , d' ])(g : D.Hom[ d' , d'' ])
+            → F-homᴰ (f D.⋆ g) Cᴰ.≡[ F .F-seq f g ] F-homᴰ f Cᴰ.⋆ᴰ F-homᴰ g
+
+{-
+   A Global Section is a local section over the identity functor.
+
+          Cᴰ
+        ↗ |
+       /  |
+    s /   |
+     /    |
+    /     ↓
+   C ==== C
+
+
+   So global sections are by definition local sections
+
+   All local sections can be implemented as global sections into the
+   reindexed displayed category. See Reindex.agda for details.
+
+   But this isomorphism is not definitional (i.e. the equations are
+   not provable by refl). Constructing a local section is preferable
+   as they are more flexible, but often elimination principles are
+   naturally proven first about global sections and then generalized
+   to local sections using reindexing.
+
+   It is good style is to offer both: elimLocal to construct a local
+   section and elimGlobal to construct a global section.
+-}
+
+module _ {C : Category ℓC ℓC'}
+         (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+         where
+  GlobalSection : Type _
+  GlobalSection = Section Id Cᴰ
+
+-- Reindexing a section.
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         where
+  open Section
+  private
+    module Cᴰ = Categoryᴰ Cᴰ
+    module R = HomᴰReasoning Cᴰ
+
+  -- the following reindexes a section to be over a different functor
+  -- that is equal to it, analogous to reind in Displayed.Reasoning.
+
+  -- This version is easily defined by subst, but its action on
+  -- objects and morphisms involves a transport, which is often
+  -- undesirable.
+  reindS : ∀ {F G}(H : Path (Functor D C) F G) → Section F Cᴰ → Section G Cᴰ
+  reindS H = subst (λ F → Section F Cᴰ) H
+
+  -- This version works by taking in a FunctorEq rather than a Path,
+  -- meaning we can define the section by J. If the FunctorEq is given
+  -- by (refl , refl) then this definition will not involve any
+  -- transport and is preferable to reindS.
+  reindS' : ∀ {F G : Functor D C} (H : FunctorEq F G)
+          → Section F Cᴰ
+          → Section G Cᴰ
+  reindS' {F}{G} (H-ob , H-hom) Fᴰ = record
+    { F-obᴰ = Gᴰ-obᴰ (F-singl .fst)
+    ; F-homᴰ = Gᴰ-homᴰ F-singl
+    ; F-idᴰ = Gᴰ-idᴰ F-singl (G .F-id)
+    ; F-seqᴰ = Gᴰ-seqᴰ F-singl (G .F-seq)
+    } where
+      F-singl : FunctorSingl F
+      F-singl = (_ , H-ob) , (_ , H-hom)
+
+      Gᴰ-obᴰ : (G : Eq.singl (F .F-ob)) → (d : D .ob) → Cᴰ.ob[ G .fst d ]
+      Gᴰ-obᴰ (_ , Eq.refl) = Fᴰ .F-obᴰ
+
+      Gᴰ-homᴰ : (G : FunctorSingl F) → ∀ {d d'} (f : D [ d , d' ])
+              → Cᴰ.Hom[ G .snd .fst f
+                     ][ Gᴰ-obᴰ (G .fst) d
+                      , Gᴰ-obᴰ (G .fst) d' ]
+      Gᴰ-homᴰ ((_ , Eq.refl), (_ , Eq.refl)) = Fᴰ .F-homᴰ
+
+      Gᴰ-idᴰ : (G : FunctorSingl F)
+               (G-id : ∀ {x} → G .snd .fst (D .id {x}) ≡ C .id)
+             →  ∀ {d} → Gᴰ-homᴰ G (D .id {d}) Cᴰ.≡[ G-id ] Cᴰ.idᴰ
+      Gᴰ-idᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-id = R.≡[]-rectify (Fᴰ .F-idᴰ)
+
+      Gᴰ-seqᴰ : (G : FunctorSingl F)
+                (G-seq : ∀ {d d' d''}(f : D [ d , d' ])(g : D [ d' , d'' ])
+                       → G .snd .fst (f ⋆⟨ D ⟩ g)
+                       ≡ G .snd .fst f ⋆⟨ C ⟩ G .snd .fst g)
+              → ∀ {d d' d'' : D .ob} (f : D [ d , d' ]) (g : D [ d' , d'' ])
+              → Gᴰ-homᴰ G (f ⋆⟨ D ⟩ g)
+                Cᴰ.≡[ G-seq f g ] (Gᴰ-homᴰ G f Cᴰ.⋆ᴰ Gᴰ-homᴰ G g)
+      Gᴰ-seqᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-seq f g =
+        R.≡[]-rectify (Fᴰ .F-seqᴰ f g)
+{-
+
+   Composition of a Section and a Functor
+
+                 Cᴰ
+               ↗ |
+              /  |
+           s /   |
+            /    |
+           /     ↓
+   E ---→ D ---→ C
+              F
+
+-}
+module _ {B : Category ℓB ℓB'}
+         {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {F : Functor C D}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+       where
+  open Functor
+  open Section
+  private
+    module Dᴰ = Categoryᴰ Dᴰ
+    module R = HomᴰReasoning Dᴰ
+  compSectionFunctor : Section F Dᴰ → (G : Functor B C) → Section (F ∘F G) Dᴰ
+  compSectionFunctor Fᴰ G .F-obᴰ d     = Fᴰ .F-obᴰ (G .F-ob d)
+  compSectionFunctor Fᴰ G .F-homᴰ f    = Fᴰ .F-homᴰ (G .F-hom f)
+  compSectionFunctor Fᴰ G .F-idᴰ       = R.≡[]-rectify (R.≡[]∙ _ _
+    (cong (Fᴰ .F-homᴰ) (G .F-id))
+    (Fᴰ .F-idᴰ))
+  compSectionFunctor Fᴰ G .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _
+    (cong (Fᴰ .F-homᴰ) (G .F-seq f g))
+    (Fᴰ .F-seqᴰ (G .F-hom f) (G .F-hom g)))
+
+module _ {D : Category ℓD ℓD'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+       where
+  open Functor
+  open Section
+  private
+    module Dᴰ = Categoryᴰ Dᴰ
+    module R = HomᴰReasoning Dᴰ
+
+  compGSectionFunctor : {C : Category ℓC ℓC'}
+    → GlobalSection Dᴰ
+    → (G : Functor C D)
+    → Section G Dᴰ
+  compGSectionFunctor s G = reindS' (Eq.refl , Eq.refl) (compSectionFunctor s G)
+{-
+
+  Composition of a Section and a Functorᴰ
+
+              Fᴰ'
+          Cᴰ ---→ Cᴰ'
+        ↗ |       |
+       /  |       |
+    s /   |       |
+     /    |       |
+    /     ↓       ↓
+   D ---→ C ----→ C'
+       F     F'
+
+-}
+module _ {B : Category ℓB ℓB'}
+         {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {F : Functor C D}
+         {G : Functor B C}
+         {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+       where
+  open Functor
+  open Functorᴰ
+  open Section
+  private
+    module Dᴰ = Categoryᴰ Dᴰ
+    module Cᴰ = Categoryᴰ Cᴰ
+    module R = HomᴰReasoning Dᴰ
+  compFunctorᴰSection : Functorᴰ F Cᴰ Dᴰ → Section G Cᴰ → Section (F ∘F G) Dᴰ
+  compFunctorᴰSection Fᴰ Gᴰ .F-obᴰ d    = Fᴰ .F-obᴰ (Gᴰ .F-obᴰ d)
+  compFunctorᴰSection Fᴰ Gᴰ .F-homᴰ f   = Fᴰ .F-homᴰ (Gᴰ .F-homᴰ f)
+  compFunctorᴰSection Fᴰ Gᴰ .F-idᴰ      = R.≡[]-rectify (R.≡[]∙ _ _
+    (λ i → Fᴰ .F-homᴰ (Gᴰ .F-idᴰ i))
+    (Fᴰ .F-idᴰ))
+  compFunctorᴰSection Fᴰ Gᴰ .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _
+    (λ i → Fᴰ .F-homᴰ (Gᴰ .F-seqᴰ f g i))
+    (Fᴰ .F-seqᴰ (Gᴰ .F-homᴰ f) (Gᴰ .F-homᴰ g)))
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {F : Functor C D}
+         {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+       where
+  open Functor
+  open Functorᴰ
+  open Section
+  private
+    module Dᴰ = Categoryᴰ Dᴰ
+    module Cᴰ = Categoryᴰ Cᴰ
+    module R = HomᴰReasoning Dᴰ
+
+  compFunctorᴰGlobalSection : Functorᴰ F Cᴰ Dᴰ → GlobalSection Cᴰ → Section F Dᴰ
+  compFunctorᴰGlobalSection Fᴰ Gᴰ = reindS' (Eq.refl , Eq.refl)
+    (compFunctorᴰSection Fᴰ Gᴰ)
diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda
index f41b400666..bb52b4a497 100644
--- a/Cubical/Categories/Functor/ComposeProperty.agda
+++ b/Cubical/Categories/Functor/ComposeProperty.agda
@@ -5,6 +5,7 @@ module Cubical.Categories.Functor.ComposeProperty where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv
+open import Cubical.Functions.Embedding
 
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation as Prop
@@ -12,13 +13,19 @@ open import Cubical.HITs.PropositionalTruncation as Prop
 open import Cubical.Categories.Category
 open import Cubical.Categories.Isomorphism
 open import Cubical.Categories.Functor
-open import Cubical.Categories.NaturalTransformation.Base
+open import Cubical.Categories.NaturalTransformation
 open import Cubical.Categories.Equivalence
 open import Cubical.Categories.Equivalence.WeakEquivalence
 
 open import Cubical.Categories.Instances.Functors
 
 
+open Category
+open Functor
+open NatTrans
+open isIso
+open isWeakEquivalence
+
 -- Composition by functor with special properties
 
 module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
@@ -26,12 +33,6 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
   (F : Functor C D)
   where
 
-  open Category
-  open Functor
-  open NatTrans
-  open isIso
-
-
   -- If F is essential surjective, (- ∘ F) is faithful.
 
   isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F)
@@ -145,15 +146,8 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
   {E : Category ℓE ℓE'} (isUnivE : isUnivalent E)
   (F : Functor C D)
   where
-
-  open Category
-  open Functor
-  open NatTrans
-  open isIso
-  open isWeakEquivalence
   open isUnivalent isUnivE
 
-
   -- If F is weak equivalence and the target category is univalent, (- ∘ F) is essentially surjective.
 
   isWeakEquiv→isEssSurjPrecomp : isWeakEquivalence F → isEssentiallySurj (precomposeF E F)
@@ -418,3 +412,38 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
   isWeakEquiv→isEquivPrecomp w-equiv =
     isWeakEquiv→isEquiv (isUnivalentFUNCTOR _ _ isUnivE) (isUnivalentFUNCTOR _ _ isUnivE)
       (isWeakEquiv→isWeakEquivPrecomp w-equiv)
+
+module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
+  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {E : Category ℓE ℓE'}
+  {G : Functor D E}
+  (isFullyFaithfulG : isFullyFaithful G)
+  where
+
+  private
+    GFF : ∀ {x y} → D [ x , y ] ≃ E [ G ⟅ x ⟆ , G ⟅ y ⟆ ]
+    GFF = _ , (isFullyFaithfulG _ _)
+
+    GFaith : ∀ {x y} → (D [ x , y ]) ↪ (E [ G ⟅ x ⟆ , G ⟅ y ⟆ ])
+    GFaith = _ , isEquiv→isEmbedding (GFF .snd)
+    -- this would be convenient as FF.Reasoning
+    G-hom⁻ : ∀ {x y} → E [ G ⟅ x ⟆ , G ⟅ y ⟆ ] → D [ x , y ]
+    G-hom⁻ = invIsEq (isFullyFaithfulG _ _)
+
+
+  isFullyFaithfulPostcomposeF : isFullyFaithful (postcomposeF C G)
+  isFullyFaithfulPostcomposeF F F' .equiv-proof α =
+    uniqueExists
+      (natTrans (λ x → G-hom⁻ (α ⟦ x ⟧)) λ f →
+        isEmbedding→Inj (GFaith .snd) _ _
+        ( G .F-seq _ _
+        ∙ cong₂ (seq' E) refl (secEq GFF _)
+        ∙ α.N-hom _
+        ∙ sym (cong₂ (seq' E) (secEq GFF _) refl)
+        ∙ sym (G .F-seq _ _)))
+      (makeNatTransPath (funExt λ c → secIsEq (isFullyFaithfulG _ _) (α ⟦ c ⟧)))
+      (λ _ → isSetNatTrans _ _)
+      λ β G∘β≡α → makeNatTransPath (funExt λ c →
+        isEmbedding→Inj (isEquiv→isEmbedding (isFullyFaithfulG _ _)) _ _
+        (secIsEq (isFullyFaithfulG _ _) _ ∙ sym (cong (_⟦ c ⟧) G∘β≡α)))
+
+    where module α = NatTrans α
diff --git a/Cubical/Categories/Functor/Equality.agda b/Cubical/Categories/Functor/Equality.agda
new file mode 100644
index 0000000000..d0401b6ba7
--- /dev/null
+++ b/Cubical/Categories/Functor/Equality.agda
@@ -0,0 +1,41 @@
+{-
+  A version of Eq for functors, convenient for parameterizing
+  constructions that use J where the equalities are refl.
+-}
+
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Functor.Equality where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+import      Cubical.Data.Equality as Eq
+
+private
+  variable
+    ℓ ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+module _
+  {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  (F : Functor C D)
+  where
+  open Functor
+
+  private
+    module C = Category C
+    module D = Category D
+
+  FunctorSingl : Type _
+  FunctorSingl = Σ[ ob' ∈ Eq.singl (F .F-ob) ]
+    Eq.singlP (Eq.ap (λ F-ob → ∀ {x}{y} → C [ x , y ] → D [ F-ob x , F-ob y ])
+              (ob' .snd))
+    (F .F-hom)
+
+  module _ (G : Functor C D) where
+    FunctorEq : Type _
+    FunctorEq = Σ[ FG-ob ∈ F .F-ob Eq.≡ G .F-ob ]
+      Eq.HEq (Eq.ap (λ F-ob → ∀ {x} {y} → C [ x , y ] → D [ F-ob x , F-ob y ])
+             FG-ob)
+        (F .F-hom)
+        (G .F-hom)
diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda
index 8bbbb9b8be..968052e27e 100644
--- a/Cubical/Categories/Functor/Properties.agda
+++ b/Cubical/Categories/Functor/Properties.agda
@@ -263,3 +263,46 @@ F-seq (TransportFunctor p) {x} {y} {z} f g i =
        , transport-filler (λ i₁ → ob (p i₁)) x (i ∨ jj) ]
         (transport-filler (λ i₁ → ob (p i₁)) z (i ∨ jj))) i
      (_⋆_ (p i) (transport-filler q f i) (transport-filler q g i))
+
+
+module _ {F : Functor C D} {G : Functor D E} where
+  open Category
+  open Functor
+
+  module _
+    (isFullyFaithfulF : isFullyFaithful F)
+    (isFullyFaithfulG : isFullyFaithful G)
+    where
+    isFullyFaithfulG∘F : isFullyFaithful (G ∘F F)
+    isFullyFaithfulG∘F x y =
+      equivIsEquiv
+        (compEquiv (_ , isFullyFaithfulF x y)
+                 (_ , isFullyFaithfulG (F ⟅ x ⟆) (F ⟅ y ⟆)))
+
+  module _
+    (isFullG : isFull G)
+    (isFullF : isFull F)
+    where
+    isFullG∘F : isFull (G ∘F F)
+    isFullG∘F x y G∘F[f] =
+      rec
+        isPropPropTrunc
+        (λ Ff → rec
+          isPropPropTrunc
+          (λ f → ∣ f .fst , cong (G .F-hom) (f .snd) ∙ Ff .snd ∣₁)
+          (isFullF x y (Ff .fst)))
+        (isFullG (F ⟅ x ⟆) (F ⟅ y ⟆) G∘F[f])
+
+  module _
+    (isFaithfulF : isFaithful F)
+    (isFaithfulG : isFaithful G)
+    where
+
+    isFaithfulG∘F : isFaithful (G ∘F F)
+    isFaithfulG∘F x y =
+      isEmbedding→Inj
+        (compEmbedding
+        ((λ v → F-hom G v) ,
+          (injEmbedding (E .isSetHom) (isFaithfulG (F ⟅ x ⟆) (F ⟅ y ⟆) _ _)))
+        ((λ z → F-hom F z) ,
+          (injEmbedding (D .isSetHom) (isFaithfulF x y _ _))) .snd)
diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda
index 440a8b84ff..3f28355ccb 100644
--- a/Cubical/Categories/Instances/Sets.agda
+++ b/Cubical/Categories/Instances/Sets.agda
@@ -132,6 +132,17 @@ isUnivalent.univ isUnivalentSET (A , isSet-A) (B , isSet-B)  =
             (λ x i → transp (λ _ → B) i (ci .fst (transp (λ _ → A) i x)))
             (λ x i → transp (λ _ → A) i (ci .snd .cInv (transp (λ _ → B) i x))))
 
+module _ {A}{B} (f : CatIso (SET ℓ) A B) a where
+  open isUnivalent
+  -- univalence of SET behaves as expected
+  univSetβ : transport (cong fst (CatIsoToPath isUnivalentSET f)) a
+             ≡ f .fst a
+  univSetβ = (transportRefl _
+    ∙ transportRefl _
+    ∙ transportRefl _
+    ∙ cong (f .fst) (transportRefl _ ∙ transportRefl _ ))
+
+
 -- SET is complete
 open LimCone
 open Cone
diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda
index ca13f619e5..75c3474f4e 100644
--- a/Cubical/Categories/Isomorphism.agda
+++ b/Cubical/Categories/Isomorphism.agda
@@ -3,6 +3,7 @@ module Cubical.Categories.Isomorphism where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism using (isoFunInjective)
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Function
 open import Cubical.Categories.Category
@@ -111,7 +112,6 @@ module _ {C : Category ℓC ℓC'} where
       ∙ ⋆IdL _
 
   module _ (isUnivC : isUnivalent C) where
-
     open isUnivalent isUnivC
 
 
@@ -240,3 +240,21 @@ module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} whe
 
   F-pathToIso-∘ : {x y : C .ob} → F-Iso ∘ pathToIso {x = x} {y = y} ≡ pathToIso ∘ cong (F .F-ob)
   F-pathToIso-∘ i p = F-pathToIso p i
+
+module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  (isUnivC : isUnivalent C) (isUnivD : isUnivalent D)
+  (F : Functor C D)
+  where
+    open isUnivalent
+    open Category
+    open Functor
+    private
+      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/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda
index 93b9fb2bd8..a24eeb794d 100644
--- a/Cubical/Categories/NaturalTransformation/Base.agda
+++ b/Cubical/Categories/NaturalTransformation/Base.agda
@@ -247,3 +247,12 @@ module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} {D : Category ℓD
   whiskerTrans : {F F' : Functor B C} {G G' : Functor C D} (β : NatTrans G G') (α : NatTrans F F')
     → NatTrans (G ∘F F) (G' ∘F F')
   whiskerTrans {F}{F'}{G}{G'} β α = compTrans (β ∘ˡ F') (G ∘ʳ α)
+
+module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
+  open NatIso
+  -- whiskering
+  -- αF
+  _∘ˡⁱ_ : ∀ {G H : Functor C D} (α : NatIso G H) → (F : Functor B C)
+        → NatIso (G ∘F F) (H ∘F F)
+  _∘ˡⁱ_ {G} {H} α F .trans = α .trans ∘ˡ F
+  _∘ˡⁱ_ {G} {H} α F .nIso x = α .nIso (F ⟅ x ⟆)
diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda
index 42aa2fdb7c..350b05cbb6 100644
--- a/Cubical/Categories/Presheaf/Representable.agda
+++ b/Cubical/Categories/Presheaf/Representable.agda
@@ -33,6 +33,7 @@ open import Cubical.Reflection.RecordEquiv
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Constructions.Elements
+open import Cubical.Categories.Constructions.Opposite
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.Instances.Sets
@@ -43,7 +44,7 @@ open import Cubical.Categories.Presheaf.Properties
 open import Cubical.Categories.Yoneda
 
 private
-  variable ℓ ℓ' : Level
+  variable ℓ ℓ' ℓS : Level
 
 open Category
 open Contravariant
@@ -194,3 +195,12 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
     compIso
       Representation≅UniversalElement
       (invIso TerminalElement≅UniversalElement)
+
+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 (Covariant.isUnivalent∫ (isUnivalentOp isUnivC) P)))
diff --git a/Cubical/Data/Equality/Base.agda b/Cubical/Data/Equality/Base.agda
index e219099bc3..c092ce08d2 100644
--- a/Cubical/Data/Equality/Base.agda
+++ b/Cubical/Data/Equality/Base.agda
@@ -116,3 +116,12 @@ id x = x
 
 isEquivId : isEquiv (id {A = A})
 equiv-proof isEquivId y = (y , refl) , λ where (_ , refl) → refl
+
+HEq : {A0 A1 : Type ℓ}(Aeq : A0 ≡ A1) (a0 : A0)(a1 : A1) → Type _
+HEq Aeq a0 a1 = transport (λ A → A) Aeq a0 ≡ a1
+
+singlP : {A0 A1 : Type ℓ}(Aeq : A0 ≡ A1) (a : A0) → Type _
+singlP {A1 = A1} Aeq a = Σ[ x ∈ A1 ] HEq Aeq a x
+
+singl : {A : Type ℓ}(a : A) → Type _
+singl {A = A} a = singlP refl a
diff --git a/Cubical/Data/Graph/Displayed.agda b/Cubical/Data/Graph/Displayed.agda
new file mode 100644
index 0000000000..73fca91ea1
--- /dev/null
+++ b/Cubical/Data/Graph/Displayed.agda
@@ -0,0 +1,51 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Graph.Displayed where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Graph.Base
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.UnderlyingGraph
+open import Cubical.Categories.Displayed.Base
+
+private
+  variable
+    ℓc ℓc' ℓcᴰ ℓcᴰ' ℓd ℓd' ℓg ℓg' ℓgᴰ ℓgᴰ' ℓh ℓh' ℓhᴰ ℓhᴰ' ℓj ℓ : Level
+
+open Graph
+module _ (G : Graph ℓg ℓg') where
+  record Graphᴰ ℓgᴰ ℓgᴰ' : Type (ℓ-max (ℓ-max ℓg ℓg') (ℓ-suc (ℓ-max ℓgᴰ ℓgᴰ')))
+         where
+    no-eta-equality
+    field
+      Node[_] : G .Node → Type ℓgᴰ
+      Edge[_][_,_] : ∀ {u v} (e : G .Edge u v) (uᴰ : Node[ u ]) (vᴰ : Node[ v ])
+                   → Type ℓgᴰ'
+
+open Graphᴰ
+open Categoryᴰ
+
+module _ {G : Graph ℓg ℓg'}{H : Graph ℓh ℓh'}
+         (ϕ : GraphHom G H)
+         (Hᴰ : Graphᴰ H ℓhᴰ ℓhᴰ')
+         where
+  private
+    module G = Graph G
+    module Hᴰ = Graphᴰ Hᴰ
+  open GraphHom
+  record Section : Type (ℓ-max (ℓ-max ℓg ℓg')
+                        (ℓ-max (ℓ-max ℓh ℓh')
+                        (ℓ-max ℓhᴰ ℓhᴰ'))) where
+    field
+      _$gᴰ_ : ∀ (u : G.Node) → Hᴰ.Node[ ϕ $g u ]
+      _<$g>ᴰ_ :
+        ∀ {u v : G.Node} → (e : G.Edge u v)
+        → Hᴰ.Edge[ ϕ <$g> e ][ _$gᴰ_ u , _$gᴰ_ v ]
+
+Categoryᴰ→Graphᴰ : {C : Category ℓc ℓc'}(Cᴰ : Categoryᴰ C ℓcᴰ ℓcᴰ')
+                 → Graphᴰ (Cat→Graph C) ℓcᴰ ℓcᴰ'
+Categoryᴰ→Graphᴰ Cᴰ .Node[_] = Cᴰ .ob[_]
+Categoryᴰ→Graphᴰ Cᴰ .Edge[_][_,_] = Cᴰ .Hom[_][_,_]
+
+-- TODO: CatSection→GrSection
+
diff --git a/Cubical/Data/Quiver/Base.agda b/Cubical/Data/Quiver/Base.agda
new file mode 100644
index 0000000000..6f5acdf2de
--- /dev/null
+++ b/Cubical/Data/Quiver/Base.agda
@@ -0,0 +1,115 @@
+-- A Quiver is an endo-span of types.
+--   ob <- mor -> ob
+-- This is often used in set theory as the data over which a category
+-- is defined to be algebraic structure.
+
+-- A Quiver is equivalent to a Graph (modulo universe issues), but
+-- they are not definitionally isomorphic: turning a quiver into a
+-- graph introduces a Path between objects/nodes in the definition of
+-- an Edge.
+
+-- Since avoiding Paths generally leads to cleaner code, Graphs or
+-- Quivers may be preferable depending on the variance of a
+-- construction.
+
+-- 1. *Using* a Graph generally requires fewer paths between
+--    objects. For instance, Graphs are preferable to be used in the
+--    definition of a category because composition can be defined by
+--    sharing a common middle variable Hom[ A , B ] × Hom[ B , C ] →
+--    Hom[ A , C ], which in a Quiver would need a path (e e' : mor) →
+--    (cod e ≡ dom e') → mor.
+--
+-- 2. *Producing* a Quiver generally requires fewer paths between
+--    objects. For instance, Quivers are preferable to be used in the
+--    definition of generating data for free and presented categories.
+--    As an example, the "Funny tensor product" C ⊗ D of categories is
+--    defined by generators and relations. The generators are easy to
+--    define as a Quiver, but if defined as a graph, then the
+--    generators require a path between objects.
+
+-- So as a principle, to get the most general definitions,
+-- 1. *Produce* Graphs
+-- 2. *Use* Quivers
+-- when you can get away with it.
+
+{-# OPTIONS --safe #-}
+module Cubical.Data.Quiver.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Graph.Base
+open import Cubical.Data.Graph.Displayed as DG hiding (Section)
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.UnderlyingGraph
+open import Cubical.Categories.Displayed.Base
+
+private
+  variable
+   ℓC ℓC' ℓg ℓg' ℓgᴰ ℓgᴰ' ℓq ℓq' ℓh ℓh' ℓj ℓ : Level
+
+-- Useful in certain applications to separate this into components
+record QuiverOver (ob : Type ℓg) ℓg' : Type (ℓ-suc (ℓ-max ℓg ℓg')) where
+  field
+    mor : Type ℓg'
+    dom : mor → ob
+    cod : mor → ob
+
+open QuiverOver
+Quiver : ∀ ℓg ℓg' → Type _
+Quiver ℓg ℓg' = Σ[ ob ∈ Type ℓg ] QuiverOver ob ℓg'
+
+-- A "heteromorphism" from a Quiver to a Graph
+record HetQG (Q : Quiver ℓq ℓq') (G : Graph ℓg ℓg')
+       : Type (ℓ-max (ℓ-max ℓq ℓq') (ℓ-max ℓg ℓg')) where
+  field
+    _$g_ : Q .fst → G .Node
+    _<$g>_ : (e : Q .snd .mor)
+           → G .Edge (_$g_ (Q .snd .dom e)) (_$g_ (Q .snd .cod e))
+open HetQG public
+
+module _ {G : Graph ℓg ℓg'}
+         {H : Graph ℓh ℓh'}
+         {Q : Quiver ℓq ℓq'}
+         where
+  compGrHomHetQG : GraphHom G H → HetQG Q G → HetQG Q H
+  compGrHomHetQG ϕ h ._$g_   q = ϕ GraphHom.$g (h HetQG.$g q)
+  compGrHomHetQG ϕ h ._<$g>_ e = ϕ GraphHom.<$g> (h HetQG.<$g> e)
+
+-- Universal property:
+-- HetQG Q G ≅ QHom Q (Graph→Quiver G)
+Graph→Quiver : Graph ℓg ℓg' → Quiver ℓg (ℓ-max ℓg ℓg')
+Graph→Quiver g .fst = g .Node
+Graph→Quiver g .snd .mor = Σ[ A ∈ g .Node ] Σ[ B ∈ g .Node ] g .Edge A B
+Graph→Quiver g .snd .dom x = x .fst
+Graph→Quiver g .snd .cod x = x .snd .fst
+
+-- | The use of ≡ in this definition is the raison d'etre for the
+-- | Quiver-Graph distinction
+-- HetQG Q G ≅ QHom (Quiver→Graph Q) G
+Quiver→Graph : Quiver ℓq ℓq' → Graph _ _
+Quiver→Graph Q .Node = Q .fst
+Quiver→Graph Q .Edge A B =
+  Σ[ e ∈ Q .snd .mor ]
+    (Q .snd .dom e ≡ A)
+  × (Q .snd .cod e ≡ B)
+
+Cat→Quiver : Category ℓC ℓC' → Quiver _ _
+Cat→Quiver 𝓒 = Graph→Quiver (Cat→Graph 𝓒)
+
+-- A "heterogeneous" local section of a displayed graph
+module _ {Q : Quiver ℓq ℓq'}{G : Graph ℓg ℓg'}
+         (ϕ : HetQG Q G)
+         (Gᴰ : Graphᴰ G ℓgᴰ ℓgᴰ')
+         where
+  private
+    module Gᴰ = Graphᴰ Gᴰ
+  open HetQG
+  record HetSection : Type (ℓ-max (ℓ-max ℓq ℓq')
+                        (ℓ-max (ℓ-max ℓg ℓg')
+                        (ℓ-max ℓgᴰ ℓgᴰ'))) where
+    field
+      _$gᴰ_ : ∀ (u : Q .fst) → Gᴰ.Node[ ϕ $g u ]
+      _<$g>ᴰ_ : ∀ (e : Q .snd .mor)
+              → Gᴰ.Edge[ ϕ <$g> e
+                ][ _$gᴰ_ (Q .snd .dom e)
+                 , _$gᴰ_ (Q .snd .cod e) ]
diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda
index 237a24a251..02a87e8619 100644
--- a/Cubical/Foundations/Isomorphism.agda
+++ b/Cubical/Foundations/Isomorphism.agda
@@ -104,6 +104,15 @@ isoToEquiv : Iso A B → A ≃ B
 isoToEquiv i .fst = i .Iso.fun
 isoToEquiv i .snd = isoToIsEquiv i
 
+isoToIsIso : {f : A → B} → isIso f → Iso A B
+isoToIsIso {f = f} fIsIso .Iso.fun = f
+isoToIsIso fIsIso .Iso.inv = fIsIso .fst
+isoToIsIso fIsIso .Iso.rightInv = fIsIso .snd .fst
+isoToIsIso fIsIso .Iso.leftInv = fIsIso .snd .snd
+
+isIsoToIsEquiv : {f : A → B} → isIso f → isEquiv f
+isIsoToIsEquiv fIsIso = isoToIsEquiv (isoToIsIso fIsIso)
+
 isoToPath : Iso A B → A ≡ B
 isoToPath {A = A} {B = B} f i =
   Glue B (λ { (i = i0) → (A , isoToEquiv f)
diff --git a/Cubical/Tactics/CategorySolver/Reflection.agda b/Cubical/Tactics/CategorySolver/Reflection.agda
index 4f6ff5d596..e3ba3ac761 100644
--- a/Cubical/Tactics/CategorySolver/Reflection.agda
+++ b/Cubical/Tactics/CategorySolver/Reflection.agda
@@ -18,7 +18,7 @@ open import Cubical.Tactics.CategorySolver.Solver
 open import Cubical.Tactics.Reflection
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Category.Base
+open import Cubical.Categories.Constructions.Free.Category.Quiver as FC
 
 private
   variable
@@ -37,11 +37,15 @@ module ReflectionSolver where
 
     -- Parse the input into an exp
     buildExpression : Term → Term
-    buildExpression “id” = con (quote FreeCategory.idₑ) []
+    buildExpression “id” = con (quote FC.idₑ) []
     buildExpression (“⋆” f g) =
-      con (quote FreeCategory._⋆ₑ_)
+      con (quote FC._⋆ₑ_)
           (buildExpression f v∷ buildExpression g v∷ [])
-    buildExpression f = con (quote FreeCategory.↑_) (f v∷ [])
+    buildExpression f =
+      con (quote FC.↑_)
+      (con (quote _,_) (unknown
+      v∷ con (quote _,_) (unknown
+      v∷ f v∷ []) v∷ []) v∷ [])
 
   solve-macro : Term -- ^ The term denoting the category
               → Term -- ^ The hole whose goal should be an equality between
diff --git a/Cubical/Tactics/CategorySolver/Solver.agda b/Cubical/Tactics/CategorySolver/Solver.agda
index a79b713f32..0748789418 100644
--- a/Cubical/Tactics/CategorySolver/Solver.agda
+++ b/Cubical/Tactics/CategorySolver/Solver.agda
@@ -3,8 +3,9 @@ module Cubical.Tactics.CategorySolver.Solver where
 
 open import Cubical.Foundations.Prelude
 
+open import Cubical.Data.Quiver.Base
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Category.Base
+open import Cubical.Categories.Constructions.Free.Category.Quiver as FreeCat
 open import Cubical.Categories.Constructions.Power
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Instances.Sets
@@ -18,29 +19,36 @@ open Functor
 
 module Eval (𝓒 : Category ℓ ℓ') where
   -- Semantics in 𝓒 itself, tautologically
-  open FreeCategory (Cat→Graph 𝓒)
+  private
+    W𝓒 = FreeCat (Cat→Quiver 𝓒)
   sem𝓒 = ε {𝓒 = 𝓒}
   ⟦_⟧c = sem𝓒 .F-hom
-  𝓟 = PowerCategory (𝓒 .ob) (SET (ℓ-max ℓ ℓ'))
-  𝓘 : Functor FreeCat 𝓟
-  𝓘 = PseudoYoneda {C = FreeCat}
+  𝓟 = PowerCategory (W𝓒 .ob) (SET (ℓ-max ℓ ℓ'))
+  𝓘 : Functor W𝓒 𝓟
+  𝓘 = PseudoYoneda {C = W𝓒}
 
   -- Semantics in 𝓟 (𝓒 .ob), interpreting fun symbols using Yoneda
-  module YoSem = Semantics 𝓟 (𝓘 ∘Interp η)
-  ⟦_⟧yo = YoSem.sem .F-hom
+  semYo : Functor W𝓒 𝓟
+  semYo = rec _ (record {
+    _$g_ = 𝓘 .F-ob
+    ; _<$g>_ = λ e → 𝓘 .F-hom (FreeCat.η (Cat→Quiver 𝓒) <$g> e)
+    })
 
   -- | Evaluate by taking the semantics in 𝓟 (𝓒 .ob)
-  eval : ∀ {A B} → FreeCat [ A , B ] → _
-  eval {A}{B} e = ⟦ e ⟧yo
+  eval : ∀ {A B} → W𝓒 [ A , B ] → _
+  eval {A}{B} e = semYo .F-hom e
 
-  -- Evaluation agrees with the Yoneda embedding, and so is fully faithful
-  Yo-YoSem-agree : 𝓘 ≡ YoSem.sem
-  Yo-YoSem-agree = YoSem.sem-uniq refl
+--   -- Evaluation agrees with the Yoneda embedding, and so is fully faithful
+  Yo-YoSem-agree : 𝓘 ≡ semYo
+  Yo-YoSem-agree = FreeCatFunctor≡ _ _ _ (record
+    { _$gᴰ_ = λ _ → refl
+    ; _<$g>ᴰ_ = λ _ → refl
+    })
 
   -- If two expressions in the free category are equal when evaluated
   -- in 𝓟 (𝓒 .ob), then they are equal, and so are equal when
   -- evaluated in 𝓒.
-  solve : ∀ {A B} → (e₁ e₂ : FreeCat [ A , B ])
+  solve : ∀ {A B} → (e₁ e₂ : W𝓒 [ A , B ])
         → eval e₁ ≡ eval e₂
         → ⟦ e₁ ⟧c ≡ ⟦ e₂ ⟧c
   solve {A}{B} e₁ e₂ p = cong ⟦_⟧c (isFaithfulPseudoYoneda _ _ _ _ lem) where
@@ -51,7 +59,7 @@ module Eval (𝓒 : Category ℓ ℓ') where
 
 solve : (𝓒 : Category ℓ ℓ')
       → {A B : 𝓒 .ob}
-      → (e₁ e₂ : FreeCategory.FreeCat (Cat→Graph 𝓒) [ A , B ])
+      → (e₁ e₂ : FreeCat (Cat→Quiver 𝓒) [ A , B ])
       → (p : Eval.eval 𝓒 e₁ ≡ Eval.eval 𝓒 e₂)
       → _
 solve = Eval.solve