diff --git a/src/Categories/Adjoint/Instance/BaseChange.agda b/src/Categories/Adjoint/Instance/BaseChange.agda
index 937f1042..1441646c 100644
--- a/src/Categories/Adjoint/Instance/BaseChange.agda
+++ b/src/Categories/Adjoint/Instance/BaseChange.agda
@@ -6,7 +6,7 @@ module Categories.Adjoint.Instance.BaseChange {o ℓ e} (C : Category o ℓ e) w
 
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Adjoint.Compose using (_∘⊣_)
-open import Categories.Adjoint.Instance.Slice using (Forgetful⊣Free)
+open import Categories.Adjoint.Instance.Slice using (TotalSpace⊣ConstantFamily)
 open import Categories.Category.Slice C using (Slice)
 open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice≃slice)
 open import Categories.Category.Equivalence.Properties using (module C≅D)
@@ -18,4 +18,4 @@ open Category C
 module _ {A B : Obj} (f : B ⇒ A) (pullback : ∀ {C} {h : C ⇒ A} → Pullback f h) where
 
   !⊣* : BaseChange! f ⊣ BaseChange* f pullback
-  !⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ Forgetful⊣Free (Slice A) (pullback⇒product pullback)
+  !⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ TotalSpace⊣ConstantFamily (Slice A) (pullback⇒product pullback)
diff --git a/src/Categories/Adjoint/Instance/Slice.agda b/src/Categories/Adjoint/Instance/Slice.agda
index 1f425c51..195ad871 100644
--- a/src/Categories/Adjoint/Instance/Slice.agda
+++ b/src/Categories/Adjoint/Instance/Slice.agda
@@ -5,10 +5,18 @@ open import Categories.Category using (Category)
 module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where
 
 open import Categories.Adjoint using (_⊣_)
-open import Categories.Category.Slice C using (SliceObj; Slice⇒; slicearr)
-open import Categories.Functor.Slice C using (Forgetful; Free)
+open import Categories.Category.BinaryProducts C
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.Slice C using (SliceObj; sliceobj; Slice⇒; slicearr)
+open import Categories.Functor.Slice C using (TotalSpace; ConstantFamily; InternalSections)
+open import Categories.Morphism.Reasoning C
 open import Categories.NaturalTransformation using (ntHelper)
+open import Categories.Diagram.Pullback C hiding (swap)
 open import Categories.Object.Product C
+open import Categories.Object.Terminal C
+
+open import Function.Base using (_$_)
 
 open Category C
 open HomReasoning
@@ -22,8 +30,8 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where
     module product {X} = Product (product {X})
     open product
 
-  Forgetful⊣Free : Forgetful ⊣ Free product
-  Forgetful⊣Free = record
+  TotalSpace⊣ConstantFamily : TotalSpace ⊣ ConstantFamily product
+  TotalSpace⊣ConstantFamily = record
     { unit = ntHelper record
       { η = λ _ → slicearr project₁
       ; commute = λ {X} {Y} f → begin
@@ -44,3 +52,93 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where
       ⟨ π₁ , π₂ ⟩                               ≈⟨ η ⟩
       id                                        ∎
     }
+
+module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
+
+  open CartesianClosed ccc
+  open Cartesian cartesian
+  open Terminal terminal
+  open BinaryProducts products
+
+  ConstantFamily⊣InternalSections : ConstantFamily {A = A} product ⊣ InternalSections ccc pullback
+  ConstantFamily⊣InternalSections = record
+    { unit = ntHelper record
+      { η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X))
+      ; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin
+        p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ f                                       ≈⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
+        λg swap ∘ f                                                                                ≈⟨ subst ⟩
+        λg (swap ∘ first f)                                                                        ≈⟨ λ-cong swap∘⁂ ⟩
+        λg (second f ∘ swap)                                                                       ≈˘⟨ λ-cong (∘-resp-≈ʳ β′) ⟩
+        λg (second f ∘ eval′ ∘ first (λg swap))                                                    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (first-cong (p.p₂∘universal≈h₂ (sliceobj π₁))))) ⟩
+        λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _))           ≈˘⟨ λ-cong (pull-last first∘first) ⟩
+        λg ((second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ first (p.universal (sliceobj π₁) _)) ≈˘⟨ subst ⟩
+        λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _           ≈˘⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
+        p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ p.universal (sliceobj π₁) _             ∎
+      }
+    ; counit = ntHelper record
+      { η = λ X → slicearr (counit-△ X)
+      ; commute = λ {S} {T} f → begin
+        (eval′ ∘ first (p.p₂ T) ∘ swap) ∘ second (p.universal T _) ≈⟨ pull-last swap∘⁂ ⟩
+        eval′ ∘ first (p.p₂ T) ∘ first (p.universal T _) ∘ swap    ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
+        eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap            ≈⟨ refl⟩∘⟨ first-cong (p.p₂∘universal≈h₂ T) ⟩∘⟨refl ⟩
+        eval′ ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∘ swap   ≈⟨ pullˡ β′ ⟩
+        (h f ∘ eval′ ∘ first (p.p₂ S)) ∘ swap                      ≈⟨ assoc²' ⟩
+        h f ∘ eval′ ∘ first (p.p₂ S) ∘ swap                        ∎
+      }
+    ; zig = λ {X} → begin
+      (eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap) ∘ second (p.universal (sliceobj π₁) _) ≈⟨ assoc²' ⟩
+      eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap ∘ second (p.universal (sliceobj π₁) _)   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘⁂ ⟩
+      eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ first (p.universal (sliceobj π₁) _) ∘ swap    ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
+      eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap            ≈⟨ refl⟩∘⟨ first-cong (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩∘⟨refl ⟩
+      eval′ ∘ first (λg swap) ∘ swap                                                     ≈⟨ pullˡ β′ ⟩
+      swap ∘ swap                                                                        ≈⟨ swap∘swap ⟩
+      id                                                                                 ∎
+    ; zag = λ {X} → p.unique-diagram X !-unique₂ $ begin
+      p.p₂ X ∘ p.universal X _ ∘ p.universal (sliceobj π₁) _                                                  ≈⟨ pullˡ (p.p₂∘universal≈h₂ X) ⟩
+      λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩
+      λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _         ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩
+      λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap                                                  ≈⟨ subst ⟩
+      λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap))                                        ≈⟨ λ-cong (pullʳ β′) ⟩
+      λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap)                                                             ≈⟨ λ-cong (pullʳ (cancelʳ swap∘swap)) ⟩
+      λg (eval′ ∘ first (p.p₂ X))                                                                             ≈⟨ η-exp′ ⟩
+      p.p₂ X                                                                                                  ≈˘⟨ identityʳ ⟩
+      p.p₂ X ∘ id                                                                                             ∎
+    }
+    where
+      p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′))
+      p X = pullback (λg π₂) (λg (arr X ∘ eval′))
+      module p X = Pullback (p X)
+
+      abstract
+        unit-pb : ∀ (X : Obj) → eval′ ∘ first {A = X} {C = A} (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap)
+        unit-pb X = begin
+          eval′ ∘ first (λg π₂ ∘ !)                         ≈˘⟨ refl⟩∘⟨ first∘first ⟩
+          eval′ ∘ first (λg π₂) ∘ first !                   ≈⟨ pullˡ β′ ⟩
+          π₂ ∘ first !                                      ≈⟨ π₂∘⁂ ○ identityˡ ⟩
+          π₂                                                ≈˘⟨ project₁ ⟩
+          π₁ ∘ swap                                         ≈˘⟨ refl⟩∘⟨ β′ ⟩
+          π₁ ∘ eval′ ∘ first (λg swap)                      ≈˘⟨ extendʳ β′ ⟩
+          eval′ ∘ first (λg (π₁ ∘ eval′)) ∘ first (λg swap) ≈⟨ refl⟩∘⟨ first∘first ⟩
+          eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap)         ∎
+        -- A good chunk of the above, maybe all if you squint, is duplicated with F₁-lemma
+        -- eval′ ∘ first (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (f ∘ eval′) ∘ first (λg g)
+        -- With f : X ⇒ Y and g : Z × Y ⇒ X. Not sure what conditions f and g need to have
+
+        -- Would it be better if Free used π₂ rather than π₁?
+        -- It would mean we could avoid this swap
+        counit-△ : ∀ X → arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈ π₁
+        counit-△ X = begin
+          arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap     ≈˘⟨ assoc² ⟩
+          ((arr X ∘ eval′) ∘ first (p.p₂ X)) ∘ swap ≈⟨ lemma ⟩∘⟨refl ⟩
+          (π₂ ∘ first (p.p₁ X)) ∘ swap              ≈⟨ (π₂∘⁂ ○ identityˡ) ⟩∘⟨refl ⟩
+          π₂ ∘ swap                                 ≈⟨ project₂ ⟩
+          π₁                                        ∎
+          where
+            lemma : (arr X ∘ eval′) ∘ first (p.p₂ X) ≈ π₂ ∘ first (p.p₁ X)
+            lemma = λ-inj $ begin
+              λg ((arr X ∘ eval′) ∘ first (p.p₂ X)) ≈˘⟨ subst ⟩
+              λg (arr X ∘ eval′) ∘ p.p₂ X         ≈˘⟨ p.commute X ⟩
+              λg π₂ ∘ p.p₁ X                      ≈⟨ subst ⟩
+              λg (π₂ ∘ first (p.p₁ X))            ∎
+
+
diff --git a/src/Categories/Category/BinaryProducts.agda b/src/Categories/Category/BinaryProducts.agda
index 1b0cc33b..3f5907a7 100644
--- a/src/Categories/Category/BinaryProducts.agda
+++ b/src/Categories/Category/BinaryProducts.agda
@@ -94,6 +94,12 @@ record BinaryProducts : Set (levelOfTerm 𝒞) where
   ⁂-cong₂ : f ≈ g → h ≈ i → f ⁂ h ≈ g ⁂ i
   ⁂-cong₂ = [ product ⇒ product ]×-cong₂
 
+  first-cong : f ≈ g → f ⁂ h ≈ g ⁂ h
+  first-cong f≈g = ⁂-cong₂ f≈g Equiv.refl
+
+  second-cong : g ≈ h → f ⁂ g ≈ f ⁂ h
+  second-cong g≈h = ⁂-cong₂ Equiv.refl g≈h
+
   ⁂∘⟨⟩ : (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g ∘ g′ ⟩
   ⁂∘⟨⟩ = [ product ⇒ product ]×∘⟨⟩
 
diff --git a/src/Categories/Category/CartesianClosed.agda b/src/Categories/Category/CartesianClosed.agda
index 8f35da80..6eae7735 100644
--- a/src/Categories/Category/CartesianClosed.agda
+++ b/src/Categories/Category/CartesianClosed.agda
@@ -56,7 +56,7 @@ record CartesianClosed : Set (levelOfTerm 𝒞) where
   open CartesianMonoidal cartesian using (A×⊤≅A)
   open BinaryProducts cartesian.products using (_×_; product; π₁; π₂; ⟨_,_⟩;
     project₁; project₂; η; ⟨⟩-cong₂; ⟨⟩∘; _⁂_; ⟨⟩-congˡ; ⟨⟩-congʳ;
-    first∘first; firstid; first; second; first↔second; second∘second; ⁂-cong₂; -×_)
+    first∘first; firstid; first; second; first↔second; second∘second; second-cong; -×_)
   open Terminal cartesian.terminal using (⊤; !; !-unique₂; ⊤-id)
 
   B^A×A : ∀ B A → Product (B ^ A) A
@@ -194,7 +194,7 @@ record CartesianClosed : Set (levelOfTerm 𝒞) where
     ; identity     = λ-cong (identityˡ ○ (elimʳ (id×id product))) ○ η-id′
     ; homomorphism = λ-unique₂′ helper
     ; F-resp-≈     = λ where
-      (eq₁ , eq₂) → λ-cong (∘-resp-≈ eq₂ (∘-resp-≈ʳ (⁂-cong₂ refl eq₁)))
+      (eq₁ , eq₂) → λ-cong (∘-resp-≈ eq₂ (∘-resp-≈ʳ (second-cong eq₁)))
     }
     where helper : eval′ ∘ first (λg ((g ∘ f) ∘ eval′ ∘ second (h ∘ i)))
                  ≈ eval′ ∘ first (λg (g ∘ eval′ ∘ second i) ∘ λg (f ∘ eval′ ∘ second h))
diff --git a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
index fbc127f0..4492be0a 100644
--- a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
+++ b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
@@ -55,7 +55,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi
       in begin
         F.₁ (second (f C.∘ g)) ⟨$⟩ x                ≈˘⟨ [ F ]-resp-∘ second∘second ⟩
         F.₁ (second g) ⟨$⟩ (F.₁ (second f) ⟨$⟩ x) ∎
-    ; F-resp-≈     = λ {Y Z} {f g} eq → F.F-resp-≈ (⁂-cong₂ C.Equiv.refl eq)
+    ; F-resp-≈     = λ {Y Z} {f g} eq → F.F-resp-≈ (second-cong eq)
     }
     where module F = Functor F
 
@@ -79,7 +79,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi
       in begin
         F₁ (first (f C.∘ g)) ⟨$⟩ x              ≈˘⟨ [ F ]-resp-∘ first∘first ⟩
         F₁ (first g) ⟨$⟩ (F₁ (first f) ⟨$⟩ x) ∎
-    ; F-resp-≈     = λ {A B} {f g} eq → F-resp-≈ (⁂-cong₂ eq C.Equiv.refl)
+    ; F-resp-≈     = λ {A B} {f g} eq → F-resp-≈ (first-cong eq)
     }
     where open Functor F
 
@@ -113,7 +113,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi
           F.₁ C.id ⟨$⟩ (α.η Y ⟨$⟩ x)         ≈⟨ F.identity ⟩
           α.η Y ⟨$⟩ x                        ∎
       ; homomorphism = λ {X Y Z} → Setoid.sym (F.₀ (Z × _)) ([ F ]-resp-∘ first∘first)
-      ; F-resp-≈     = λ eq → F.F-resp-≈ (⁂-cong₂ eq C.Equiv.refl)
+      ; F-resp-≈     = λ eq → F.F-resp-≈ (first-cong eq)
       }
 
 module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
diff --git a/src/Categories/Category/Construction/Pullbacks.agda b/src/Categories/Category/Construction/Pullbacks.agda
index 54138bdc..212aee57 100644
--- a/src/Categories/Category/Construction/Pullbacks.agda
+++ b/src/Categories/Category/Construction/Pullbacks.agda
@@ -33,12 +33,16 @@ record Pullback⇒ W (X Y : PullbackObj W) : Set (o ⊔ ℓ ⊔ e) where
     commute₁ : Y.arr₁ ∘ mor₁ ≈ X.arr₁
     commute₂ : Y.arr₂ ∘ mor₂ ≈ X.arr₂
 
+  private abstract
+    pbarrlemma : Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈ Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂
+    pbarrlemma = begin
+      Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈⟨ pullˡ commute₁ ⟩
+      X.arr₁ ∘ X.pullback.p₁        ≈⟨ X.pullback.commute ⟩
+      X.arr₂ ∘ X.pullback.p₂        ≈˘⟨ pullˡ commute₂ ⟩
+      Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ ∎
+
   pbarr : X.pullback.P ⇒ Y.pullback.P
-  pbarr = Y.pullback.universal $ begin
-    Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈⟨ pullˡ commute₁ ⟩
-    X.arr₁ ∘ X.pullback.p₁        ≈⟨ X.pullback.commute ⟩
-    X.arr₂ ∘ X.pullback.p₂        ≈˘⟨ pullˡ commute₂ ⟩
-    Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ ∎
+  pbarr = Y.pullback.universal pbarrlemma
 
 open Pullback⇒
 
diff --git a/src/Categories/Functor/Slice.agda b/src/Categories/Functor/Slice.agda
index 6121dd81..06d09827 100644
--- a/src/Categories/Functor/Slice.agda
+++ b/src/Categories/Functor/Slice.agda
@@ -4,16 +4,22 @@ open import Categories.Category using (Category)
 
 module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where
 
-open import Function using () renaming (id to id→)
+open import Function.Base using (_$_) renaming (id to id→)
 
+open import Categories.Category.BinaryProducts
+open import Categories.Category.Cartesian
+open import Categories.Category.CartesianClosed C
 open import Categories.Diagram.Pullback C using (Pullback; unglue; Pullback-resp-≈)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Properties using ([_]-resp-∘)
 open import Categories.Morphism.Reasoning C
+open import Categories.Object.Exponential C
 open import Categories.Object.Product C
+open import Categories.Object.Terminal C
 
 import Categories.Category.Slice as S
 import Categories.Category.Construction.Pullbacks as Pbs
+import Categories.Object.Product.Construction as ×C
 
 open Category C
 open HomReasoning
@@ -36,8 +42,8 @@ module _ {A : Obj} where
 
   open S C
 
-  Forgetful : Functor (Slice A) C
-  Forgetful = record
+  TotalSpace : Functor (Slice A) C
+  TotalSpace = record
     { F₀           = Y
     ; F₁           = h
     ; identity     = refl
@@ -45,41 +51,6 @@ module _ {A : Obj} where
     ; F-resp-≈     = id→
     }
 
-  module _ (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
-    private
-      module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i)
-      open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁)
-
-    pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C
-    pullback-functorial f = record
-      { F₀           = λ X → p.P X
-      ; F₁           = λ f → p⇒ _ _ f
-      ; identity     = λ {X} → sym (p.unique X id-comm id-comm)
-      ; homomorphism = λ {_ Y Z} →
-        p.unique-diagram Z (p.p₁∘universal≈h₁ Z ○ ⟺ identityˡ ○ ⟺ (pullʳ (p.p₁∘universal≈h₁ Y)) ○ ⟺ (pullˡ (p.p₁∘universal≈h₁ Z)))
-                           (p.p₂∘universal≈h₂ Z ○ assoc ○ ⟺ (pullʳ (p.p₂∘universal≈h₂ Y)) ○ ⟺ (pullˡ (p.p₂∘universal≈h₂ Z)))
-      ; F-resp-≈     = λ {_ B} {h i} eq →
-        p.unique-diagram B (p.p₁∘universal≈h₁ B ○ ⟺ (p.p₁∘universal≈h₁ B))
-                           (p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B))
-      }
-      where p : ∀ X → Pullback f (arr X)
-            p X        = pullback f (arr X)
-            module p X = Pullback (p X)
-
-            p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y
-            p⇒ X Y g = Pbs.Pullback⇒.pbarr pX⇒pY
-              where pX : Pbs.PullbackObj C A
-                    pX = record { pullback = p X }
-                    pY : Pbs.PullbackObj C A
-                    pY = record { pullback = p Y }
-                    pX⇒pY : Pbs.Pullback⇒ C A pX pY
-                    pX⇒pY = record
-                      { mor₁     = Category.id C
-                      ; mor₂     = h g
-                      ; commute₁ = identityʳ
-                      ; commute₂ = △ g
-                      }
-
   module _ (product : {X : Obj} → Product A X) where
 
     private
@@ -87,8 +58,8 @@ module _ {A : Obj} where
       open product
 
     -- this is adapted from proposition 1.33 of Aspects of Topoi (Freyd, 1972)
-    Free : Functor C (Slice A)
-    Free = record
+    ConstantFamily : Functor C (Slice A)
+    ConstantFamily = record
       { F₀ = λ _ → sliceobj π₁
       ; F₁ = λ f → slicearr ([ product ⇒ product ]π₁∘× ○ identityˡ)
       ; identity = id×id product
@@ -96,3 +67,57 @@ module _ {A : Obj} where
       ; F-resp-≈ = λ f≈g → ⟨⟩-cong₂ refl (∘-resp-≈ˡ f≈g)
       }
 
+  -- This can and probably should be restricted
+  -- e.g. we only need exponential objects with A as domain
+  -- I don't think we need all products but I don't have a clear idea of what products we do need
+  module _ (ccc : CartesianClosed) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
+
+    open CartesianClosed ccc
+    open Cartesian cartesian
+    open Terminal terminal
+    open BinaryProducts products
+
+    InternalSections : Functor (Slice A) C
+    InternalSections = record
+      { F₀ = p.P
+      ; F₁ = λ f → p.universal _ (F₁-lemma f)
+      ; identity = λ {X} → sym $ p.unique X (sym (!-unique _)) $ begin
+        p.p₂ X ∘ id                      ≈⟨ identityʳ ⟩
+        p.p₂ X                           ≈˘⟨ η-exp′ ⟩
+        λg (eval′ ∘ first (p.p₂ X))      ≈˘⟨ λ-cong (pullˡ identityˡ) ⟩
+        λg (id ∘ eval′ ∘ first (p.p₂ X)) ∎
+      ; homomorphism = λ {S} {T} {U} {f} {g} → sym $ p.unique U (sym (!-unique _)) $ begin
+        p.p₂ U ∘ p.universal U (F₁-lemma g) ∘ p.universal T (F₁-lemma f) ≈⟨ pullˡ (p.p₂∘universal≈h₂ U) ⟩
+        λg (h g ∘ eval′ ∘ first (p.p₂ T)) ∘ p.universal T (F₁-lemma f)   ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩
+        λg (h g ∘ eval′) ∘ p.p₂ T ∘ p.universal T (F₁-lemma f)           ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ T ⟩
+        λg (h g ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S))             ≈⟨ subst ⟩
+        λg ((h g ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))))   ≈⟨ λ-cong (pullʳ β′) ⟩
+        λg (h g ∘ (h f ∘ eval′ ∘ first (p.p₂ S)))                        ≈⟨ λ-cong sym-assoc ⟩
+        λg ((h g ∘ h f) ∘ eval′ ∘ first (p.p₂ S))                        ∎
+      ; F-resp-≈ = λ f≈g → p.universal-resp-≈ _ refl (λ-cong (∘-resp-≈ˡ f≈g))
+      }
+      where
+        p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′))
+        p X = pullback (λg π₂) (λg (arr X ∘ eval′))
+        module p X = Pullback (p X)
+
+        abstract
+          F₁-lemma : ∀ {S} {T} (f : Slice⇒ S T) → λg π₂ ∘ ! ≈ λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S))
+          F₁-lemma {S} {T} f = λ-unique₂′ $ begin
+            eval′ ∘ first (λg π₂ ∘ !)                                                      ≈˘⟨ refl⟩∘⟨ first∘first ⟩
+            eval′ ∘ first (λg π₂) ∘ first !                                                ≈⟨ pullˡ β′ ⟩
+            π₂ ∘ first !                                                                   ≈⟨ π₂∘⁂ ○ identityˡ ⟩
+            π₂                                                                             ≈⟨ λ-inj lemma ⟩
+            arr S ∘ eval′ ∘ first (p.p₂ S)                                                 ≈˘⟨ pullˡ (△ f) ⟩
+            arr T ∘ h f ∘ eval′ ∘ first (p.p₂ S)                                           ≈˘⟨ pullʳ β′ ⟩
+            (arr T ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S)))                    ≈˘⟨ pullˡ β′ ⟩
+            eval′ ∘ first (λg (arr T ∘ eval′)) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ≈⟨ refl⟩∘⟨ first∘first ⟩
+            eval′ ∘ first (λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S)))         ∎
+            where
+              lemma : λg π₂ ≈ λg (arr S ∘ eval′ ∘ first (p.p₂ S))
+              lemma = begin
+                λg π₂                               ≈˘⟨ λ-cong (π₂∘⁂ ○ identityˡ) ⟩
+                λg (π₂ ∘ first (p.p₁ S))            ≈˘⟨ subst ⟩
+                λg π₂ ∘ p.p₁ S                      ≈⟨ p.commute S ⟩
+                λg (arr S ∘ eval′) ∘ p.p₂ S         ≈⟨ subst ○ λ-cong assoc ⟩
+                λg (arr S ∘ eval′ ∘ first (p.p₂ S)) ∎
diff --git a/src/Categories/Functor/Slice/BaseChange.agda b/src/Categories/Functor/Slice/BaseChange.agda
index 84ab8d87..937502e5 100644
--- a/src/Categories/Functor/Slice/BaseChange.agda
+++ b/src/Categories/Functor/Slice/BaseChange.agda
@@ -7,7 +7,7 @@ module Categories.Functor.Slice.BaseChange {o ℓ e} (C : Category o ℓ e) wher
 open import Categories.Category.Slice C using (Slice)
 open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice⇒slice; slice⇒slice-slice)
 open import Categories.Functor using (Functor; _∘F_)
-open import Categories.Functor.Slice using (Forgetful; Free)
+open import Categories.Functor.Slice using (TotalSpace; ConstantFamily)
 open import Categories.Diagram.Pullback C using (Pullback)
 
 open Category C
@@ -16,9 +16,9 @@ module _ {A B : Obj} (f : B ⇒ A) where
 
   -- Any morphism induces a functor between slices.
   BaseChange! : Functor (Slice B) (Slice A)
-  BaseChange! = Forgetful (Slice A) ∘F slice⇒slice-slice f
+  BaseChange! = TotalSpace (Slice A) ∘F slice⇒slice-slice f
 
   -- Any morphism which admits pullbacks induces a functor the other way between slices.
   -- This is adjoint to BaseChange!: see Categories.Adjoint.Instance.BaseChange.
   BaseChange* : (∀ {C} {h : C ⇒ A} → Pullback f h) → Functor (Slice A) (Slice B)
-  BaseChange* pullback = slice-slice⇒slice f ∘F Free (Slice A) (pullback⇒product pullback)
+  BaseChange* pullback = slice-slice⇒slice f ∘F ConstantFamily (Slice A) (pullback⇒product pullback)
diff --git a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda
index 639ad1db..13828d57 100644
--- a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda
+++ b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda
@@ -59,7 +59,7 @@ NNO×CCC⇒PNNO nno = record
     commute₂' {A} {X} {f} {g} = begin
       g ∘ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap                       ≈⟨ pullˡ (pullˡ (⟺ β′)) ⟩
       ((eval′ ∘ (λg (g ∘ eval′) ⁂ id)) ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ (pullʳ ⁂∘⁂) ⟩∘⟨refl ⟩
-      (eval′ ∘ (λg (g ∘ eval′) ∘  universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap    ≈⟨ (refl⟩∘⟨ (⁂-cong₂ s-commute refl)) ⟩∘⟨refl ⟩
+      (eval′ ∘ (λg (g ∘ eval′) ∘  universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap    ≈⟨ (refl⟩∘⟨ (first-cong s-commute)) ⟩∘⟨refl ⟩
       (eval′ ∘ (universal (λg (f ∘ π₂))  (λg (g ∘ eval′)) ∘ s ⁂ id ∘ id)) ∘ swap                 ≈⟨ (refl⟩∘⟨ (⟺ ⁂∘⁂)) ⟩∘⟨refl ⟩
       (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ (s ⁂ id)) ∘ swap                ≈⟨ pullʳ (pullʳ (⟺ swap∘⁂)) ⟩
       eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ swap ∘ (id ⁂ s)                  ≈⟨ sym-assoc ○ sym-assoc ⟩
@@ -71,7 +71,7 @@ NNO×CCC⇒PNNO nno = record
       λg (u ∘ swap)                                                                  ≈⟨ nno-unique 
         (⟺ (λ-unique′ 
           (begin 
-            eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id)        ≈⟨ refl⟩∘⟨ ⟺ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ 
+            eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id)        ≈⟨ refl⟩∘⟨ ⟺ (⁂∘⁂ ○ second-cong identity²) ⟩
             eval′ ∘ (λg (u ∘ swap) ⁂ id) ∘ (z ⁂ id) ≈⟨ pullˡ β′ ⟩
             (u ∘ swap) ∘ (z ⁂ id)                   ≈⟨ pullʳ swap∘⁂ ⟩
             u ∘ (id ⁂ z) ∘ swap                     ≈⟨ pushʳ (bp-unique′