Merge pull request #439 from Taneb/slice-functor-rename

Rename slice functors

Author: JacquesCarette

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)

src/Categories/Adjoint/Instance/Slice.agda

@@ -6,7 +6,7 @@ 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.Functor.Slice C using (TotalSpace; ConstantFamily)
 open import Categories.NaturalTransformation using (ntHelper)
 open import Categories.Object.Product C
 
@@ -22,8 +22,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

src/Categories/Category/CartesianClosed/Locally/Properties.agda

@@ -11,6 +11,7 @@ open import Categories.Category.Slice
 open import Categories.Category.Slice.Properties
 open import Categories.Functor
 open import Categories.Functor.Slice
+open import Categories.Functor.Slice.BaseChange
 
 private
   module C = Category C
@@ -37,7 +38,7 @@ module _ (f : A ⇒ B) where
     J = slice⇒slice-slice C f
 
     I : Functor (Slice C/B (fObj ^ fObj)) C/B
-    I = pullback-functorial C/B slice-pullbacks i
+    I = TotalSpace C/B ∘F BaseChange* C/B i (slice-pullbacks i _)
 
     K : Functor C/B/f (Slice C/B (fObj ^ fObj))
     K = Base-F C/B (fObj ⇨-)

src/Categories/Functor/Slice.agda

@@ -36,59 +36,24 @@ 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
     ; homomorphism = refl
     ; 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
       module product {X} = Product (product {X})
       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

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)