Remove BaseChage in favour of BaseChange*

Author: Taneb

src/Categories/Functor/Slice.agda

@@ -45,41 +45,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