diff --git a/src/Cat/Displayed/Adjoint.lagda.md b/src/Cat/Displayed/Adjoint.lagda.md
index 1233ad61e..584a4efb7 100644
--- a/src/Cat/Displayed/Adjoint.lagda.md
+++ b/src/Cat/Displayed/Adjoint.lagda.md
@@ -1,11 +1,19 @@
@@ -103,10 +111,10 @@ module _
{ℱ : Displayed B of ℓf}
where
private
- open Precategory B
- module ℰ = Displayed ℰ
- module ℱ = Displayed ℱ
- open Vertical-fibred-functor
+ open Cat.Reasoning B
+ module ℱ = Cat.Displayed.Reasoning ℱ
+ module ℰ = Cat.Displayed.Reasoning ℰ
+ open Vertical-functor
lvl : Level
lvl = ob ⊔ ℓb ⊔ oe ⊔ ℓe ⊔ of ⊔ ℓf
@@ -117,13 +125,13 @@ module _
```agda
record _⊣↓_
- (L : Vertical-fibred-functor ℰ ℱ)
- (R : Vertical-fibred-functor ℱ ℰ)
+ (L : Vertical-functor ℰ ℱ)
+ (R : Vertical-functor ℱ ℰ)
: Type lvl where
no-eta-equality
field
- unit′ : IdVf =>f↓ R Vf∘ L
- counit′ : L Vf∘ R =>f↓ IdVf
+ unit′ : IdV =>↓ R V∘ L
+ counit′ : L V∘ R =>↓ IdV
module unit′ = _=>↓_ unit′
module counit′ = _=>↓_ counit′ renaming (η′ to ε′)
@@ -133,4 +141,241 @@ module _
→ counit′.ε′ (L .F₀′ x′) ℱ.∘′ L .F₁′ (unit′.η′ x′) ℱ.≡[ idl id ] ℱ.id′
zag′ : ∀ {x} {x′ : ℱ.Ob[ x ]}
→ R .F₁′ (counit′.ε′ x′) ℰ.∘′ unit′.η′ (R .F₀′ x′) ℰ.≡[ idl id ] ℰ.id′
+
+ _⊣f↓_ : Vertical-fibred-functor ℰ ℱ → Vertical-fibred-functor ℱ ℰ → Type _
+ L ⊣f↓ R = Vertical-fibred-functor.vert L ⊣↓ Vertical-fibred-functor.vert R
+```
+
+## Vertical Adjuncts
+
+If $L \dashv R$ is a vertical adjunction, then we can define displayed
+versions of [adjuncts]. The vertical assumption is critical here; it
+allows us to keep morphisms displayed over the same base.
+
+[adjuncts]: Cat.Functor.Adjoint.html#adjuncts
+
+
+
+```agda
+ L-adjunct′
+ : ∀ {x y x′ y′} {f : Hom x y}
+ → ℱ.Hom[ f ] (L.₀′ x′) y′ → ℰ.Hom[ f ] x′ (R.₀′ y′)
+ L-adjunct′ f′ = ℰ.hom[ idr _ ] (R.₁′ f′ ℰ.∘′ unit′.η′ _)
+
+ R-adjunct′
+ : ∀ {x y x′ y′} {f : Hom x y}
+ → ℰ.Hom[ f ] x′ (R.₀′ y′) → ℱ.Hom[ f ] (L.₀′ x′) y′
+ R-adjunct′ f′ = ℱ.hom[ idl _ ] (counit′.ε′ _ ℱ.∘′ L.₁′ f′)
+```
+
+As in the 1-categorical case, we obtain an equivalence between hom-sets
+$\hom(La,b)$ and $\hom(a,Rb)$ over $f$.
+
+```agda
+ L-R-adjunct′
+ : ∀ {x y} {f : Hom x y} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]}
+ → is-right-inverse (R-adjunct′ {x′ = x′} {y′} {f}) L-adjunct′
+ L-R-adjunct′ f′ =
+ ℰ.hom[] (R.₁′ (ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (idr _) (ap₂ ℰ._∘′_ (R.F-∘[] _ _) refl) ⟩
+ ℰ.hom[] (ℰ.hom[] (R.₁′ (counit′.ε′ _) ℰ.∘′ R.₁′ (L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.smashl _ _ ⟩
+ ℰ.hom[] ((R.₁′ (counit′.ε′ _) ℰ.∘′ R.₁′ (L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (eliml (idl _)) (ℰ.extendr[] _ (symP $ unit′.is-natural′ _ _ _)) ⟩
+ ℰ.hom[] ((R.₁′ (counit′.ε′ _) ℰ.∘′ unit′.η′ _) ℰ.∘′ f′) ≡⟨ ℰ.shiftl _ (ℰ.eliml[] _ zag′) ⟩
+ f′ ∎
+
+ R-L-adjunct′
+ : ∀ {x y} {f : Hom x y} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]}
+ → is-left-inverse (R-adjunct′ {x′ = x′} {y′} {f}) L-adjunct′
+ R-L-adjunct′ f′ =
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (ℰ.hom[] (R.₁′ f′ ℰ.∘′ unit′.η′ _))) ≡⟨ ℱ.weave _ _ (idl _) (ap₂ ℱ._∘′_ refl (L.F-∘[] _ _)) ⟩
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ ℱ.hom[] (L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ (unit′.η′ _))) ≡⟨ ℱ.smashr _ _ ⟩
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ (unit′.η′ _)) ≡⟨ ℱ.weave _ _ (elimr (idl _)) (ℱ.extendl[] _ (counit′.is-natural′ _ _ _)) ⟩
+ ℱ.hom[] (f′ ℱ.∘′ counit′.ε′ _ ℱ.∘′ L.₁′ (unit′.η′ _)) ≡⟨ ℱ.shiftl _ (ℱ.elimr[] _ zig′) ⟩
+ f′ ∎
+```
+
+This equivalence is natural.
+
+```agda
+ L-adjunct-naturall′
+ : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℰ.Ob[ y ]} {z′ : ℱ.Ob[ z ]}
+ → {f : Hom y z} {g : Hom x y}
+ → (f′ : ℱ.Hom[ f ] (L.₀′ y′) z′) (g′ : ℰ.Hom[ g ] x′ y′)
+ → L-adjunct′ (f′ ℱ.∘′ L.₁′ g′) ≡ L-adjunct′ f′ ℰ.∘′ g′
+ L-adjunct-naturall′ {g = g} f′ g′ =
+ ℰ.hom[] (R.₁′ (f′ ℱ.∘′ L.₁′ g′) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (idr _) (ap₂ ℰ._∘′_ R.F-∘′ refl) ⟩
+ ℰ.hom[] ((R.₁′ f′ ℰ.∘′ R.₁′ (L.₁′ g′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (ap (_∘ g) (idr _)) (ℰ.extendr[] _ (symP $ unit′.is-natural′ _ _ _)) ⟩
+ ℰ.hom[] ((R.₁′ f′ ℰ.∘′ unit′.η′ _) ℰ.∘′ g′) ≡⟨ ℰ.unwhisker-l _ _ ⟩
+ ℰ.hom[] (R.₁′ f′ ℰ.∘′ unit′.η′ _) ℰ.∘′ g′ ∎
+
+ L-adjunct-naturalr′
+ : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} {z′ : ℱ.Ob[ z ]}
+ → {f : Hom y z} {g : Hom x y}
+ → (f′ : ℱ.Hom[ f ] y′ z′) (g′ : ℱ.Hom[ g ] (L.₀′ x′) y′)
+ → L-adjunct′ (f′ ℱ.∘′ g′) ≡ R.₁′ f′ ℰ.∘′ L-adjunct′ g′
+ L-adjunct-naturalr′ {f = f} f′ g′ =
+ ℰ.hom[] (R.₁′ (f′ ℱ.∘′ g′) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (ap (f ∘_) (idr _)) (ℰ.pushl[] _ R.F-∘′) ⟩
+ ℰ.hom[] (R.₁′ f′ ℰ.∘′ R.₁′ g′ ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.unwhisker-r _ _ ⟩
+ R.₁′ f′ ℰ.∘′ ℰ.hom[] (R.₁′ g′ ℰ.∘′ unit′.η′ _) ∎
+
+ R-adjunct-naturall′
+ : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℰ.Ob[ y ]} {z′ : ℱ.Ob[ z ]}
+ → {f : Hom y z} {g : Hom x y}
+ → (f′ : ℰ.Hom[ f ] y′ (R.₀′ z′)) (g′ : ℰ.Hom[ g ] x′ y′)
+ → R-adjunct′ (f′ ℰ.∘′ g′) ≡ R-adjunct′ f′ ℱ.∘′ L.₁′ g′
+ R-adjunct-naturall′ {g = g} f′ g′ =
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (f′ ℰ.∘′ g′)) ≡⟨ ℱ.weave _ _ (ap (_∘ g) (idl _)) (ℱ.pushr[] _ L.F-∘′) ⟩
+ ℱ.hom[] ((counit′.ε′ _ ℱ.∘′ L.₁′ f′) ℱ.∘′ L.F₁′ g′) ≡⟨ ℱ.unwhisker-l _ _ ⟩
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ f′) ℱ.∘′ L.₁′ g′ ∎
+
+ R-adjunct-naturalr′
+ : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} {z′ : ℱ.Ob[ z ]}
+ → {f : Hom y z} {g : Hom x y}
+ → (f′ : ℱ.Hom[ f ] y′ z′) (g′ : ℰ.Hom[ g ] x′ (R.₀′ y′))
+ → R-adjunct′ (R.₁′ f′ ℰ.∘′ g′) ≡ f′ ℱ.∘′ R-adjunct′ g′
+ R-adjunct-naturalr′ {f = f} f′ g′ =
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′ ℰ.∘′ g′)) ≡⟨ ℱ.weave _ _ (idl _) (ap₂ ℱ._∘′_ refl L.F-∘′) ⟩
+ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ g′) ≡⟨ ℱ.weave _ _ (ap (f ∘_) (idl _)) (ℱ.extendl[] _ (counit′.is-natural′ _ _ _)) ⟩
+ ℱ.hom[] (f′ ℱ.∘′ counit′.ε′ _ ℱ.∘′ L.₁′ g′) ≡⟨ ℱ.unwhisker-r _ _ ⟩
+ f′ ℱ.∘′ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ g′) ∎
```
+
+## Vertical Right Adjoints are Fibred
+
+If $L \dashv R$ is a vertical adjunction, then $R$ is a fibred functor.
+
+```agda
+ Vert-right-adjoint-fibred
+ : {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ}
+ → L ⊣↓ R
+ → is-vertical-fibred R
+ Vert-right-adjoint-fibred {L = L} {R = R} adj {f = f} f′ cart = R-cart where
+ open is-cartesian
+ module L = Cat.Displayed.Functor.Vertical.Reasoning L
+ module R = Cat.Displayed.Functor.Vertical.Reasoning R
+```
+
+Let $f : \cC(x,y)$ and $f' : \cF(x', y')_{f}$ be a cartesian morphism.
+To show that $R$ is fibred, we need to show that $R(f')$ is cartesian.
+Let $m : \cC(a, x)$, and $h' : \cE(a', y')_{f \circ m}$; we need to
+construct a universal factorization of $h'$ through $R(f')$.
+
+As $f'$ is cartesian, we can perform the following factorization of
+the left adjunct $\varepsilon \circ L(h')$ of $h$, yielding a map
+$\hat{h} : \cF(a', x')$.
+
+~~~{.quiver}
+\begin{tikzcd}
+ {a'} \\
+ & {x'} && {y'} \\
+ a \\
+ & y && x
+ \arrow["{f'}", from=2-2, to=2-4]
+ \arrow["f", from=4-2, to=4-4]
+ \arrow[lies over, from=2-2, to=4-2]
+ \arrow[lies over, from=2-4, to=4-4]
+ \arrow["m", from=3-1, to=4-2]
+ \arrow["{\varepsilon \circ L(h')}", curve={height=-12pt}, from=1-1, to=2-4]
+ \arrow[lies over, from=1-1, to=3-1]
+ \arrow["{f \circ m}", curve={height=-12pt}, from=3-1, to=4-4]
+ \arrow["{\exists! \hat{h}}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=2-2]
+\end{tikzcd}
+~~~
+
+We can then take the right adjunct $R(\hat{h}) \circ \eta$ of $\hat{h}$
+to obtain the desired factorization.
+
+
+```agda
+ R-cart : is-cartesian ℰ f (R.F₁′ f′)
+ R-cart .universal m h′ =
+ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′))
+```
+
+
+Showing that this factorization is universal is a matter of
+pushing around the adjuncts.
+
+
+```agda
+ R-cart .commutes m h′ =
+ R.F₁′ f′ ℰ.∘′ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′)) ≡˘⟨ L-adjunct-naturalr′ adj _ _ ⟩
+ L-adjunct′ adj (f′ ℱ.∘′ cart .universal m (R-adjunct′ adj h′)) ≡⟨ ap (L-adjunct′ adj) (cart .commutes _ _) ⟩
+ L-adjunct′ adj (R-adjunct′ adj h′) ≡⟨ L-R-adjunct′ adj h′ ⟩
+ h′ ∎
+ R-cart .unique {m = m} {h′ = h′} m′ p =
+ m′ ≡˘⟨ L-R-adjunct′ adj m′ ⟩
+ L-adjunct′ adj (R-adjunct′ adj m′) ≡⟨ ap (L-adjunct′ adj) (cart .unique _ (sym $ R-adjunct-naturalr′ adj _ _)) ⟩
+ L-adjunct′ adj (cart .universal m (R-adjunct′ adj ⌜ R .F₁′ f′ ℰ.∘′ m′ ⌝)) ≡⟨ ap! p ⟩
+ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′)) ∎
+```
+
+
+Dually, vertical left adjoints are opfibred.
+
+```agda
+ Vert-left-adjoint-opfibred
+ : {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ}
+ → L ⊣↓ R
+ → is-vertical-opfibred L
+```
+
+
+The proof is entirely dual to the one for right adjoints.
+
+```agda
+ Vert-left-adjoint-opfibred {L = L} {R = R} adj {f = f} f′ cocart = L-cocart where
+ open is-cocartesian
+ module L = Cat.Displayed.Functor.Vertical.Reasoning L
+ module R = Cat.Displayed.Functor.Vertical.Reasoning R
+
+ L-cocart : is-cocartesian ℱ f (L.F₁′ f′)
+ L-cocart .universal m h′ =
+ R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′))
+ L-cocart .commutes m h′ =
+ R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′)) ℱ.∘′ L.F₁′ f′ ≡˘⟨ R-adjunct-naturall′ adj _ _ ⟩
+ R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′) ℰ.∘′ f′) ≡⟨ ap (R-adjunct′ adj) (cocart .commutes _ _) ⟩
+ R-adjunct′ adj (L-adjunct′ adj h′) ≡⟨ R-L-adjunct′ adj h′ ⟩
+ h′ ∎
+ L-cocart .unique {m = m} {h′ = h′} m′ p =
+ m′ ≡˘⟨ R-L-adjunct′ adj m′ ⟩
+ R-adjunct′ adj (L-adjunct′ adj m′) ≡⟨ ap (R-adjunct′ adj) (cocart .unique _ (sym $ L-adjunct-naturall′ adj _ _)) ⟩
+ R-adjunct′ adj (cocart .universal m (L-adjunct′ adj ⌜ m′ ℱ.∘′ L .F₁′ f′ ⌝)) ≡⟨ ap! p ⟩
+ R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′)) ∎
+```
+
+
+
+## Adjunctions between Fibre Categories
+
+Vertical adjunctions yield adjunctions between fibre categories.
+
+```agda
+ vertical-adjunction→fibre-adjunction
+ : ∀ {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ}
+ → L ⊣↓ R
+ → ∀ x → Restrict↓ L x ⊣ Restrict↓ R x
+ vertical-adjunction→fibre-adjunction {L = L} {R = R} vadj x = adj where
+ open _⊣↓_ vadj
+ open _⊣_
+ open _=>_
+ open _=>↓_
+
+ adj : Restrict↓ L x ⊣ Restrict↓ R x
+ adj .unit .η x = unit′ .η′ x
+ adj .unit .is-natural x′ y′ f′ =
+ Vert-nat-restrict {F′ = IdV} {G′ = R V∘ L} unit′ x .is-natural x′ y′ f′
+ adj .counit .η x = counit′ .η′ x
+ adj .counit .is-natural x′ y′ f′ =
+ Vert-nat-restrict {F′ = L V∘ R} {G′ = IdV} counit′ x .is-natural x′ y′ f′
+ adj .zig = from-pathp zig′
+ adj .zag = from-pathp zag′
+```
+
diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md
index 870ea8050..65d764694 100644
--- a/src/Cat/Displayed/Cartesian.lagda.md
+++ b/src/Cat/Displayed/Cartesian.lagda.md
@@ -3,7 +3,7 @@
open import Cat.Displayed.Base
open import Cat.Prelude
-import Cat.Displayed.Reasoning as DR
+import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Reasoning
```
@@ -13,11 +13,15 @@ import Cat.Reasoning
module Cat.Displayed.Cartesian
{o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) where
+```
+
+
# Cartesian morphisms and Fibrations
diff --git a/src/Cat/Displayed/Cartesian/Identity.lagda.md b/src/Cat/Displayed/Cartesian/Identity.lagda.md
index 985ede495..03bdc12b0 100644
--- a/src/Cat/Displayed/Cartesian/Identity.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Identity.lagda.md
@@ -33,7 +33,6 @@ private
open Cat.Displayed.Univalence.Reasoning E
open Cat.Displayed.Univalence E
open Cat.Displayed.Morphism E
-open Displayed E
open Dr E
open _≅[_]_
```
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
index 999b645ba..e4d4a989f 100644
--- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -30,7 +30,6 @@ open Cartesian-fibration cartesian
open Cat.Displayed.Reasoning E
open Cat.Reasoning B
open Cartesian-lift
-open Displayed E
open is-cartesian
open Functor
```
diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md
index 2a7fee03f..2ed392ccd 100644
--- a/src/Cat/Displayed/Cartesian/Right.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Right.lagda.md
@@ -24,7 +24,6 @@ module Cat.Displayed.Cartesian.Right
where
open Cat.Reasoning ℬ
-open Displayed ℰ
open Cat.Displayed.Cartesian ℰ
open Cat.Displayed.Morphism ℰ
open Cat.Displayed.Reasoning ℰ
diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md
index 22c413897..40dfd649a 100644
--- a/src/Cat/Displayed/Cartesian/Weak.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md
@@ -31,7 +31,6 @@ module Cat.Displayed.Cartesian.Weak
+
+```agda
+ Restrict↓ : Vertical-functor ℰ ℱ → ∀ x → Functor (Fibre ℰ x) (Fibre ℱ x)
+ Restrict↓ F' _ .Functor.F₀ = F' .F₀′
+ Restrict↓ F' _ .Functor.F₁ = F' .F₁′
+ Restrict↓ F' _ .Functor.F-id = F' .F-id′
+```
+
+As per usual, transports get in our way. This `comp`{.Agda} really is
+the best way to handle this.
+
+```agda
+ Restrict↓ F' _ .Functor.F-∘ {x} {y} {z} f g i =
+ comp (λ j → ℱ.Hom[ idl id j ] (F' .F₀′ x) (F' .F₀′ z)) (∂ i) λ where
+ j (i = i0) →
+ F' .F₁′ (transp (λ i → ℰ.Hom[ idl id (i ∧ j) ] x z) (~ j) (f ℰ.∘′ g))
+ j (i = i1) →
+ transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F' .F₀′ x) (F' .F₀′ z)) (~ j)
+ (F' .F₁′ f ℱ.∘′ F' .F₁′ g)
+ j (j = i0) → F' .F-∘′ {f′ = f} {g′ = g} i
+
+ Restrict↓f : Vertical-fibred-functor ℰ ℱ → ∀ x → Functor (Fibre ℰ x) (Fibre ℱ x)
+ Restrict↓f F' = Restrict↓ (Vertical-fibred-functor.vert F')
+```
+
+
## Displayed Natural Transformations
Just like we have defined a [displayed functor][disfct]
@@ -632,3 +717,38 @@ to be preserved.
F′ =>f↓ G′ = F′ .vert =>↓ G′ .vert
where open Vertical-fibred-functor
```
+
+Vertical natural transformations restrict to natural transformations
+between restrictions of vertical functors (what a mouthful!).
+
+
+
+```agda
+ Vert-nat-restrict
+ : ∀ {F′ G′ : Vertical-functor ℰ ℱ}
+ → F′ =>↓ G′ → ∀ x → Restrict↓ F′ x => Restrict↓ G′ x
+ Vert-nat-restrict α′ x .η x′ = α′ .η′ x′
+ Vert-nat-restrict {F′ = F′} {G′ = G′} α′ x .is-natural x′ y′ f′ i =
+ comp (λ j → ℱ.Hom[ hom-filler i j ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (∂ i) λ where
+ j (i = i0) →
+ transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (~ j)
+ (α′ .η′ y′ ℱ.∘′ F′ .F₁′ f′)
+ j (i = i1) →
+ transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (~ j)
+ (G′ .F₁′ f′ ℱ.∘′ α′ .η′ x′)
+ j (j = i0) → α′ .is-natural′ x′ y′ f′ i
+ where
+ hom-filler : I → I → Hom x x
+ hom-filler i j =
+ is-set→squarep (λ i j → Hom-set x x) (idl id) id-comm-sym refl (idl id) j i
+
+ Vert-fib-nat-restrict
+ : ∀ {F′ G′ : Vertical-fibred-functor ℰ ℱ}
+ → F′ =>f↓ G′ → ∀ x → Restrict↓f F′ x => Restrict↓f G′ x
+ Vert-fib-nat-restrict α′ x = Vert-nat-restrict α′ x
+```
diff --git a/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md
new file mode 100644
index 000000000..6ccafead2
--- /dev/null
+++ b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md
@@ -0,0 +1,63 @@
+
+
+```agda
+module Cat.Displayed.Functor.Vertical.Reasoning
+ {ob ℓb oe ℓe of ℓf}
+ {B : Precategory ob ℓb}
+ {ℰ : Displayed B oe ℓe} {ℱ : Displayed B of ℓf}
+ (F : Vertical-functor ℰ ℱ)
+ where
+```
+
+# Reasoning Combinators for Vertical Functors
+
+This module provides versions of the [functor reasoning combinators][func]
+that have been adapted to work with vertical functors.
+
+[func]: Cat.Functor.Reasoning.html
+
+
+
+```agda
+F-∘[]
+ : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {h : Hom x z}
+ → {p : f ∘ g ≡ h}
+ → (f′ : ℰ.Hom[ f ] y′ z′) (g′ : ℰ.Hom[ g ] x′ y′)
+ → F₁′ (ℰ.hom[ p ] (f′ ℰ.∘′ g′)) ≡ ℱ.hom[ p ] (F₁′ f′ ℱ.∘′ F₁′ g′)
+F-∘[] {x′ = x′} {z′ = z′} {p = p} f′ g′ i =
+ comp (λ j → ℱ.Hom[ p j ] (F₀′ x′) (F₀′ z′)) (∂ i) λ where
+ j (i = i0) →
+ F₁′ (transp (λ i → ℰ.Hom[ p (i ∧ j) ] x′ z′) (~ j) (f′ ℰ.∘′ g′))
+ j (i = i1) →
+ transp (λ i → ℱ.Hom[ p (i ∧ j) ] (F₀′ x′) (F₀′ z′)) (~ j)
+ (F₁′ f′ ℱ.∘′ F₁′ g′)
+ j (j = i0) → F-∘′ {f′ = f′} {g′ = g′} i
+```
+
+```agda
+collapse′
+ : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {h : Hom x z}
+ → {f′ : ℰ.Hom[ f ] y′ z′} {g′ : ℰ.Hom[ g ] x′ y′} {h′ : ℰ.Hom[ h ] x′ z′}
+ → {p : f ∘ g ≡ h}
+ → f′ ℰ.∘′ g′ ℰ.≡[ p ] h′
+ → F₁′ f′ ℱ.∘′ F₁′ g′ ℱ.≡[ p ] F₁′ h′
+collapse′ q = ℱ.cast[] (symP F-∘′ ℱ.∙[] (λ i → F₁′ (q i)))
+```
diff --git a/src/Cat/Displayed/Instances/Diagrams.lagda.md b/src/Cat/Displayed/Instances/Diagrams.lagda.md
index d9bbebbfb..984dd8799 100644
--- a/src/Cat/Displayed/Instances/Diagrams.lagda.md
+++ b/src/Cat/Displayed/Instances/Diagrams.lagda.md
@@ -24,7 +24,6 @@ module Cat.Displayed.Instances.Diagrams
where
open Cat.Reasoning B
-open Displayed E
open Cat.Displayed.Reasoning E
open Functor
open _=>_
@@ -53,21 +52,39 @@ liftings along a constant functor $\Delta_{x} : \cJ \to \cB$, we get a
diagram in $\cE$ that lies entirely in the fibre $\cE_{x}$: a fibrewise
diagram!
-This allows us to concisely define the fibration of fibrewise diagrams
-as the base change of $\cE \to \cB$ along the functor $\cB \to [\cJ,
-\cB]$ that takes an object to the constant diagram on that object.
+We could concisely define the fibration of fibrewise diagrams as the
+base change of $\cE \to \cB$ along the functor $\cB \to [\cJ, \cB]$ that
+takes an object to the constant diagram on that object, but this runs
+into some annoying issues with transports. Therefore, we unfold the
+definition instead.
[fibration of liftings]: Cat.Displayed.Instances.Lifting.html
+
+
```agda
Diagrams
: ∀ {oj ℓj} (J : Precategory oj ℓj)
→ Displayed B _ _
-Diagrams J = Change-of-base ConstD (Liftings E J)
+Diagrams J .Ob[_] b = Lifting {J = J} E (Const b)
+Diagrams J .Hom[_] u F G = F =[ const-nt u ]=>l G
+Diagrams J .Hom[_]-set _ _ _ = Nat-lift-is-set
+Diagrams J .id′ .η′ _ = id′
+Diagrams J .id′ .is-natural′ _ _ _ =
+ cast[] $ idl′ _ ∙[] symP (idr′ _)
+Diagrams J ._∘′_ α β .η′ j = α .η′ j ∘′ β .η′ j
+Diagrams J ._∘′_ α β .is-natural′ x y f =
+ cast[] $ pullr[] _ (β .is-natural′ x y f) ∙[] extendl[] _ (α .is-natural′ x y f)
+Diagrams J .idr′ α = Nat-lift-pathp λ _ → idr′ _
+Diagrams J .idl′ α = Nat-lift-pathp λ _ → idl′ _
+Diagrams J .assoc′ α β γ = Nat-lift-pathp λ _ → assoc′ _ _ _
```
-When $\cE$ is a fibration, then so is the fibration of diagrams.
-
+## As a fibration
+
+We begin by characterizing the cartesian maps in the diagram fibration.
+Like the fibration of liftings, these are the pointwise cartesian maps.
+This proof is identical to `pointwise-cartesian→Liftings-cartesian`{.Agda},
+but we are off by some definitional equalities, so we have to unfold
+some things.
+
+```agda
+ pointwise-cartesian→Diagram-cartesian
+ : ∀ {x y : Ob} {F : Lifting E (Const x)} {G : Lifting E (Const y)}
+ → {u : Hom x y} {α : F =[ const-nt u ]=>l G}
+ → (∀ j → is-cartesian E u (α .η′ j))
+ → is-cartesian (Diagrams J) u α
+ pointwise-cartesian→Diagram-cartesian {u = u} {α = α} pointwise = cart where
+ module pointwise x = is-cartesian (pointwise x)
+
+ cart : is-cartesian (Diagrams J) u α
+ cart .is-cartesian.universal m β .η′ x =
+ pointwise.universal x m (β .η′ x)
+ cart .is-cartesian.universal m β .is-natural′ x y f =
+ pointwise.uniquep₂ _ _ _ _ _ _
+ (pulll[] _ (pointwise.commutes _ _ _) ∙[] β .is-natural′ _ _ _)
+ (pulll[] _ (α .is-natural′ x y f)
+ ∙[] pullr[] _ (pointwise.commutes _ _ _))
+ cart .is-cartesian.commutes m β =
+ Nat-lift-pathp (λ _ → pointwise.commutes _ _ _)
+ cart .is-cartesian.unique β' p =
+ Nat-lift-pathp (λ x → pointwise.unique _ _ λ i → p i .η′ x)
+```
+
+We can use the previous fact to show that the fibration of diagrams is
+actually a fibration. Luckily, we get to re-use a lot of the proof
+that the fibration of liftings is a fibration.
+
```agda
Diagram-fibration : Cartesian-fibration E → Cartesian-fibration (Diagrams J)
- Diagram-fibration fib =
- Change-of-base-fibration ConstD (Liftings E _)
- (Liftings-fibration E _ fib)
+ Diagram-fibration fib .Cartesian-fibration.has-lift f F = cart-lift where
+ module fib = Cartesian-fibration.has-lift fib
+ open Cartesian-fibration (Liftings-fibration E J fib)
+
+ cart-lift : Cartesian-lift _ f F
+ cart-lift .Cartesian-lift.x′ = has-lift.x′ (const-nt f) F
+ cart-lift .Cartesian-lift.lifting = has-lift.lifting (const-nt f) F
+ cart-lift .Cartesian-lift.cartesian =
+ pointwise-cartesian→Diagram-cartesian (λ _ → fib.cartesian _ _)
```
## The constant fibrewise diagram functor
@@ -116,9 +174,26 @@ of shape $\cJ$, which takes an $x'$ to the constant diagram.
ConstFibD .Vertical-functor.F₀′ = ConstL
ConstFibD .Vertical-functor.F₁′ = const-ntl
ConstFibD .Vertical-functor.F-id′ =
- Nat-lift-pathp (λ x → sym (transport-refl _))
+ Nat-lift-pathp (λ x → refl)
ConstFibD .Vertical-functor.F-∘′ =
- Nat-lift-pathp (λ x → sym (transport-refl _))
+ Nat-lift-pathp (λ x → refl)
+```
+
+Furthermore, this functor is fibred.
+
+```agda
+ ConstFibD-fibred : is-vertical-fibred ConstFibD
+ ConstFibD-fibred f′ cart =
+ pointwise-cartesian→Diagram-cartesian (λ _ → cart)
+```
+
+We will use the fibred version of this functor quite a bit, so we give
+it a nice short name.
+
+```agda
+ Δd : Vertical-fibred-functor E (Diagrams J)
+ Δd .Vertical-fibred-functor.vert = ConstFibD
+ Δd .Vertical-fibred-functor.F-cartesian = ConstFibD-fibred
```
Next, we note that liftings of the constant functor correspond with
@@ -186,8 +261,8 @@ functor categories $[\cJ, \cE_x]$.
Fibrewise-diagram : ∀ {x} → Functor Cat[ J , Fibre E x ] (Fibre (Diagrams J) x)
Fibrewise-diagram .F₀ = Diagram→ConstL
Fibrewise-diagram .F₁ = Diagram-nat→ConstL-natl
- Fibrewise-diagram .F-id = Nat-lift-pathp λ _ → sym Regularity.reduce!
- Fibrewise-diagram .F-∘ _ _ = Nat-lift-pathp λ _ → sym Regularity.reduce!
+ Fibrewise-diagram .F-id = Nat-lift-pathp λ _ → refl
+ Fibrewise-diagram .F-∘ _ _ = Nat-lift-pathp λ _ → sym (Regularity.reduce!)
```
Again, this isomorphism is *almost* definitional.
diff --git a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md
index 0f675e7b7..88302ff54 100644
--- a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md
+++ b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md
@@ -25,7 +25,6 @@ module Cat.Displayed.Instances.DisplayedFamilies
@@ -164,7 +163,6 @@ module _
private module J = Precategory J
open Cat.Reasoning B
- open Displayed E
open Cat.Displayed.Reasoning E
open Lifting
```
@@ -308,7 +306,6 @@ module _
private module J = Precategory J
open Cat.Reasoning B
- open Displayed E
open Cat.Displayed.Reasoning E
open Lifting
open _=[_]=>l_
diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md
index 10d937baa..4d75ea691 100644
--- a/src/Cat/Displayed/InternalSum.lagda.md
+++ b/src/Cat/Displayed/InternalSum.lagda.md
@@ -43,5 +43,5 @@ record Internal-sum : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
no-eta-equality
field
∐ : Vertical-fibred-functor (Disp-family E) E
- adjunction : ∐ ⊣↓ ConstDispFamVf E
+ adjunction : ∐ ⊣f↓ ConstDispFamVf E
```
diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md
index 97cc15086..2b5273052 100644
--- a/src/Cat/Displayed/Morphism.lagda.md
+++ b/src/Cat/Displayed/Morphism.lagda.md
@@ -18,7 +18,6 @@ module Cat.Displayed.Morphism
@@ -45,10 +43,10 @@ shorthand syntax for that here. You can think of this as being an
abbreviation for `subst`{.Agda} because... that's what it is.
```agda
-hom[_] : ∀ {a b x y} {f g : B.Hom a b} → f ≡ g → E.Hom[ f ] x y → E.Hom[ g ] x y
-hom[ p ] f′ = subst (λ h → E.Hom[ h ] _ _) p f′
+hom[_] : ∀ {a b x y} {f g : Hom a b} → f ≡ g → Hom[ f ] x y → Hom[ g ] x y
+hom[ p ] f′ = subst (λ h → Hom[ h ] _ _) p f′
-hom[_]⁻ : ∀ {a b x y} {f g : B.Hom a b} → g ≡ f → E.Hom[ f ] x y → E.Hom[ g ] x y
+hom[_]⁻ : ∀ {a b x y} {f g : Hom a b} → g ≡ f → Hom[ f ] x y → Hom[ g ] x y
hom[ p ]⁻ f′ = hom[ sym p ] f′
```
@@ -57,17 +55,17 @@ adjust the path we're transporting over to get something more convenient.
```agda
reindex
- : ∀ {a b x y} {f g : B.Hom a b} (p q : f ≡ g) {f′ : E.Hom[ f ] x y}
+ : ∀ {a b x y} {f g : Hom a b} (p q : f ≡ g) {f′ : Hom[ f ] x y}
→ hom[ p ] f′ ≡ hom[ q ] f′
-reindex p q {f′} = ap (λ e → hom[ e ] f′) (B.Hom-set _ _ _ _ p q)
+reindex p q {f′} = ap (λ e → hom[ e ] f′) (Hom-set _ _ _ _ p q)
cast[]
- : ∀ {a b x y} {f g : B.Hom a b} {f′ : E.Hom[ f ] x y} {g′ : E.Hom[ g ] x y}
+ : ∀ {a b x y} {f g : Hom a b} {f′ : Hom[ f ] x y} {g′ : Hom[ g ] x y}
→ {p q : f ≡ g}
- → f′ E.≡[ p ] g′
- → f′ E.≡[ q ] g′
+ → f′ ≡[ p ] g′
+ → f′ ≡[ q ] g′
cast[] {f = f} {g = g} {f′ = f′} {g′ = g′} {p = p} {q = q} r =
- coe0→1 (λ i → f′ E.≡[ B.Hom-set _ _ f g p q i ] g′) r
+ coe0→1 (λ i → f′ ≡[ Hom-set _ _ f g p q i ] g′) r
```
@@ -79,14 +77,14 @@ composite unchanged.
```agda
hom[]-∙
- : ∀ {a b x y} {f g h : B.Hom a b} (p : f ≡ g) (q : g ≡ h)
- {f′ : E.Hom[ f ] x y}
+ : ∀ {a b x y} {f g h : Hom a b} (p : f ≡ g) (q : g ≡ h)
+ {f′ : Hom[ f ] x y}
→ hom[ q ] (hom[ p ] f′) ≡ hom[ p ∙ q ] f′
-hom[]-∙ p q = sym (subst-∙ (λ h → E.Hom[ h ] _ _) _ _ _)
+hom[]-∙ p q = sym (subst-∙ (λ h → Hom[ h ] _ _) _ _ _)
duplicate
- : ∀ {a b x y} {f f' g : B.Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f')
- {f′ : E.Hom[ f ] x y}
+ : ∀ {a b x y} {f f' g : Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f')
+ {f′ : Hom[ f ] x y}
→ hom[ p ] f′ ≡ hom[ q ] (hom[ r ] f′)
duplicate p q r = reindex _ _ ∙ sym (hom[]-∙ r q)
```
@@ -105,42 +103,42 @@ we can't just get rid of the transport $p^*(-)$.
```agda
whisker-r
- : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
→ (p : g ≡ g')
- → f′ E.∘′ hom[ p ] g′ ≡ hom[ ap (f B.∘_) p ] (f′ E.∘′ g′)
+ → f′ ∘′ hom[ p ] g′ ≡ hom[ ap (f ∘_) p ] (f′ ∘′ g′)
whisker-r {f = f} {a′ = a′} {_} {c′} {f′} {g′} p i =
- comp (λ j → E.Hom[ f B.∘ p (i ∨ j) ] a′ c′) (∂ i) λ where
- j (i = i0) → f′ E.∘′ transport-filler (λ i → E.Hom[ p i ] _ _) g′ j
- j (i = i1) → hom[ ap (f B.∘_) p ] (f′ E.∘′ g′)
- j (j = i0) → transport-filler (λ i → E.Hom[ f B.∘ p i ] _ _) (f′ E.∘′ g′) i
+ comp (λ j → Hom[ f ∘ p (i ∨ j) ] a′ c′) (∂ i) λ where
+ j (i = i0) → f′ ∘′ transport-filler (λ i → Hom[ p i ] _ _) g′ j
+ j (i = i1) → hom[ ap (f ∘_) p ] (f′ ∘′ g′)
+ j (j = i0) → transport-filler (λ i → Hom[ f ∘ p i ] _ _) (f′ ∘′ g′) i
whisker-l
- : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
→ (p : f ≡ f')
- → hom[ p ] f′ E.∘′ g′ ≡ hom[ ap (B._∘ g) p ] (f′ E.∘′ g′)
+ → hom[ p ] f′ ∘′ g′ ≡ hom[ ap (_∘ g) p ] (f′ ∘′ g′)
whisker-l {g = g} {a′} {_} {c′} {f′ = f′} {g′ = g′} p i =
- comp (λ j → E.Hom[ p (i ∨ j) B.∘ g ] a′ c′) (∂ i) λ where
- j (i = i0) → transport-filler (λ i → E.Hom[ p i ] _ _) f′ j E.∘′ g′
- j (i = i1) → hom[ ap (B._∘ g) p ] (f′ E.∘′ g′)
- j (j = i0) → transport-filler (λ i → E.Hom[ p i B.∘ g ] _ _) (f′ E.∘′ g′) i
+ comp (λ j → Hom[ p (i ∨ j) ∘ g ] a′ c′) (∂ i) λ where
+ j (i = i0) → transport-filler (λ i → Hom[ p i ] _ _) f′ j ∘′ g′
+ j (i = i1) → hom[ ap (_∘ g) p ] (f′ ∘′ g′)
+ j (j = i0) → transport-filler (λ i → Hom[ p i ∘ g ] _ _) (f′ ∘′ g′) i
```
@@ -150,67 +148,67 @@ lemmas above:
```agda
smashr
- : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
- → (p : g ≡ g') (q : f B.∘ g' ≡ h)
- → hom[ q ] (f′ E.∘′ hom[ p ] g′) ≡ hom[ ap (f B.∘_) p ∙ q ] (f′ E.∘′ g′)
+ : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {h : Hom a c} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
+ → (p : g ≡ g') (q : f ∘ g' ≡ h)
+ → hom[ q ] (f′ ∘′ hom[ p ] g′) ≡ hom[ ap (f ∘_) p ∙ q ] (f′ ∘′ g′)
smashr p q = ap hom[ q ] (whisker-r p) ∙ hom[]-∙ _ _
smashl
- : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
- → (p : f ≡ f') (q : f' B.∘ g ≡ h)
- → hom[ q ] (hom[ p ] f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) p ∙ q ] (f′ E.∘′ g′)
+ : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {h : Hom a c} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
+ → (p : f ≡ f') (q : f' ∘ g ≡ h)
+ → hom[ q ] (hom[ p ] f′ ∘′ g′) ≡ hom[ ap (_∘ g) p ∙ q ] (f′ ∘′ g′)
smashl p q = ap hom[ q ] (whisker-l p) ∙ hom[]-∙ _ _
expandl
- : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
- → (p : f ≡ f') (q : f B.∘ g ≡ h)
- → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) (sym p) ∙ q ] (hom[ p ] f′ E.∘′ g′)
+ : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {h : Hom a c} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
+ → (p : f ≡ f') (q : f ∘ g ≡ h)
+ → hom[ q ] (f′ ∘′ g′) ≡ hom[ ap (_∘ g) (sym p) ∙ q ] (hom[ p ] f′ ∘′ g′)
expandl p q = reindex q _ ∙ (sym $ smashl _ _)
expandr
- : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
- → (p : g ≡ g') (q : f B.∘ g ≡ h)
- → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (f B.∘_) (sym p) ∙ q ] (f′ E.∘′ hom[ p ] g′)
+ : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {h : Hom a c} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
+ → (p : g ≡ g') (q : f ∘ g ≡ h)
+ → hom[ q ] (f′ ∘′ g′) ≡ hom[ ap (f ∘_) (sym p) ∙ q ] (f′ ∘′ hom[ p ] g′)
expandr p q = reindex q _ ∙ (sym $ smashr _ _)
yank
: ∀ {a b c d}
- {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {i : B.Hom a c} {j : B.Hom b d}
+ {f : Hom c d} {g : Hom b c} {h : Hom a b} {i : Hom a c} {j : Hom b d}
{a′ b′ c′ d′}
- {f′ : E.Hom[ f ] c′ d′} {g′ : E.Hom[ g ] b′ c′} {h′ : E.Hom[ h ] a′ b′}
- (p : g B.∘ h ≡ i) (q : f B.∘ g ≡ j) (r : f B.∘ i ≡ j B.∘ h)
- → (f′ E.∘′ hom[ p ](g′ E.∘′ h′)) E.≡[ r ] hom[ q ] (f′ E.∘′ g′) E.∘′ h′
+ {f′ : Hom[ f ] c′ d′} {g′ : Hom[ g ] b′ c′} {h′ : Hom[ h ] a′ b′}
+ (p : g ∘ h ≡ i) (q : f ∘ g ≡ j) (r : f ∘ i ≡ j ∘ h)
+ → (f′ ∘′ hom[ p ](g′ ∘′ h′)) ≡[ r ] hom[ q ] (f′ ∘′ g′) ∘′ h′
yank {f′ = f′} {g′ = g′} {h′ = h′} p q r = to-pathp $
- hom[ r ] (f′ E.∘′ hom[ p ] (g′ E.∘′ h′)) ≡⟨ smashr p r ⟩
- hom[ ap (B._∘_ _) p ∙ r ] (f′ E.∘′ g′ E.∘′ h′) ≡⟨ ap hom[ _ ] (sym (from-pathp λ i → E.assoc′ f′ g′ h′ (~ i))) ⟩
- hom[ ap (B._∘_ _) p ∙ r ] (hom[ sym (B.assoc _ _ _) ] ((f′ E.∘′ g′) E.∘′ h′)) ≡⟨ hom[]-∙ _ _ ⟩
- hom[ sym (B.assoc _ _ _) ∙ (ap (B .Precategory._∘_ _) p ∙ r)] ((f′ E.∘′ g′) E.∘′ h′) ≡⟨ reindex _ _ ⟩
- hom[ (ap (B._∘ _) q) ] ((f′ E.∘′ g′) E.∘′ h′) ≡˘⟨ whisker-l q ⟩
- hom[ q ] (f′ E.∘′ g′) E.∘′ h′ ∎
+ hom[ r ] (f′ ∘′ hom[ p ] (g′ ∘′ h′)) ≡⟨ smashr p r ⟩
+ hom[ ap (_∘_ _) p ∙ r ] (f′ ∘′ g′ ∘′ h′) ≡⟨ ap hom[ _ ] (sym (from-pathp λ i → assoc′ f′ g′ h′ (~ i))) ⟩
+ hom[ ap (_∘_ _) p ∙ r ] (hom[ sym (assoc _ _ _) ] ((f′ ∘′ g′) ∘′ h′)) ≡⟨ hom[]-∙ _ _ ⟩
+ hom[ sym (assoc _ _ _) ∙ (ap (B .Precategory._∘_ _) p ∙ r)] ((f′ ∘′ g′) ∘′ h′) ≡⟨ reindex _ _ ⟩
+ hom[ (ap (_∘ _) q) ] ((f′ ∘′ g′) ∘′ h′) ≡˘⟨ whisker-l q ⟩
+ hom[ q ] (f′ ∘′ g′) ∘′ h′ ∎
cancel
- : ∀ {a b} {f g : B.Hom a b} (p q : f ≡ g) {a′ b′}
- {f′ : E.Hom[ f ] a′ b′} {g′ : E.Hom[ g ] a′ b′}
- → PathP (λ i → E.Hom[ q i ] a′ b′) f′ g′
+ : ∀ {a b} {f g : Hom a b} (p q : f ≡ g) {a′ b′}
+ {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] a′ b′}
+ → PathP (λ i → Hom[ q i ] a′ b′) f′ g′
→ hom[ p ] f′ ≡ g′
cancel p q r = reindex p q ∙ from-pathp r
kill₁
- : ∀ {a b} {a′ b′} {f g h : B.Hom a b} {h₁′ : E.Hom[ f ] a′ b′} {h₂′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b} {a′ b′} {f g h : Hom a b} {h₁′ : Hom[ f ] a′ b′} {h₂′ : Hom[ g ] a′ b′}
→ (p : f ≡ g) (q : g ≡ h)
- → PathP (λ i → E.Hom[ p i ] a′ b′) h₁′ h₂′
+ → PathP (λ i → Hom[ p i ] a′ b′) h₁′ h₂′
→ hom[ p ∙ q ] h₁′ ≡ hom[ q ] h₂′
kill₁ p q r = sym (hom[]-∙ _ _) ∙ ap hom[ q ] (from-pathp r)
-revive₁ : ∀ {a b} {f g h : B.Hom a b}
- {a′ b′} {f′ : E.Hom[ f ] a′ b′} {g′ : E.Hom[ g ] a′ b′}
+revive₁ : ∀ {a b} {f g h : Hom a b}
+ {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] a′ b′}
→ {p : f ≡ g} {q : f ≡ h}
- → f′ E.≡[ p ] g′
+ → f′ ≡[ p ] g′
→ hom[ q ] f′ ≡ hom[ sym p ∙ q ] g′
revive₁ {f′ = f′} {g′ = g′} {p = p} {q = q} p′ =
hom[ q ] f′ ≡⟨ reindex _ _ ⟩
@@ -221,93 +219,93 @@ revive₁ {f′ = f′} {g′ = g′} {p = p} {q = q} p′ =
-- something. We combine the reindexing to fix the association and
-- killing the first parameter to "weave" here.
weave
- : ∀ {a b} {a′ b′} {f g h : B.Hom a b} {h₁′ : E.Hom[ f ] a′ b′} {h₂′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b} {a′ b′} {f g h : Hom a b} {h₁′ : Hom[ f ] a′ b′} {h₂′ : Hom[ g ] a′ b′}
→ (p : f ≡ h) (p′ : f ≡ g) (q : g ≡ h)
- → PathP (λ i → E.Hom[ p′ i ] a′ b′) h₁′ h₂′
+ → PathP (λ i → Hom[ p′ i ] a′ b′) h₁′ h₂′
→ hom[ p ] h₁′ ≡ hom[ q ] h₂′
weave p p′ q s =
reindex p (p′ ∙ q)
∙ kill₁ p′ q s
split
- : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′}
(p : f ≡ f') (q : g ≡ g')
- → hom[ ap₂ B._∘_ p q ] (f′ E.∘′ g′) ≡ hom[ p ] f′ E.∘′ hom[ q ] g′
+ → hom[ ap₂ _∘_ p q ] (f′ ∘′ g′) ≡ hom[ p ] f′ ∘′ hom[ q ] g′
split p q =
- reindex _ (ap₂ B._∘_ p refl ∙ ap₂ B._∘_ refl q)
+ reindex _ (ap₂ _∘_ p refl ∙ ap₂ _∘_ refl q)
·· sym (hom[]-∙ _ _)
·· ap hom[ _ ] (sym (whisker-l p)) ∙ sym (whisker-r q)
liberate
- : ∀ {a b x y} {f : B.Hom a b} {f′ : E.Hom[ f ] x y}
+ : ∀ {a b x y} {f : Hom a b} {f′ : Hom[ f ] x y}
(p : f ≡ f)
→ hom[ p ] f′ ≡ f′
liberate p = reindex p refl ∙ transport-refl _
hom[]⟩⟨_
- : ∀ {a b} {f f' : B.Hom a b} {a′ b′} {p : f ≡ f'}
- {f′ g′ : E.Hom[ f ] a′ b′}
+ : ∀ {a b} {f f' : Hom a b} {a′ b′} {p : f ≡ f'}
+ {f′ g′ : Hom[ f ] a′ b′}
→ f′ ≡ g′
→ hom[ p ] f′ ≡ hom[ p ] g′
hom[]⟩⟨_ = ap hom[ _ ]
_⟩∘′⟨_
- : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
- {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′}
- {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′}
+ : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′}
+ {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′}
+ {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′}
{p : f ≡ f'} {q : g ≡ g'}
- → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′
- → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′
- → hom[ p ] f₁′ E.∘′ hom[ q ] g₁′ ≡ f₂′ E.∘′ g₂′
-p ⟩∘′⟨ q = ap₂ E._∘′_ (from-pathp p) (from-pathp q)
+ → PathP (λ i → Hom[ p i ] b′ c′) f₁′ f₂′
+ → PathP (λ i → Hom[ q i ] a′ b′) g₁′ g₂′
+ → hom[ p ] f₁′ ∘′ hom[ q ] g₁′ ≡ f₂′ ∘′ g₂′
+p ⟩∘′⟨ q = ap₂ _∘′_ (from-pathp p) (from-pathp q)
_⟩∘′⟨refl
- : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′}
- {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+ : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {a′ b′ c′}
+ {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′} {g′ : Hom[ g ] a′ b′}
{p : f ≡ f'}
- → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′
- → hom[ p ] f₁′ E.∘′ g′ ≡ f₂′ E.∘′ g′
-p ⟩∘′⟨refl = ap₂ E._∘′_ (from-pathp p) refl
+ → PathP (λ i → Hom[ p i ] b′ c′) f₁′ f₂′
+ → hom[ p ] f₁′ ∘′ g′ ≡ f₂′ ∘′ g′
+p ⟩∘′⟨refl = ap₂ _∘′_ (from-pathp p) refl
refl⟩∘′⟨_
- : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
- {f′ : E.Hom[ f ] b′ c′}
- {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′}
+ : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {a′ b′ c′}
+ {f′ : Hom[ f ] b′ c′}
+ {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′}
{q : g ≡ g'}
- → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′
- → f′ E.∘′ hom[ q ] g₁′ ≡ f′ E.∘′ g₂′
-refl⟩∘′⟨ p = ap₂ E._∘′_ refl (from-pathp p)
+ → PathP (λ i → Hom[ q i ] a′ b′) g₁′ g₂′
+ → f′ ∘′ hom[ q ] g₁′ ≡ f′ ∘′ g₂′
+refl⟩∘′⟨ p = ap₂ _∘′_ refl (from-pathp p)
split⟩⟨_
- : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
- {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′}
- {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′}
+ : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′}
+ {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′}
+ {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′}
{p : f ≡ f'} {q : g ≡ g'}
- → hom[ p ] f₁′ E.∘′ hom[ q ] g₁′ ≡ f₂′ E.∘′ g₂′
- → hom[ ap₂ B._∘_ p q ] (f₁′ E.∘′ g₁′) ≡ f₂′ E.∘′ g₂′
+ → hom[ p ] f₁′ ∘′ hom[ q ] g₁′ ≡ f₂′ ∘′ g₂′
+ → hom[ ap₂ _∘_ p q ] (f₁′ ∘′ g₁′) ≡ f₂′ ∘′ g₂′
split⟩⟨ p = split _ _ ∙ p
infixr 5 _⟩∘′⟨_ refl⟩∘′⟨_ _⟩∘′⟨refl
infixl 4 split⟩⟨_ hom[]⟩⟨_
-hom[] : ∀ {a b x y} {f g : B.Hom a b} {p : f ≡ g} → E.Hom[ f ] x y → E.Hom[ g ] x y
+hom[] : ∀ {a b x y} {f g : Hom a b} {p : f ≡ g} → Hom[ f ] x y → Hom[ g ] x y
hom[] {p = p} f′ = hom[ p ] f′
pulll-indexr
- : ∀ {a b c d} {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {ac : B.Hom a c}
- {a′ : E.Ob[ a ]} {b′ : E.Ob[ b ]} {c′ : E.Ob[ c ]} {d′ : E.Ob[ d ]}
- {f′ : E.Hom[ f ] c′ d′}
- {g′ : E.Hom[ g ] b′ c′}
- {h′ : E.Hom[ h ] a′ b′}
- {fg′ : E.Hom[ f B.∘ g ] b′ d′}
- → (p : g B.∘ h ≡ ac)
- → (f′ E.∘′ g′ ≡ fg′)
- → f′ E.∘′ hom[ p ] (g′ E.∘′ h′) ≡ hom[ B.pullr p ] (fg′ E.∘′ h′)
+ : ∀ {a b c d} {f : Hom c d} {g : Hom b c} {h : Hom a b} {ac : Hom a c}
+ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {c′ : Ob[ c ]} {d′ : Ob[ d ]}
+ {f′ : Hom[ f ] c′ d′}
+ {g′ : Hom[ g ] b′ c′}
+ {h′ : Hom[ h ] a′ b′}
+ {fg′ : Hom[ f ∘ g ] b′ d′}
+ → (p : g ∘ h ≡ ac)
+ → (f′ ∘′ g′ ≡ fg′)
+ → f′ ∘′ hom[ p ] (g′ ∘′ h′) ≡ hom[ pullr p ] (fg′ ∘′ h′)
pulll-indexr p q = whisker-r _ ∙
- sym ( reindex _ (sym (B.assoc _ _ _) ∙ ap (_ B.∘_) p) ·· sym (hom[]-∙ _ _)
- ·· ap hom[] ( ap hom[] (ap (E._∘′ _) (sym q))
- ∙ from-pathp (symP (E.assoc′ _ _ _))))
+ sym ( reindex _ (sym (assoc _ _ _) ∙ ap (_ ∘_) p) ·· sym (hom[]-∙ _ _)
+ ·· ap hom[] ( ap hom[] (ap (_∘′ _) (sym q))
+ ∙ from-pathp (symP (assoc′ _ _ _))))
```
Using these tools, we can define displayed versions of the usual category
@@ -315,9 +313,6 @@ reasoning combinators.
diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md
index 6a40d160e..44b3d3708 100644
--- a/src/Cat/Functor/Hom/Displayed.lagda.md
+++ b/src/Cat/Functor/Hom/Displayed.lagda.md
@@ -20,7 +20,6 @@ module Cat.Functor.Hom.Displayed