chore: push-out -> cobase-change

the1lab · Feb 1, 2023 · cdeba29 · cdeba29
1 parent fc84619
commit cdeba29
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 20 deletions.
diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md
@@ -81,10 +81,10 @@ module _ (bifib : is-bifibration) where
   open Cat.Displayed.Cartesian.Indexing ℰ fibration
   open Cat.Displayed.Cocartesian.Indexing ℰ opfibration
 
-  push-out⊣base-change
+  cobase-change⊣base-change
     : ∀ {x y} (f : Hom x y)
-    → push-out f ⊣ base-change f
-  push-out⊣base-change {x} {y} f =
+    → cobase-change f ⊣ base-change f
+  cobase-change⊣base-change {x} {y} f =
     hom-natural-iso→adjoints $
       (opfibration→hom-iso opfibration f ni⁻¹) ni∘ fibration→hom-iso fibration f
 ```
@@ -108,11 +108,11 @@ module _ (fib : Cartesian-fibration) where
   open Cartesian-fibration fib
   open Cat.Displayed.Cartesian.Indexing ℰ fib
 
-  left-adjoint-reindexing→opfibration
+  left-adjoint-base-change→opfibration
     : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y))
     → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) 
     → Cocartesian-fibration
-  left-adjoint-reindexing→opfibration L adj =
+  left-adjoint-base-change→opfibration L adj =
     cartesian+weak-opfibration→opfibration fib $
     hom-iso→weak-opfibration L λ u →
       fibration→hom-iso-from fib u ni∘ (adjunct-hom-iso-from (adj u) _ ni⁻¹)
@@ -125,8 +125,8 @@ With some repackaging, we can see that this yields a bifibration.
     : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y))
     → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f))
     → is-bifibration
-  left-adjoint-reindexing→bifibration L adj .is-bifibration.fibration =
+  left-adjoint-base-change→bifibration L adj .is-bifibration.fibration =
     fib
-  left-adjoint-reindexing→bifibration L adj .is-bifibration.opfibration =
-    left-adjoint-reindexing→opfibration L adj
+  left-adjoint-base-change→bifibration L adj .is-bifibration.opfibration =
+    left-adjoint-base-change→opfibration L adj
 ```
diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
@@ -48,21 +48,18 @@ adding in empty fibres.
 [the canonical self-indexing]: Cat.Displayed.Instances.Slice.html
 [pullbacks]: Cat.Diagram.Pullback.html
 
-Continuing the analogy of indexing as pullback, we call the opreindexing
-functors _pushouts_.
-
 ```agda
-push-out : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)
-push-out f .F₀ ob = has-lift.y′ f ob
-push-out f .F₁ vert = rebase f vert
+cobase-change : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)
+cobase-change f .F₀ ob = has-lift.y′ f ob
+cobase-change f .F₁ vert = rebase f vert
 ```
 
 <!--
 ```agda
-push-out f .F-id =
+cobase-change f .F-id =
   sym $ has-lift.uniquev _ _ _ $ to-pathp $
     idl[] ∙ (sym $ cancel _ _ (idr′ _))
-push-out f .F-∘ f′ g′ =
+cobase-change f .F-∘ f′ g′ =
   sym $ has-lift.uniquev _ _ _ $ to-pathp $
     smashl _ _
     ·· revive₁ (pullr[] _ (has-lift.commutesv _ _ _))

diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
@@ -680,13 +680,13 @@ module _ (opfib : Cocartesian-fibration) where
     : ∀ {x y y′} (u : Hom x y)
     → natural-iso
         (Hom-over-into ℰ u y′)
-        (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (push-out u) )
+        (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) )
   opfibration→hom-iso-into {y = y} {y′ = y′} u = to-natural-iso mi where
     open make-natural-iso
 
     mi : make-natural-iso
            (Hom-over-into ℰ u y′)
-           (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (push-out u) )
+           (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) )
     mi .eta x u′ = has-lift.universalv u x u′
     mi .inv x v′ = hom[ idl u ] (v′ ∘′ has-lift.lifting u _)
     mi .eta∘inv x = funext λ v′ →
@@ -703,7 +703,9 @@ module _ (opfib : Cocartesian-fibration) where
 
   opfibration→hom-iso
     : ∀ {x y} (u : Hom x y)
-    → natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (push-out u) F× Id))
+    → natural-iso
+        (Hom-over ℰ u)
+        (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id))
   opfibration→hom-iso {y = y} u = to-natural-iso mi where
     open make-natural-iso
     open _=>_
@@ -715,7 +717,7 @@ module _ (opfib : Cocartesian-fibration) where
 
     mi : make-natural-iso
            (Hom-over ℰ u)
-           (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (push-out u) F× Id))
+           (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id))
     mi .eta x u′ = has-lift.universalv u _ u′
     mi .inv x v′ = hom[ idl u ] (v′ ∘′ has-lift.lifting u _)
     mi .eta∘inv x = funext λ v′ →