diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md
index 8bdd4f235..c5e68ebf4 100644
--- a/src/Cat/Displayed/Cartesian.lagda.md
+++ b/src/Cat/Displayed/Cartesian.lagda.md
@@ -117,38 +117,39 @@ composite, rather than displayed directly over a composite.
universal' {u' = u'} p h' =
universal _ (coe1→0 (λ i → Hom[ p i ] u' b') h')
- commutesp : ∀ {u u'} {m : Hom u a} {k : Hom u b}
- → (p : f ∘ m ≡ k) (h' : Hom[ k ] u' b')
- → f' ∘' universal' p h' ≡[ p ] h'
- commutesp {u' = u'} p h' =
- to-pathp⁻ $ commutes _ (coe1→0 (λ i → Hom[ p i ] u' b') h')
-
- universalp : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
- → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
- → (h' : Hom[ k ] u' b')
- → universal' p h' ≡[ q ] universal' r h'
- universalp {u = u} p q r h' i =
- universal' (is-set→squarep (λ _ _ → Hom-set u b) (ap (f ∘_) q) p r refl i) h'
-
- uniquep : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
- → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
- → {h' : Hom[ k ] u' b'}
- → (m' : Hom[ m₁ ] u' a')
- → f' ∘' m' ≡[ p ] h' → m' ≡[ q ] universal' r h'
- uniquep p q r {h' = h'} m' s =
- to-pathp⁻ (unique m' (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h'))
-
- uniquep₂
- : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
- → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
- → {h' : Hom[ k ] u' b'} (m₁' : Hom[ m₁ ] u' a') (m₂' : Hom[ m₂ ] u' a')
- → f' ∘' m₁' ≡[ p ] h'
- → f' ∘' m₂' ≡[ r ] h'
- → m₁' ≡[ q ] m₂'
- uniquep₂ {u' = u'} p q r m₁' m₂' α β = to-pathp⁻ $
- unique m₁' (from-pathp⁻ α)
- ∙∙ from-pathp⁻ (universalp p q r _)
- ∙∙ ap (coe1→0 (λ i → Hom[ q i ] u' a')) (sym (unique m₂' (from-pathp⁻ β)))
+ abstract
+ commutesp : ∀ {u u'} {m : Hom u a} {k : Hom u b}
+ → (p : f ∘ m ≡ k) (h' : Hom[ k ] u' b')
+ → f' ∘' universal' p h' ≡[ p ] h'
+ commutesp {u' = u'} p h' =
+ to-pathp⁻ $ commutes _ (coe1→0 (λ i → Hom[ p i ] u' b') h')
+
+ universalp : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
+ → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
+ → (h' : Hom[ k ] u' b')
+ → universal' p h' ≡[ q ] universal' r h'
+ universalp {u = u} p q r h' i =
+ universal' (is-set→squarep (λ _ _ → Hom-set u b) (ap (f ∘_) q) p r refl i) h'
+
+ uniquep : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
+ → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
+ → {h' : Hom[ k ] u' b'}
+ → (m' : Hom[ m₁ ] u' a')
+ → f' ∘' m' ≡[ p ] h' → m' ≡[ q ] universal' r h'
+ uniquep p q r {h' = h'} m' s =
+ to-pathp⁻ (unique m' (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h'))
+
+ uniquep₂
+ : ∀ {u u'} {m₁ m₂ : Hom u a} {k : Hom u b}
+ → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k)
+ → {h' : Hom[ k ] u' b'} (m₁' : Hom[ m₁ ] u' a') (m₂' : Hom[ m₂ ] u' a')
+ → f' ∘' m₁' ≡[ p ] h'
+ → f' ∘' m₂' ≡[ r ] h'
+ → m₁' ≡[ q ] m₂'
+ uniquep₂ {u' = u'} p q r m₁' m₂' α β = to-pathp⁻ $
+ unique m₁' (from-pathp⁻ α)
+ ∙∙ from-pathp⁻ (universalp p q r _)
+ ∙∙ ap (coe1→0 (λ i → Hom[ q i ] u' a')) (sym (unique m₂' (from-pathp⁻ β)))
```
Furthermore, if $f'' : a'' \to_{f} b'$ is also displayed over $f$,
@@ -217,6 +218,36 @@ is-cartesian-is-prop {f' = f'} cart cart' = worker where
```
+
+
We also provide a bundled form of cartesian morphisms.
```agda
@@ -272,15 +303,15 @@ cartesian-∘ {f = f} {g = g} {f' = f'} {g' = g'} f-cart g-cart = fg-cart where
fg-cart .is-cartesian.universal m h' =
g'.universal m (f'.universal' (assoc f g m) h')
fg-cart .is-cartesian.commutes m h' =
- (f' ∘' g') ∘' g'.universal m (f'.universal' (assoc f g m) h') ≡⟨ shiftr (sym $ assoc _ _ _) (pullr' refl (g'.commutes m _)) ⟩
- hom[] (f' ∘' f'.universal' (assoc f g m) h') ≡⟨ hom[]⟩⟨ f'.commutes _ _ ⟩
- hom[] (hom[] h') ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩
- h' ∎
+ cast[] $
+ (f' ∘' g') ∘' g'.universal m (f'.universal' _ h') ≡[]⟨ pullr[] _ (g'.commutes _ _) ⟩
+ f' ∘' f'.universal' _ h' ≡[]⟨ f'.commutesp (assoc f g m) h' ⟩
+ h' ∎
fg-cart .is-cartesian.unique {m = m} {h' = h'} m' p =
- g'.unique m' $ f'.unique (g' ∘' m') $
- f' ∘' g' ∘' m' ≡⟨ from-pathp⁻ (assoc' f' g' m') ⟩
- hom[] ((f' ∘' g') ∘' m') ≡⟨ weave _ _ _ p ⟩
- hom[] h' ∎
+ g'.unique m' $ f'.uniquep _ _ _ (g' ∘' m') $
+ f' ∘' g' ∘' m' ≡[]⟨ assoc' f' g' m' ⟩
+ (f' ∘' g') ∘' m' ≡[]⟨ p ⟩
+ h' ∎
_∘cart_
: ∀ {x y z x' y' z'} {f : Hom y z} {g : Hom x y}
@@ -321,22 +352,22 @@ invertible→cartesian
→ is-cartesian f f'
invertible→cartesian
{f = f} {f' = f'} f-inv f'-inv = f-cart where
- module f-inv = is-invertible f-inv
- module f'-inv = is-invertible[_] f'-inv
+ module f = is-invertible f-inv
+ module f' = is-invertible[_] f'-inv
f-cart : is-cartesian f f'
f-cart .is-cartesian.universal m h' =
- hom[ cancell f-inv.invr ] (f'-inv.inv' ∘' h')
+ hom[ cancell f.invr ] (f'.inv' ∘' h')
f-cart .is-cartesian.commutes m h' =
- f' ∘' hom[ cancell f-inv.invr ] (f'-inv.inv' ∘' h') ≡⟨ whisker-r _ ⟩
- hom[] (f' ∘' f'-inv.inv' ∘' h') ≡⟨ revive₁ (cancell' f-inv.invl f'-inv.invl' {q = cancell f-inv.invl}) ⟩
- hom[] h' ≡⟨ liberate _ ⟩
- h' ∎
+ cast[] $
+ f' ∘' hom[] (f'.inv' ∘' h') ≡[]⟨ unwrapr _ ⟩
+ f' ∘' f'.inv' ∘' h' ≡[]⟨ cancell[] _ f'.invl' ⟩
+ h' ∎
f-cart .is-cartesian.unique {h' = h'} m' p =
- m' ≡˘⟨ liberate _ ⟩
- hom[] m' ≡⟨ weave refl (insertl f-inv.invr) (cancell f-inv.invr) (insertl' _ f'-inv.invr') ⟩
- hom[] (f'-inv.inv' ∘' f' ∘' m') ≡⟨ apr' p ⟩
- hom[] (f'-inv.inv' ∘' h') ∎
+ cast[] $
+ m' ≡[]⟨ introl[] f.invr f'.invr' ∙[] pullr[] _ p ⟩
+ f'.inv' ∘' h' ≡[]⟨ wrap (cancell f.invr) ⟩
+ hom[] (f'.inv' ∘' h') ∎
```
+```agda
+module Cat.Displayed.Cartesian.Joint
+ {o ℓ o' ℓ'}
+ {B : Precategory o ℓ} (E : Displayed B o' ℓ')
+ where
+```
+
+
+
+# Jointly cartesian families
+
+:::{.definition #jointly-cartesian-family}
+A family of morphisms $f_{i} : \cE_{u_i}(A', B'_{i})$ over $u_{i} : \cB(A, B_{i})$
+is **jointly cartesian** if it satisfies a familial version of the universal
+property of a [[cartesian|cartesian-morphism]] map.
+:::
+
+```agda
+record is-jointly-cartesian
+ {ℓi} {Ix : Type ℓi}
+ {a : Ob} {bᵢ : Ix → Ob}
+ {a' : Ob[ a ]} {bᵢ' : (ix : Ix) → Ob[ bᵢ ix ]}
+ (uᵢ : (ix : Ix) → Hom a (bᵢ ix))
+ (fᵢ : (ix : Ix) → Hom[ uᵢ ix ] a' (bᵢ' ix))
+ : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ' ⊔ ℓi) where
+```
+
+Explicitly, a family $f_{i}$ is jointly cartesian if for every map
+$v : \cB(X, A)$ and family of morphisms $h_{i} : \cE_{u_i \circ v}(X', B_{i}')$,
+there exists a unique universal map $\langle v , h_{i} \rangle : \cE_{v}(X', A')$
+such that $f_{i} \circ \langle v , h_{i} \rangle = h_{i}$.
+
+~~~{.quiver}
+\begin{tikzcd}
+ {X'} \\
+ && {A'} && {B_i'} \\
+ X \\
+ && A && {B_i}
+ \arrow["{\exists!}"{description}, dashed, from=1-1, to=2-3]
+ \arrow["{h_i}"{description}, curve={height=-12pt}, from=1-1, to=2-5]
+ \arrow[from=1-1, to=3-1]
+ \arrow["{f_i}"{description}, from=2-3, to=2-5]
+ \arrow[from=2-3, to=4-3]
+ \arrow[from=2-5, to=4-5]
+ \arrow["v"{description}, from=3-1, to=4-3]
+ \arrow["{u_i \circ v}"{description, pos=0.7}, curve={height=-12pt}, from=3-1, to=4-5]
+ \arrow["{u_i}"{description}, from=4-3, to=4-5]
+\end{tikzcd}
+~~~
+
+```agda
+ no-eta-equality
+ field
+ universal
+ : ∀ {x x'}
+ → (v : Hom x a)
+ → (∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix))
+ → Hom[ v ] x' a'
+ commutes
+ : ∀ {x x'}
+ → (v : Hom x a)
+ → (hᵢ : ∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix))
+ → ∀ ix → fᵢ ix ∘' universal v hᵢ ≡ hᵢ ix
+ unique
+ : ∀ {x x'}
+ → {v : Hom x a}
+ → {hᵢ : ∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix)}
+ → (other : Hom[ v ] x' a')
+ → (∀ ix → fᵢ ix ∘' other ≡ hᵢ ix)
+ → other ≡ universal v hᵢ
+```
+
+
+
+
+
+::: warning
+Some sources ([@Adamek-Herrlich-Strecker:2004], [@Dubuc-Espanol:2006])
+refer to jointly cartesian families as "initial families". We opt to
+avoid this terminology, as it leads to unnecessary conflicts with
+[[initial objects]].
+:::
+
+At first glance, jointly cartesian families appear very similar to cartesian maps.
+However, replacing a single map with a family of maps has some very strong
+consequences: cartesian morphisms typically behave as witnesses to [[base change]]
+operations, whereas jointly cartesian families act more like a combination
+of base-change maps and projections out of a product. This can be seen
+by studying prototypical examples of jointly cartesian families:
+
+- If we view the category of topological spaces as a [[displayed category]],
+then the jointly cartesian maps are precisely the initial topologies.
+
+- Jointly cartesian maps in the [[subobject fibration]] of $\Sets$
+arise from pulling back a family of subsets $A_{i} \subset Y_{i}$ along
+maps $u_{i} : X \to Y_{i}$, and then taking their intersection.
+
+- When $\cB$ is considered as a displayed category over the [[terminal category]],
+the jointly cartesian families are precisely the [[indexed products]].
+In contrast, the cartesian maps are the invertible maps.
+
+## Relating cartesian maps and jointly cartesian families
+
+Every [[cartesian map]] can be regarded as a jointly cartesian family
+over a contractible type.
+
+```agda
+cartesian→jointly-cartesian
+ : is-contr Ix
+ → is-cartesian u f
+ → is-jointly-cartesian {Ix = Ix} (λ _ → u) (λ _ → f)
+cartesian→jointly-cartesian {u = u} {f = f} ix-contr f-cart = f-joint-cart where
+ module f = is-cartesian f-cart
+ open is-jointly-cartesian
+
+ f-joint-cart : is-jointly-cartesian (λ _ → u) (λ _ → f)
+ f-joint-cart .universal v hᵢ =
+ f.universal v (hᵢ (ix-contr .centre))
+ f-joint-cart .commutes v hᵢ ix =
+ f ∘' f.universal v (hᵢ (ix-contr .centre)) ≡⟨ f.commutes v (hᵢ (ix-contr .centre)) ⟩
+ hᵢ (ix-contr .centre) ≡⟨ ap hᵢ (ix-contr .paths ix) ⟩
+ hᵢ ix ∎
+ f-joint-cart .unique other p =
+ f.unique other (p (ix-contr .centre))
+```
+
+Conversely, if the constant family $\lambda i.\; f$ is a jointly cartesian
+$I$-indexed family over a merely inhabited type $I$, then $f$ is cartesian.
+
+```agda
+const-jointly-cartesian→cartesian
+ : ∥ Ix ∥
+ → is-jointly-cartesian {Ix = Ix} (λ _ → u) (λ _ → f)
+ → is-cartesian u f
+const-jointly-cartesian→cartesian {Ix = Ix} {u = u} {f = f} ∥ix∥ f-joint-cart =
+ rec! f-cart ∥ix∥
+ where
+ module f = is-jointly-cartesian f-joint-cart
+ open is-cartesian
+
+ f-cart : Ix → is-cartesian u f
+ f-cart ix .universal v h = f.universal v λ _ → h
+ f-cart ix .commutes v h = f.commutes v (λ _ → h) ix
+ f-cart ix .unique other p = f.unique other (λ _ → p)
+```
+
+Jointly cartesian families over empty types act more like codiscrete objects
+than pullbacks, as the space of maps into the shared domain of the family
+is unique for any $v : \cE{B}(X, A)$ and $X' \liesover X$. In the displayed
+category of topological spaces, such maps are precisely the codiscrete spaces.
+
+```agda
+empty-jointly-cartesian→codiscrete
+ : ∀ {uᵢ : (ix : Ix) → Hom a (bᵢ ix)} {fᵢ : (ix : Ix) → Hom[ uᵢ ix ] a' (bᵢ' ix)}
+ → ¬ Ix
+ → is-jointly-cartesian uᵢ fᵢ
+ → ∀ {x} (v : Hom x a) → (x' : Ob[ x ]) → is-contr (Hom[ v ] x' a')
+empty-jointly-cartesian→codiscrete ¬ix fᵢ-cart v x' =
+ contr (fᵢ.universal v λ ix → absurd (¬ix ix)) λ other →
+ sym (fᵢ.unique other λ ix → absurd (¬ix ix))
+ where
+ module fᵢ = is-jointly-cartesian fᵢ-cart
+```
+
+In the other direction, let $f : \cE_{u}(A', B')$ be some map.
+If the constant family $\lambda b.\; f : 2 \to \cE_{u}(A', B')$
+is jointly cartesian as a family over the booleans,
+then the type of morphisms $\cE_{u \circ v}(X', A')$ is a [[proposition]]
+for every $v : \cB(X, A)$ and $X' \liesover X$.
+
+```agda
+const-pair-joint-cartesian→thin
+ : ∀ {u : Hom a b} {f : Hom[ u ] a' b'}
+ → is-jointly-cartesian {Ix = Bool} (λ _ → u) (λ _ → f)
+ → ∀ {x} (v : Hom x a) → (x' : Ob[ x ]) → is-prop (Hom[ u ∘ v ] x' b')
+```
+
+Let $g, h : \cE_{u \circ v}(X', A')$ be a pair of parallel maps in $\cE$.
+We can view the the pair $(g, h)$ as a `Bool`{.Agda} indexed family of
+maps over $u \circ v$, so by the universal property of jointly cartesian
+families, there must be a universal map $\alpha$ such that $g = f \circ \alpha$
+and $h = f \circ \alpha$; thus $f = g$.
+
+
+```agda
+const-pair-joint-cartesian→thin {b' = b'} {u = u} {f = f} f-cart v x' g h =
+ cast[] $
+ g ≡[]˘⟨ commutes v gh true ⟩
+ f ∘' universal v gh ≡[]⟨ commutes v gh false ⟩
+ h ∎
+ where
+ open is-jointly-cartesian f-cart
+
+ gh : Bool → Hom[ u ∘ v ] x' b'
+ gh true = g
+ gh false = h
+```
+
+As a corollary, if $(id_{A'}, id_{A'})$ is a jointly cartesian family, then
+every hom set $\cE_{u}(X',A')$ is a proposition.
+
+```agda
+id-pair-joint-cartesian→thin
+ : is-jointly-cartesian {Ix = Bool} (λ _ → id {a}) (λ _ → id' {a} {a'})
+ → ∀ {x} (u : Hom x a) → (x' : Ob[ x ]) → is-prop (Hom[ u ] x' a')
+id-pair-joint-cartesian→thin id²-cart u x' f g =
+ cast[] $
+ f ≡[]⟨ wrap (sym (idl u)) ⟩
+ hom[] f ≡[]⟨ const-pair-joint-cartesian→thin id²-cart u x' (hom[ idl u ]⁻ f) (hom[ idl u ]⁻ g) ⟩
+ hom[] g ≡[]⟨ unwrap (sym (idl u)) ⟩
+ g ∎
+```
+
+## Closure properties of jointly cartesian families
+
+If $g_{i} : X' \to_{v_i} Y_{i}'$ is an $I$-indexed jointly cartesian family, and
+$f_{i,j} : Y_{i}' \to_{u_{i,j}} Z_{i,j}'$ is an $I$-indexed family of $J_{i}$-indexed
+jointly cartesian families, then their composite is a $\Sigma (i : I).\; J_i$-indexed
+jointly cartesian family.
+
+```agda
+jointly-cartesian-∘
+ : {uᵢⱼ : (i : Ix) → (j : Jx i) → Hom (bᵢ i) (cᵢⱼ i j)}
+ → {fᵢⱼ : (i : Ix) → (j : Jx i) → Hom[ uᵢⱼ i j ] (bᵢ' i) (cᵢⱼ' i j)}
+ → {vᵢ : (i : Ix) → Hom a (bᵢ i)}
+ → {gᵢ : (i : Ix) → Hom[ vᵢ i ] a' (bᵢ' i)}
+ → (∀ i → is-jointly-cartesian (uᵢⱼ i) (fᵢⱼ i))
+ → is-jointly-cartesian vᵢ gᵢ
+ → is-jointly-cartesian
+ (λ ij → uᵢⱼ (ij .fst) (ij .snd) ∘ vᵢ (ij .fst))
+ (λ ij → fᵢⱼ (ij .fst) (ij .snd) ∘' gᵢ (ij .fst))
+```
+
+
+
+Despite the high quantifier complexity of the statement, the proof
+follows the exact same plan that we use to show that `cartesian maps compose`{.Agda ident=cartesian-∘}.
+
+```agda
+jointly-cartesian-∘ {Ix = Ix} {uᵢⱼ = uᵢⱼ} {fᵢⱼ = fᵢⱼ} {vᵢ = vᵢ} {gᵢ = gᵢ} fᵢⱼ-cart gᵢ-cart =
+ fᵢⱼ∘gᵢ-cart
+ where
+ module fᵢⱼ (i : Ix) = is-jointly-cartesian (fᵢⱼ-cart i)
+ module gᵢ = is-jointly-cartesian gᵢ-cart
+ open is-jointly-cartesian
+
+ fᵢⱼ∘gᵢ-cart
+ : is-jointly-cartesian
+ (λ ij → uᵢⱼ (ij .fst) (ij .snd) ∘ vᵢ (ij .fst))
+ (λ ij → fᵢⱼ (ij .fst) (ij .snd) ∘' gᵢ (ij .fst))
+ fᵢⱼ∘gᵢ-cart .universal v hᵢⱼ =
+ gᵢ.universal v λ i →
+ fᵢⱼ.universal' i (λ j → assoc (uᵢⱼ i j) (vᵢ i) v) λ j →
+ hᵢⱼ (i , j)
+ fᵢⱼ∘gᵢ-cart .commutes w hᵢⱼ (i , j) =
+ cast[] $
+ (fᵢⱼ i j ∘' gᵢ i) ∘' gᵢ.universal _ (λ i → fᵢⱼ.universal' i _ (λ j → hᵢⱼ (i , j))) ≡[]⟨ pullr[] _ (gᵢ.commutes w _ i) ⟩
+ fᵢⱼ i j ∘' fᵢⱼ.universal' i _ (λ j → hᵢⱼ (i , j)) ≡[]⟨ fᵢⱼ.commutesp i _ _ j ⟩
+ hᵢⱼ (i , j) ∎
+ fᵢⱼ∘gᵢ-cart .unique {hᵢ = hᵢⱼ} other p =
+ gᵢ.unique other $ λ i →
+ fᵢⱼ.uniquep i _ _ _ (gᵢ i ∘' other) λ j →
+ fᵢⱼ i j ∘' gᵢ i ∘' other ≡[]⟨ assoc' (fᵢⱼ i j) (gᵢ i) other ⟩
+ (fᵢⱼ i j ∘' gᵢ i) ∘' other ≡[]⟨ p (i , j) ⟩
+ hᵢⱼ (i , j) ∎
+```
+
+As a nice corollary, we get that jointly cartesian families compose with
+[[cartesian maps]], as cartesian maps are precisely the singleton jointly cartesian
+families.
+
+```agda
+jointly-cartesian-cartesian-∘
+ : is-jointly-cartesian uᵢ fᵢ
+ → is-cartesian v g
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g)
+```
+
+
+We actually opt to prove this corollary by hand to get nicer
+definitional behaviour of the resulting universal maps.
+
+
+```agda
+jointly-cartesian-cartesian-∘ {uᵢ = uᵢ} {fᵢ = fᵢ} {v = v} {g = g} fᵢ-cart g-cart = fᵢ∘g-cart
+ where
+ module fᵢ = is-jointly-cartesian fᵢ-cart
+ module g = is-cartesian g-cart
+ open is-jointly-cartesian
+
+ fᵢ∘g-cart : is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g)
+ fᵢ∘g-cart .universal w hᵢ =
+ g.universal w $ fᵢ.universal' (λ ix → assoc (uᵢ ix) v w) hᵢ
+ fᵢ∘g-cart .commutes w hᵢ ix =
+ cast[] $
+ (fᵢ ix ∘' g) ∘' universal fᵢ∘g-cart w hᵢ ≡[]⟨ pullr[] _ (g.commutes w _) ⟩
+ fᵢ ix ∘' fᵢ.universal' (λ ix → assoc (uᵢ ix) v w) hᵢ ≡[]⟨ fᵢ.commutesp _ hᵢ ix ⟩
+ hᵢ ix ∎
+ fᵢ∘g-cart .unique other pᵢ =
+ g.unique other $
+ fᵢ.uniquep _ _ _ (g ∘' other) λ ix →
+ assoc' (fᵢ ix) g other ∙[] pᵢ ix
+```
+
+
+Similarly, if $f_{i}$ is a family of maps with each $f_{i}$ individually
+cartesian, and $g_{i}$ is jointly cartesian, then the composite $f_{i} \circ g_{i}$
+is jointly cartesian.
+
+```agda
+pointwise-cartesian-jointly-cartesian-∘
+ : (∀ ix → is-cartesian (uᵢ ix) (fᵢ ix))
+ → is-jointly-cartesian vᵢ gᵢ
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ vᵢ ix) (λ ix → fᵢ ix ∘' gᵢ ix)
+```
+
+
+We again prove this by hand to get better definitional behaviour.
+
+```agda
+pointwise-cartesian-jointly-cartesian-∘
+ {uᵢ = uᵢ} {fᵢ = fᵢ} {vᵢ = vᵢ} {gᵢ = gᵢ} fᵢ-cart gᵢ-cart = fᵢ∘gᵢ-cart where
+ module fᵢ ix = is-cartesian (fᵢ-cart ix)
+ module gᵢ = is-jointly-cartesian gᵢ-cart
+ open is-jointly-cartesian
+
+ fᵢ∘gᵢ-cart : is-jointly-cartesian (λ ix → uᵢ ix ∘ vᵢ ix) (λ ix → fᵢ ix ∘' gᵢ ix)
+ fᵢ∘gᵢ-cart .universal v hᵢ =
+ gᵢ.universal v λ ix → fᵢ.universal' ix (assoc (uᵢ ix) (vᵢ ix) v) (hᵢ ix)
+ fᵢ∘gᵢ-cart .commutes v hᵢ ix =
+ cast[] $
+ (fᵢ ix ∘' gᵢ ix) ∘' gᵢ.universal v (λ ix → fᵢ.universal' ix _ (hᵢ ix)) ≡[]⟨ pullr[] refl (gᵢ.commutes v _ ix) ⟩
+ fᵢ ix ∘' fᵢ.universal' ix _ (hᵢ ix) ≡[]⟨ fᵢ.commutesp ix (assoc (uᵢ ix) (vᵢ ix) v) (hᵢ ix) ⟩
+ hᵢ ix ∎
+ fᵢ∘gᵢ-cart .unique other p =
+ gᵢ.unique other λ ix →
+ fᵢ.uniquep ix _ _ _ (gᵢ ix ∘' other)
+ (assoc' (fᵢ ix) (gᵢ ix) other ∙[] p ix)
+```
+
+
+Like their non-familial counterparts, jointly cartesian maps are stable
+under vertical retractions.
+
+```agda
+jointly-cartesian-vertical-retraction-stable
+ : ∀ {fᵢ : ∀ (ix : Ix) → Hom[ uᵢ ix ] a' (cᵢ' ix)}
+ → {fᵢ' : ∀ (ix : Ix) → Hom[ uᵢ ix ] b' (cᵢ' ix)}
+ → {ϕ : Hom[ id ] a' b'}
+ → is-jointly-cartesian uᵢ fᵢ
+ → has-section↓ ϕ
+ → (∀ ix → fᵢ' ix ∘' ϕ ≡[ idr _ ] fᵢ ix)
+ → is-jointly-cartesian uᵢ fᵢ'
+```
+
+
+
+
+The proof is essentially the same as the `non-joint case`{.Agda ident=cartesian-vertical-retraction-stable},
+so we omit the details.
+
+```agda
+jointly-cartesian-vertical-retraction-stable
+ {uᵢ = uᵢ} {fᵢ = fᵢ} {fᵢ' = fᵢ'} {ϕ = ϕ} fᵢ-cart ϕ-sect factor
+ = fᵢ'-cart
+ where
+ module fᵢ = is-jointly-cartesian fᵢ-cart
+ module ϕ = has-section[_] ϕ-sect
+
+ fᵢ'-cart : is-jointly-cartesian uᵢ fᵢ'
+ fᵢ'-cart .is-jointly-cartesian.universal v hᵢ =
+ hom[ idl v ] (ϕ ∘' fᵢ.universal v hᵢ)
+ fᵢ'-cart .is-jointly-cartesian.commutes v hᵢ ix =
+ cast[] $
+ fᵢ' ix ∘' hom[] (ϕ ∘' fᵢ.universal v hᵢ) ≡[]⟨ unwrapr (idl v) ⟩
+ fᵢ' ix ∘' ϕ ∘' fᵢ.universal v hᵢ ≡[]⟨ pulll[] (idr (uᵢ ix)) (factor ix) ⟩
+ fᵢ ix ∘' fᵢ.universal v hᵢ ≡[]⟨ fᵢ.commutes v hᵢ ix ⟩
+ hᵢ ix ∎
+ fᵢ'-cart .is-jointly-cartesian.unique {v = v} {hᵢ = hᵢ} other p =
+ cast[] $
+ other ≡[]⟨ introl[] _ ϕ.is-section' ⟩
+ (ϕ ∘' ϕ.section') ∘' other ≡[]⟨ pullr[] _ (wrap (idl v) ∙[] fᵢ.unique _ unique-lemma) ⟩
+ ϕ ∘' fᵢ.universal v hᵢ ≡[]⟨ wrap (idl v) ⟩
+ hom[ idl v ] (ϕ ∘' fᵢ.universal v hᵢ) ∎
+
+ where
+ unique-lemma : ∀ ix → fᵢ ix ∘' hom[ idl v ] (ϕ.section' ∘' other) ≡ hᵢ ix
+ unique-lemma ix =
+ cast[] $
+ fᵢ ix ∘' hom[ idl v ] (ϕ.section' ∘' other) ≡[]⟨ unwrapr (idl v) ⟩
+ fᵢ ix ∘' ϕ.section' ∘' other ≡[]⟨ pulll[] _ (symP (pre-section[] ϕ-sect (factor ix))) ⟩
+ fᵢ' ix ∘' other ≡[]⟨ p ix ⟩
+ hᵢ ix ∎
+```
+
+
+## Cancellation properties of jointly cartesian families
+
+Every jointly cartesian family is a [[jointly weak monic family]];
+this follows immediately from the uniqueness portion of the
+universal property.
+
+```agda
+jointly-cartesian→jointly-weak-monic
+ : is-jointly-cartesian uᵢ fᵢ
+ → is-jointly-weak-monic fᵢ
+jointly-cartesian→jointly-weak-monic {fᵢ = fᵢ} fᵢ-cart {g = w} g h p p' =
+ fᵢ.uniquep₂ (λ _ → ap₂ _∘_ refl p) p (λ _ → refl) g h p' (λ _ → refl)
+ where module fᵢ = is-jointly-cartesian fᵢ-cart
+```
+
+If $f_{i,j}$ is an $I$-indexed family of $J_{i}$-indexed
+[[jointly weak monic families]] and $f_{i,j} \circ g_{i}$ is a
+$\Sigma (i : I).\; J_{i}$-indexed jointly cartesian family, then
+$g_{i}$ must be a $I$-indexed jointly cartesian family.
+
+```agda
+jointly-cartesian-weak-monic-cancell
+ : {uᵢⱼ : (i : Ix) → (j : Jx i) → Hom (bᵢ i) (cᵢⱼ i j)}
+ → {fᵢⱼ : (i : Ix) → (j : Jx i) → Hom[ uᵢⱼ i j ] (bᵢ' i) (cᵢⱼ' i j)}
+ → {vᵢ : (i : Ix) → Hom a (bᵢ i)}
+ → {gᵢ : (i : Ix) → Hom[ vᵢ i ] a' (bᵢ' i)}
+ → (∀ i → is-jointly-weak-monic (fᵢⱼ i))
+ → is-jointly-cartesian
+ (λ ij → uᵢⱼ (ij .fst) (ij .snd) ∘ vᵢ (ij .fst))
+ (λ ij → fᵢⱼ (ij .fst) (ij .snd) ∘' gᵢ (ij .fst))
+ → is-jointly-cartesian vᵢ gᵢ
+```
+
+Like the general composition lemma for jointly cartesian families,
+the statement is more complicated than the proof, which follows from
+some short calculations.
+
+```agda
+jointly-cartesian-weak-monic-cancell
+ {uᵢⱼ = uᵢⱼ} {fᵢⱼ} {vᵢ} {gᵢ} fᵢⱼ-weak-mono fᵢⱼ∘gᵢ-cart
+ = gᵢ-cart
+ where
+ module fᵢⱼ∘gᵢ = is-jointly-cartesian fᵢⱼ∘gᵢ-cart
+ open is-jointly-cartesian
+
+ gᵢ-cart : is-jointly-cartesian vᵢ gᵢ
+ gᵢ-cart .universal w hᵢ =
+ fᵢⱼ∘gᵢ.universal' (λ (i , j) → sym (assoc (uᵢⱼ i j) (vᵢ i) w)) λ (i , j) →
+ fᵢⱼ i j ∘' hᵢ i
+ gᵢ-cart .commutes w hᵢ i =
+ fᵢⱼ-weak-mono i _ _ refl $ λ j →
+ cast[] $
+ fᵢⱼ i j ∘' gᵢ i ∘' fᵢⱼ∘gᵢ.universal' _ (λ (i , j) → fᵢⱼ i j ∘' hᵢ i) ≡[]⟨ assoc' _ _ _ ⟩
+ (fᵢⱼ i j ∘' gᵢ i) ∘' fᵢⱼ∘gᵢ.universal' _ (λ (i , j) → fᵢⱼ i j ∘' hᵢ i) ≡[]⟨ fᵢⱼ∘gᵢ.commutesp _ _ (i , j) ⟩
+ fᵢⱼ i j ∘' hᵢ i ∎
+ gᵢ-cart .unique other p =
+ fᵢⱼ∘gᵢ.uniquep _ _ _ other λ (i , j) →
+ pullr[] _ (p i)
+```
+
+As an immediate corollary, we get a left cancellation property
+for composites of joint cartesian families.
+
+```agda
+jointly-cartesian-cancell
+ : {uᵢⱼ : (i : Ix) → (j : Jx i) → Hom (bᵢ i) (cᵢⱼ i j)}
+ → {fᵢⱼ : (i : Ix) → (j : Jx i) → Hom[ uᵢⱼ i j ] (bᵢ' i) (cᵢⱼ' i j)}
+ → {vᵢ : (i : Ix) → Hom a (bᵢ i)}
+ → {gᵢ : (i : Ix) → Hom[ vᵢ i ] a' (bᵢ' i)}
+ → (∀ i → is-jointly-cartesian (uᵢⱼ i) (fᵢⱼ i))
+ → is-jointly-cartesian
+ (λ ij → uᵢⱼ (ij .fst) (ij .snd) ∘ vᵢ (ij .fst))
+ (λ ij → fᵢⱼ (ij .fst) (ij .snd) ∘' gᵢ (ij .fst))
+ → is-jointly-cartesian vᵢ gᵢ
+jointly-cartesian-cancell fᵢⱼ-cart fᵢⱼ∘gᵢ-cart =
+ jointly-cartesian-weak-monic-cancell
+ (λ i → jointly-cartesian→jointly-weak-monic (fᵢⱼ-cart i))
+ fᵢⱼ∘gᵢ-cart
+```
+
+We also obtain a further set of corollaries that describe some special
+cases of the general cancellation property.
+
+```agda
+jointly-cartesian-pointwise-weak-monic-cancell
+ : (∀ ix → is-weak-monic (fᵢ ix))
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ vᵢ ix) (λ ix → fᵢ ix ∘' gᵢ ix)
+ → is-jointly-cartesian vᵢ gᵢ
+
+jointly-cartesian-jointly-weak-monic-cancell
+ : is-jointly-weak-monic fᵢ
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g)
+ → is-cartesian v g
+
+jointly-cartesian-pointwise-cartesian-cancell
+ : (∀ ix → is-cartesian (uᵢ ix) (fᵢ ix))
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ vᵢ ix) (λ ix → fᵢ ix ∘' gᵢ ix)
+ → is-jointly-cartesian vᵢ gᵢ
+
+jointly-cartesian-cartesian-cancell
+ : is-jointly-cartesian uᵢ fᵢ
+ → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g)
+ → is-cartesian v g
+```
+
+
+As before, we opt to prove these results by hand to get nicer
+definitional behaviour.
+
+
+```agda
+jointly-cartesian-pointwise-weak-monic-cancell
+ {uᵢ = uᵢ} {fᵢ = fᵢ} {vᵢ = vᵢ} {gᵢ = gᵢ} fᵢ-weak-monic fᵢ∘gᵢ-cart
+ = gᵢ-cart
+ where
+ module fᵢ∘gᵢ = is-jointly-cartesian fᵢ∘gᵢ-cart
+ open is-jointly-cartesian
+
+ gᵢ-cart : is-jointly-cartesian vᵢ gᵢ
+ gᵢ-cart .universal w hᵢ =
+ fᵢ∘gᵢ.universal' (λ ix → sym (assoc (uᵢ ix) (vᵢ ix) w))
+ (λ ix → fᵢ ix ∘' hᵢ ix)
+ gᵢ-cart .commutes w hᵢ ix =
+ fᵢ-weak-monic ix _ _ refl $
+ cast[] $
+ fᵢ ix ∘' gᵢ ix ∘' fᵢ∘gᵢ.universal' _ (λ ix → fᵢ ix ∘' hᵢ ix) ≡[]⟨ assoc' _ _ _ ⟩
+ (fᵢ ix ∘' gᵢ ix) ∘' fᵢ∘gᵢ.universal' _ (λ ix → fᵢ ix ∘' hᵢ ix) ≡[]⟨ fᵢ∘gᵢ.commutesp _ _ ix ⟩
+ fᵢ ix ∘' hᵢ ix ∎
+ gᵢ-cart .unique other p =
+ fᵢ∘gᵢ.uniquep _ _ _ other (λ ix → pullr[] _ (p ix))
+
+jointly-cartesian-jointly-weak-monic-cancell
+ {uᵢ = uᵢ} {fᵢ = fᵢ} {v = v} {g = g} fᵢ-weak-monic fᵢ∘g-cart
+ = g-cart
+ where
+ module fᵢ∘g = is-jointly-cartesian fᵢ∘g-cart
+ open is-cartesian
+
+ g-cart : is-cartesian v g
+ g-cart .universal w h =
+ fᵢ∘g.universal' (λ ix → sym (assoc (uᵢ ix) v w)) (λ ix → fᵢ ix ∘' h)
+ g-cart .commutes w h =
+ fᵢ-weak-monic _ _ refl λ ix →
+ cast[] $
+ fᵢ ix ∘' g ∘' fᵢ∘g.universal' _ (λ ix → fᵢ ix ∘' h) ≡[]⟨ assoc' _ _ _ ⟩
+ (fᵢ ix ∘' g) ∘' fᵢ∘g.universal' _ (λ ix → fᵢ ix ∘' h) ≡[]⟨ fᵢ∘g.commutesp _ _ ix ⟩
+ fᵢ ix ∘' h ∎
+ g-cart .unique other p =
+ fᵢ∘g.uniquep _ _ _ other (λ ix → pullr[] _ p)
+
+jointly-cartesian-pointwise-cartesian-cancell fᵢ-cart fᵢ∘gᵢ-cart =
+ jointly-cartesian-pointwise-weak-monic-cancell
+ (λ ix → cartesian→weak-monic (fᵢ-cart ix))
+ fᵢ∘gᵢ-cart
+
+jointly-cartesian-cartesian-cancell fᵢ-cart fᵢ∘g-cart =
+ jointly-cartesian-jointly-weak-monic-cancell
+ (jointly-cartesian→jointly-weak-monic fᵢ-cart)
+ fᵢ∘g-cart
+
+```
+
+
+## Extending jointly cartesian families
+
+This section characterises when we can extend an $I'$-indexed jointly
+cartesian family $f_{i}$ to a $I$-indexed cartesian family along a map
+$e : I' \to I$. Though seemingly innocent, being able to extend every family
+$f_{i} : \cE_{u_i}(A', B_{i}')$ is equivalent to the displayed category
+being thin!
+
+For the forward direction, suppose that $\cE$ is thin.
+Let $f_{i} : \cE{u_i}(A', B_{i}')$ be a family such that the restriction
+of $f_{i}$ along a map $e : I' \to I$ is jointly cartesian.
+We can then easily extend the family $f_{i}$ along an arbitrary map
+by ignoring every single equality, as all hom sets involved are thin.
+
+```agda
+thin→jointly-cartesian-extend
+ : ∀ {u : (i : Ix) → Hom a (bᵢ i)} {fᵢ : (i : Ix) → Hom[ uᵢ i ] a' (bᵢ' i)}
+ → (∀ {x} (v : Hom x a) → (x' : Ob[ x ]) → ∀ (i : Ix) → is-prop (Hom[ uᵢ i ∘ v ] x' (bᵢ' i)))
+ → (e : Ix' → Ix)
+ → is-jointly-cartesian (λ i' → uᵢ (e i')) (λ i' → fᵢ (e i'))
+ → is-jointly-cartesian (λ i → uᵢ i) (λ i → fᵢ i)
+thin→jointly-cartesian-extend {uᵢ = uᵢ} {fᵢ = fᵢ} uᵢ∘v-thin e fₑᵢ-cart = fᵢ-cart where
+ module fₑᵢ = is-jointly-cartesian fₑᵢ-cart
+ open is-jointly-cartesian
+
+ fᵢ-cart : is-jointly-cartesian (λ i' → uᵢ i') (λ i' → fᵢ i')
+ fᵢ-cart .universal v hᵢ =
+ fₑᵢ.universal v (λ i' → hᵢ (e i'))
+ fᵢ-cart .commutes {x} {x'} v hᵢ i =
+ uᵢ∘v-thin v x' i (fᵢ i ∘' fₑᵢ.universal v (λ i' → hᵢ (e i'))) (hᵢ i)
+ fᵢ-cart .unique {x} {x'} {v} {hᵢ} other p =
+ fₑᵢ.unique other λ i' → uᵢ∘v-thin v x' (e i') (fᵢ (e i') ∘' other) (hᵢ (e i'))
+```
+
+For the reverse direction, suppose we could extend arbitrary families.
+In particular, this means that we can extend singleton families to constant
+families, which lets us transfer a proof that a morphism is cartesian to
+a proof that a constant family is jointly cartesian.
+
+In particular, this means that the pair $(\id, \id)$ is jointly cartesian,
+which means that the hom set is thin!
+
+```agda
+jointly-cartesian-extend→thin
+ : ∀ (extend
+ : ∀ {Ix' Ix : Type} {bᵢ : Ix → Ob} {bᵢ' : (i : Ix) → Ob[ bᵢ i ]}
+ → {uᵢ : (i : Ix) → Hom a (bᵢ i)} {fᵢ : (i : Ix) → Hom[ uᵢ i ] a' (bᵢ' i)}
+ → (e : Ix' → Ix)
+ → is-jointly-cartesian (λ i' → uᵢ (e i')) (λ i' → fᵢ (e i'))
+ → is-jointly-cartesian (λ i → uᵢ i) (λ i → fᵢ i))
+ → ∀ {x} (v : Hom x a) → (x' : Ob[ x ]) → is-prop (Hom[ v ] x' a')
+jointly-cartesian-extend→thin extend v x' =
+ id-pair-joint-cartesian→thin
+ (extend (λ _ → true)
+ (cartesian→jointly-cartesian ⊤-is-contr cartesian-id))
+ v x'
+```
+
+## Universal properties
+
+Jointly cartesian families have an alternative presentation of their
+universal property: a family $f_{i} : \cE_{u_i}(A', B_{i}')$ is jointly
+cartesian if and only if the joint postcomposition map
+
+$$h \mapsto \lambda i.\; f_{i} \circ h$$
+
+is an [[equivalence]].
+
+```agda
+postcompose-equiv→jointly-cartesian
+ : {uᵢ : ∀ ix → Hom a (bᵢ ix)}
+ → (fᵢ : ∀ ix → Hom[ uᵢ ix ] a' (bᵢ' ix))
+ → (∀ {x} (v : Hom x a) → (x' : Ob[ x ])
+ → is-equiv {B = ∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix)} (λ h ix → fᵢ ix ∘' h))
+ → is-jointly-cartesian uᵢ fᵢ
+
+jointly-cartesian→postcompose-equiv
+ : {uᵢ : ∀ ix → Hom a (bᵢ ix)}
+ → {fᵢ : ∀ ix → Hom[ uᵢ ix ] a' (bᵢ' ix)}
+ → is-jointly-cartesian uᵢ fᵢ
+ → ∀ {x} (v : Hom x a) → (x' : Ob[ x ])
+ → is-equiv {B = ∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix)} (λ h ix → fᵢ ix ∘' h)
+```
+
+
+The proofs are just shuffling about data, so we shall skip
+over the details.
+
+```agda
+postcompose-equiv→jointly-cartesian {a = a} {uᵢ = uᵢ} fᵢ eqv = fᵢ-cart where
+ module eqv {x} {v : Hom x a} {x' : Ob[ x ]} = Equiv (_ , eqv v x')
+ open is-jointly-cartesian
+
+ fᵢ-cart : is-jointly-cartesian uᵢ fᵢ
+ fᵢ-cart .universal v hᵢ =
+ eqv.from hᵢ
+ fᵢ-cart .commutes v hᵢ ix =
+ eqv.ε hᵢ ·ₚ ix
+ fᵢ-cart .unique {hᵢ = hᵢ} other p =
+ sym (eqv.η other) ∙ ap eqv.from (ext p)
+
+jointly-cartesian→postcompose-equiv {uᵢ = uᵢ} {fᵢ = fᵢ} fᵢ-cart v x' .is-eqv hᵢ =
+ contr (fᵢ.universal v hᵢ , ext (fᵢ.commutes v hᵢ)) λ fib →
+ Σ-prop-pathp! (sym (fᵢ.unique (fib .fst) (λ ix → fib .snd ·ₚ ix)))
+ where
+ module fᵢ = is-jointly-cartesian fᵢ-cart
+```
+
+
+## Jointly cartesian lifts
+
+:::{.definition #jointly-cartesian-lift}
+A **jointly cartesian lift** of a family of objects $Y_{i}' \liesover Y_{i}$
+along a family of maps $u_{i} : \cB(X, Y_{i})$ is an object
+$\bigcap_{i : I} u_{i}^{*} Y_{i}$ equipped with a jointly cartesian family
+$\pi_{i} : \cE_{u_i}(\bigcap_{i : I} u_{i}^{*} Y_{i}, Y_{i})$.
+:::
+
+```agda
+record Joint-cartesian-lift
+ {ℓi : Level} {Ix : Type ℓi}
+ {x : Ob} {yᵢ : Ix → Ob}
+ (uᵢ : (ix : Ix) → Hom x (yᵢ ix))
+ (yᵢ' : (ix : Ix) → Ob[ yᵢ ix ])
+ : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ' ⊔ ℓi)
+ where
+ no-eta-equality
+ field
+ {x'} : Ob[ x ]
+ lifting : (ix : Ix) → Hom[ uᵢ ix ] x' (yᵢ' ix)
+ jointly-cartesian : is-jointly-cartesian uᵢ lifting
+
+ open is-jointly-cartesian jointly-cartesian public
+```
+
+:::{.definition #jointly-cartesian-fibration}
+A **$\kappa$ jointly cartesian fibration** is a displayed category
+that joint cartesian lifts of all $\kappa$-small families.
+:::
+
+```agda
+Jointly-cartesian-fibration : (κ : Level) → Type _
+Jointly-cartesian-fibration κ =
+ ∀ (Ix : Type κ)
+ → {x : Ob} {yᵢ : Ix → Ob}
+ → (uᵢ : (ix : Ix) → Hom x (yᵢ ix))
+ → (yᵢ' : (ix : Ix) → Ob[ yᵢ ix ])
+ → Joint-cartesian-lift uᵢ yᵢ'
+
+module Jointly-cartesian-fibration {κ} (fib : Jointly-cartesian-fibration κ) where
+```
+
+
+The following section defines some nice notation for jointly
+cartesian fibrations, but is a bit verbose.
+
+```agda
+ module _
+ (Ix : Type κ) {x : Ob} {yᵢ : Ix → Ob}
+ (uᵢ : (ix : Ix) → Hom x (yᵢ ix))
+ (yᵢ' : (ix : Ix) → Ob[ yᵢ ix ])
+ where
+ open Joint-cartesian-lift (fib Ix uᵢ yᵢ')
+ using ()
+ renaming (x' to ∏*)
+ public
+
+ module _
+ {Ix : Type κ} {x : Ob} {yᵢ : Ix → Ob}
+ (uᵢ : (ix : Ix) → Hom x (yᵢ ix))
+ (yᵢ' : (ix : Ix) → Ob[ yᵢ ix ])
+ where
+ open Joint-cartesian-lift (fib Ix uᵢ yᵢ')
+ using ()
+ renaming (lifting to π*)
+ public
+
+ module π*
+ {Ix : Type κ} {x : Ob} {yᵢ : Ix → Ob}
+ {uᵢ : (ix : Ix) → Hom x (yᵢ ix)}
+ {yᵢ' : (ix : Ix) → Ob[ yᵢ ix ]}
+ where
+ open Joint-cartesian-lift (fib Ix uᵢ yᵢ')
+ hiding (x'; lifting)
+ public
+```
+
+
+Every jointly cartesian fibration has objects that act like codiscrete
+spaces arising from lifts of empty families.
+
+```agda
+ opaque
+ Codisc* : ∀ (x : Ob) → Ob[ x ]
+ Codisc* x = ∏* (Lift _ ⊥) {yᵢ = λ ()} (λ ()) (λ ())
+
+ codisc*
+ : ∀ {x y : Ob}
+ → (u : Hom x y) (x' : Ob[ x ])
+ → Hom[ u ] x' (Codisc* y)
+ codisc* u x' = π*.universal u (λ ())
+
+ codisc*-unique
+ : ∀ {x y : Ob}
+ → {u : Hom x y} {x' : Ob[ x ]}
+ → (other : Hom[ u ] x' (Codisc* y))
+ → other ≡ codisc* u x'
+ codisc*-unique other = π*.unique other (λ ())
+```
diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md
index 0b92856ad..32c233e44 100644
--- a/src/Cat/Displayed/Cocartesian.lagda.md
+++ b/src/Cat/Displayed/Cocartesian.lagda.md
@@ -289,7 +289,7 @@ cocartesian-vertical-section-stable
→ ϕ ∘' f'' ≡[ idl _ ] f'
→ is-cocartesian f f''
-cocartesian-pasting
+cocartesian-cancelr
: ∀ {x y z} {f : Hom y z} {g : Hom x y}
→ ∀ {x' y' z'} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
→ is-cocartesian g g'
@@ -337,9 +337,9 @@ cocartesian-vertical-section-stable cocart ret factor =
(vertical-retract→vertical-co-section ret)
factor
-cocartesian-pasting g-cocart fg-cocart =
+cocartesian-cancelr g-cocart fg-cocart =
co-cartesian→cocartesian $
- cartesian-pasting (ℰ ^total-op)
+ cartesian-cancell (ℰ ^total-op)
(cocartesian→co-cartesian g-cocart)
(cocartesian→co-cartesian fg-cocart)
diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md
index 328465fe1..7b4dc1dec 100644
--- a/src/Cat/Displayed/Instances/Subobjects.lagda.md
+++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md
@@ -32,7 +32,7 @@ open Displayed
```
-->
-# The fibration of subobjects {defines="poset-of-subobjects subobject"}
+# The fibration of subobjects {defines="poset-of-subobjects subobject subobject-fibration"}
Given a base category $\cB$, we can define the [[displayed category]] of
_subobjects_ over $\cB$. This is, in essence, a restriction of the
diff --git a/src/Cat/Displayed/Instances/Trivial.lagda.md b/src/Cat/Displayed/Instances/Trivial.lagda.md
index 40bbb6bcb..11fc14a81 100644
--- a/src/Cat/Displayed/Instances/Trivial.lagda.md
+++ b/src/Cat/Displayed/Instances/Trivial.lagda.md
@@ -1,7 +1,9 @@
@@ -21,13 +26,19 @@ module Cat.Displayed.Instances.Trivial
-# The trivial bifibration
+# The trivial bifibration {defines="trivial-bifibration"}
Any category $\ca{C}$ can be regarded as being displayed over the
[[terminal category]] $\top$.
@@ -44,6 +55,30 @@ Trivial .Displayed.idl' = idl
Trivial .Displayed.assoc' = assoc
```
+
+
All morphisms in the trivial [[displayed category]] are vertical over
the same object, so producing cartesian lifts is extremely easy: just
use the identity morphism!
@@ -76,6 +111,90 @@ Trivial-bifibration .is-bifibration.fibration = Trivial-fibration
Trivial-bifibration .is-bifibration.opfibration = Trivial-opfibration
```
+The joint cartesian morphisms in the trivial displayed category
+are precisely the projections out of [[indexed products]].
+
+```agda
+trivial-joint-cartesian→product
+ : ∀ {κ} {Ix : Type κ}
+ → {∏xᵢ : Ob} {xᵢ : Ix → Ob} {π : (i : Ix) → Hom ∏xᵢ (xᵢ i)}
+ → is-jointly-cartesian Trivial (λ _ → tt) π
+ → is-indexed-product 𝒞 xᵢ π
+
+product→trivial-joint-cartesian
+ : ∀ {κ} {Ix : Type κ}
+ → {∏xᵢ : Ob} {xᵢ : Ix → Ob} {π : (i : Ix) → Hom ∏xᵢ (xᵢ i)}
+ → is-indexed-product 𝒞 xᵢ π
+ → is-jointly-cartesian Trivial (λ _ → tt) π
+```
+
+
+The proofs are basically just shuffling data around,
+so we will not describe the details.
+
+
+```agda
+trivial-joint-cartesian→product {xᵢ = xᵢ} {π = π} π-cart =
+ π-product
+ where
+ module π = is-jointly-cartesian π-cart
+ open is-indexed-product
+
+ π-product : is-indexed-product 𝒞 xᵢ π
+ π-product .tuple fᵢ = π.universal tt fᵢ
+ π-product .commute = π.commutes tt _ _
+ π-product .unique fᵢ p = π.unique _ p
+
+product→trivial-joint-cartesian {xᵢ = xᵢ} {π = π} π-product =
+ π-cart
+ where
+ module π = is-indexed-product π-product
+ open is-jointly-cartesian
+
+ π-cart : is-jointly-cartesian Trivial (λ _ → tt) π
+ π-cart .universal tt fᵢ = π.tuple fᵢ
+ π-cart .commutes tt fᵢ ix = π.commute
+ π-cart .unique other p = π.unique _ p
+```
+
+
+In contrast, the cartesian morphisms in the trivial displayed category
+are the invertible morphisms.
+
+```agda
+invertible→trivial-cartesian
+ : ∀ {a b} {f : Hom a b}
+ → is-invertible f
+ → is-cartesian Trivial tt f
+
+trivial-cartesian→invertible
+ : ∀ {a b} {f : Hom a b}
+ → is-cartesian Trivial tt f
+ → is-invertible f
+```
+
+The forward direction is easy: every invertible morphism is cartesian,
+and the invertible morphisms in the trivial displayed category on $\cC$ are
+the invertible maps in $\cC$.
+
+```agda
+invertible→trivial-cartesian f-inv =
+ invertible→cartesian Trivial
+ (⊤Cat-is-pregroupoid tt)
+ (invertible→trivial-invertible f-inv)
+```
+
+For the reverse direction, recall that all vertical cartesian morphisms
+are invertible. Every morphism in the trivial displayed category is vertical,
+so cartesianness implies invertibility.
+
+```agda
+trivial-cartesian→invertible f-cart =
+ trivial-invertible→invertible $
+ vertical+cartesian→invertible Trivial f-cart
+```
+
+
Furthermore, the [[total category]] of the trivial bifibration is *isomorphic*
to the category we started with.
diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md
index d404266ef..8afd2f2dd 100644
--- a/src/Cat/Displayed/Morphism.lagda.md
+++ b/src/Cat/Displayed/Morphism.lagda.md
@@ -22,9 +22,14 @@ open Displayed ℰ
open Cat.Reasoning ℬ
open Cat.Displayed.Reasoning ℰ
private variable
+ ℓi : Level
+ Ix : Type ℓi
a b c d : Ob
- f : Hom a b
+ aᵢ bᵢ cᵢ : Ix → Ob
+ f g h : Hom a b
a' b' c' : Ob[ a ]
+ aᵢ' bᵢ' cᵢ' : (ix : Ix) → Ob[ bᵢ ix ]
+ f' g' h' : Hom[ f ] a' b'
```
-->
@@ -71,7 +76,7 @@ record _↪[_]_
open _↪[_]_ public
```
-## Weak monos
+## Weak monos {defines="weak-monomorphism weakly-monic"}
When working in a displayed setting, we also have weaker versions of
the morphism classes we are familiar with, wherein we can only left/right
@@ -84,18 +89,17 @@ is-weak-monic
→ Hom[ f ] a' b'
→ Type _
is-weak-monic {a = a} {a' = a'} {f = f} f' =
- ∀ {c c'} {g : Hom c a}
- → (g' g'' : Hom[ g ] c' a')
- → f' ∘' g' ≡ f' ∘' g''
- → g' ≡ g''
+ ∀ {c c'} {g h : Hom c a}
+ → (g' : Hom[ g ] c' a') (h' : Hom[ h ] c' a')
+ → (p : g ≡ h)
+ → f' ∘' g' ≡[ ap (f ∘_) p ] f' ∘' h'
+ → g' ≡[ p ] h'
is-weak-monic-is-prop
: ∀ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
→ (f' : Hom[ f ] a' b')
→ is-prop (is-weak-monic f')
-is-weak-monic-is-prop f' mono mono' i g' g'' p =
- is-prop→pathp (λ i → Hom[ _ ]-set _ _ g' g'')
- (mono g' g'' p) (mono' g' g'' p) i
+is-weak-monic-is-prop f' = hlevel 1
record weak-mono-over
{a b} (f : Hom a b) (a' : Ob[ a ]) (b' : Ob[ b ])
@@ -109,6 +113,112 @@ record weak-mono-over
open weak-mono-over public
```
+Weak monomorphisms are closed under composition, and every displayed
+monomorphism is weakly monic.
+
+```agda
+weak-monic-∘
+ : is-weak-monic f'
+ → is-weak-monic g'
+ → is-weak-monic (f' ∘' g')
+weak-monic-∘ {f' = f'} {g' = g'} f'-weak-monic g'-weak-monic h' k' p p' =
+ g'-weak-monic h' k' p $
+ f'-weak-monic (g' ∘' h') (g' ∘' k') (ap₂ _∘_ refl p) $
+ cast[] $
+ f' ∘' g' ∘' h' ≡[]⟨ assoc' f' g' h' ⟩
+ (f' ∘' g') ∘' h' ≡[]⟨ p' ⟩
+ (f' ∘' g') ∘' k' ≡[]˘⟨ assoc' f' g' k' ⟩
+ f' ∘' g' ∘' k' ∎
+
+is-monic[]→is-weak-monic
+ : {f-monic : is-monic f}
+ → is-monic[ f-monic ] f'
+ → is-weak-monic f'
+is-monic[]→is-weak-monic f'-monic g' h' p p' =
+ cast[] $ f'-monic g' h' (ap₂ _∘_ refl p) p'
+```
+
+If $f' \circ g'$ is weakly monic, then so is $g'$.
+
+```agda
+weak-monic-cancell
+ : is-weak-monic (f' ∘' g')
+ → is-weak-monic g'
+weak-monic-cancell {f' = f'} {g' = g'} fg-weak-monic h' k' p p' =
+ fg-weak-monic h' k' p (extendr' _ p')
+```
+
+Moreover, postcomposition with a weak monomorphism is an [[embedding]].
+This suggests that weak monomorphisms are the "right" notion of
+monomorphisms in displayed categories.
+
+```agda
+weak-monic-postcomp-embedding
+ : {f : Hom b c} {g : Hom a b}
+ → {f' : Hom[ f ] b' c'}
+ → is-weak-monic f'
+ → is-embedding {A = Hom[ g ] a' b'} (f' ∘'_)
+weak-monic-postcomp-embedding {f' = f'} f'-weak-monic =
+ injective→is-embedding (hlevel 2) (f' ∘'_) λ {g'} {h'} → f'-weak-monic g' h' refl
+```
+
+### Jointly weak monos
+
+We can generalize the notion of weak monomorphisms to families of morphisms, which
+yields a displayed version of a [[jointly monic family]].
+
+:::{.definition #jointly-weak-monic-family}
+A family of displayed morphisms $f_{i}' : A' \to_{f_{i}} B_{i}'$ is *jointly monic*
+if for all $g', g'' : X' \to_{g} A'$, $g' = g''$ if $f_{i}' \circ g' = f_{i} \circ g''$
+for all $i : I$.
+:::
+
+```agda
+is-jointly-weak-monic
+ : {fᵢ : (ix : Ix) → Hom a (bᵢ ix)}
+ → (fᵢ' : (ix : Ix) → Hom[ fᵢ ix ] a' (bᵢ' ix))
+ → Type _
+is-jointly-weak-monic {a = a} {a' = a'} {fᵢ = fᵢ} fᵢ' =
+ ∀ {x x'} {g h : Hom x a}
+ → (g' : Hom[ g ] x' a') (h' : Hom[ h ] x' a')
+ → (p : g ≡ h)
+ → (∀ ix → fᵢ' ix ∘' g' ≡[ ap (fᵢ ix ∘_) p ] fᵢ' ix ∘' h')
+ → g' ≡[ p ] h'
+```
+
+Jointly weak monic families are closed under precomposition
+with weak monos.
+
+```agda
+jointly-weak-monic-∘
+ : {fᵢ : (ix : Ix) → Hom a (bᵢ ix)}
+ → {fᵢ' : (ix : Ix) → Hom[ fᵢ ix ] a' (bᵢ' ix)}
+ → is-jointly-weak-monic fᵢ'
+ → is-weak-monic g'
+ → is-jointly-weak-monic (λ ix → fᵢ' ix ∘' g')
+jointly-weak-monic-∘ {g' = g'} {fᵢ' = fᵢ'} fᵢ'-joint-mono g'-joint-mono h' h'' p p' =
+ g'-joint-mono h' h'' p $
+ fᵢ'-joint-mono (g' ∘' h') (g' ∘' h'') (ap₂ _∘_ refl p) λ ix →
+ cast[] $
+ fᵢ' ix ∘' g' ∘' h' ≡[]⟨ assoc' (fᵢ' ix) g' h' ⟩
+ (fᵢ' ix ∘' g') ∘' h' ≡[]⟨ p' ix ⟩
+ (fᵢ' ix ∘' g') ∘' h'' ≡[]˘⟨ assoc' (fᵢ' ix) g' h'' ⟩
+ fᵢ' ix ∘' g' ∘' h'' ∎
+```
+
+Similarly, if $f_{i}' \circ g'$ is a jointly weak monic family, then
+$g'$ must be a weak mono.
+
+```agda
+jointly-weak-monic-cancell
+ : {fᵢ : (ix : Ix) → Hom a (bᵢ ix)}
+ → {fᵢ' : (ix : Ix) → Hom[ fᵢ ix ] a' (bᵢ' ix)}
+ → is-jointly-weak-monic (λ ix → fᵢ' ix ∘' g')
+ → is-weak-monic g'
+jointly-weak-monic-cancell fᵢ'-joint-mono h' h'' p p' =
+ fᵢ'-joint-mono h' h'' p λ _ → extendr' (ap₂ _∘_ refl p) p'
+```
+
## Epis
Displayed [epimorphisms] are defined in a similar fashion.
@@ -158,18 +268,17 @@ is-weak-epic
→ Hom[ f ] a' b'
→ Type _
is-weak-epic {b = b} {b' = b'} {f = f} f' =
- ∀ {c c'} {g : Hom b c}
- → (g' g'' : Hom[ g ] b' c')
- → g' ∘' f' ≡ g'' ∘' f'
- → g' ≡ g''
+ ∀ {c c'} {g h : Hom b c}
+ → (g' : Hom[ g ] b' c') (h' : Hom[ h ] b' c')
+ → (p : g ≡ h)
+ → g' ∘' f' ≡[ ap (_∘ f) p ] h' ∘' f'
+ → g' ≡[ p ] h'
is-weak-epic-is-prop
: ∀ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
→ (f' : Hom[ f ] a' b')
- → is-prop (is-weak-monic f')
-is-weak-epic-is-prop f' epi epi' i g' g'' p =
- is-prop→pathp (λ i → Hom[ _ ]-set _ _ g' g'')
- (epi g' g'' p) (epi' g' g'' p) i
+ → is-prop (is-weak-epic f')
+is-weak-epic-is-prop f' = hlevel 1
record weak-epi-over
{a b} (f : Hom a b) (a' : Ob[ a ]) (b' : Ob[ b ])
@@ -550,3 +659,50 @@ iso[]→from-has-retract[]
iso[]→from-has-retract[] f' .retract' = f' .to'
iso[]→from-has-retract[] f' .is-retract' = f' .invl'
```
+
+
diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md
index 0578544ae..90d1763b8 100644
--- a/src/Cat/Displayed/Reasoning.lagda.md
+++ b/src/Cat/Displayed/Reasoning.lagda.md
@@ -79,13 +79,13 @@ 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}
+ → {f' : E.Hom[ f ] x y}
→ hom[ q ] (hom[ p ] f') ≡ hom[ p ∙ q ] f'
hom[]-∙ p q = sym (subst-∙ (λ h → E.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}
+ → {f' : E.Hom[ f ] x y}
→ hom[ p ] f' ≡ hom[ q ] (hom[ r ] f')
duplicate p q r = reindex _ _ ∙ sym (hom[]-∙ r q)
```
@@ -105,7 +105,7 @@ 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'}
+ → {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
→ (p : g ≡ g₁)
→ f' E.∘' hom[ p ] g' ≡ hom[ ap (f B.∘_) p ] (f' E.∘' g')
whisker-r {f = f} {a' = a'} {_} {c'} {f'} {g'} p i =
@@ -116,7 +116,7 @@ whisker-r {f = f} {a' = a'} {_} {c'} {f'} {g'} p 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'}
+ → {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
→ (p : f ≡ f₁)
→ hom[ p ] f' E.∘' g' ≡ hom[ ap (B._∘ g) p ] (f' E.∘' g')
whisker-l {g = g} {a'} {_} {c'} {f' = f'} {g' = g'} p i =
@@ -130,14 +130,14 @@ whisker-l {g = g} {a'} {_} {c'} {f' = f'} {g' = g'} p i =
```agda
unwhisker-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'}
+ → {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
→ (p : f B.∘ g ≡ f B.∘ g₁) (q : g ≡ g₁)
→ hom[ p ] (f' E.∘' g') ≡ f' E.∘' hom[ q ] g'
unwhisker-r p q = reindex _ _ ∙ sym (whisker-r _)
unwhisker-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'}
+ → {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
→ (p : f B.∘ g ≡ f₁ B.∘ g) (q : f ≡ f₁)
→ hom[ p ] (f' E.∘' g') ≡ hom[ q ] f' E.∘' g'
unwhisker-l p q = reindex _ _ ∙ sym (whisker-l _)
@@ -150,38 +150,37 @@ 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'}
+ → {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')
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'}
+ → {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')
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'}
+ → {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')
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'}
+ → {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')
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}
- {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)
+ : ∀ {a b c d 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' : 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'
yank {f' = f'} {g' = g'} {h' = h'} p q r = to-pathp $
hom[ r ] (f' E.∘' hom[ p ] (g' E.∘' h')) ≡⟨ smashr p r ⟩
@@ -206,11 +205,12 @@ kill₁
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'}
- → {p : f ≡ g} {q : f ≡ h}
- → f' E.≡[ p ] g'
- → hom[ q ] f' ≡ hom[ sym p ∙ q ] g'
+revive₁
+ : ∀ {a b a' b'} {f g h : B.Hom a b}
+ → {f' : E.Hom[ f ] a' b'} {g' : E.Hom[ g ] a' b'}
+ → {p : f ≡ g} {q : f ≡ h}
+ → f' E.≡[ p ] g'
+ → hom[ q ] f' ≡ hom[ sym p ∙ q ] g'
revive₁ {f' = f'} {g' = g'} {p = p} {q = q} p' =
hom[ q ] f' ≡⟨ reindex _ _ ⟩
hom[ p ∙ sym p ∙ q ] f' ≡⟨ kill₁ p (sym p ∙ q) p' ⟩
@@ -230,8 +230,8 @@ weave p 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'}
- (p : f ≡ f₁) (q : g ≡ g₁)
+ → {f' : E.Hom[ f ] b' c'} {g' : E.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'
split p q =
reindex _ (ap₂ B._∘_ p refl ∙ ap₂ B._∘_ refl q)
@@ -240,22 +240,22 @@ split p q =
liberate
: ∀ {a b x y} {f : B.Hom a b} {f' : E.Hom[ f ] x y}
- (p : f ≡ f)
- → hom[ p ] f' ≡ f'
+ → (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'}
+ → {f' g' : E.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'}
- {p : f ≡ f'} {q : g ≡ g'}
+ → {f₁' : E.Hom[ f ] b' c'} {f₂' : E.Hom[ f' ] b' c'}
+ → {g₁' : E.Hom[ g ] a' b'} {g₂' : E.Hom[ g' ] a' b'}
+ → {p : f ≡ f'} {q : g ≡ g'}
→ f₁' E.≡[ p ] f₂'
→ g₁' E.≡[ q ] g₂'
→ f₁' E.∘' g₁' E.≡[ ap₂ B._∘_ p q ] f₂' E.∘' g₂'
@@ -263,26 +263,26 @@ _⟩∘'⟨_
_⟩∘'⟨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'}
- {p : f ≡ f'}
+ → {f₁' : E.Hom[ f ] b' c'} {f₂' : E.Hom[ f' ] b' c'} {g' : E.Hom[ g ] a' b'}
+ → {p : f ≡ f'}
→ f₁' E.≡[ p ] f₂'
→ f₁' E.∘' g' E.≡[ p B.⟩∘⟨refl ] f₂' E.∘' g'
_⟩∘'⟨refl {g' = g'} p = apd (λ _ → E._∘' g') p
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'}
- {q : g ≡ g'}
+ → {f' : E.Hom[ f ] b' c'}
+ → {g₁' : E.Hom[ g ] a' b'} {g₂' : E.Hom[ g' ] a' b'}
+ → {q : g ≡ g'}
→ g₁' E.≡[ q ] g₂'
→ f' E.∘' g₁' E.≡[ B.refl⟩∘⟨ q ] f' E.∘' g₂'
refl⟩∘'⟨_ {f' = f'} p = apd (λ _ → f' E.∘'_) 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'}
- {p : f ≡ f'} {q : g ≡ g'}
+ → {f₁' : E.Hom[ f ] b' c'} {f₂' : E.Hom[ f' ] b' c'}
+ → {g₁' : E.Hom[ g ] a' b'} {g₂' : E.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₂'
split⟩⟨ p = split _ _ ∙ p
@@ -295,11 +295,11 @@ 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'}
+ → {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')
@@ -392,20 +392,22 @@ situation.
```agda
module _ {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'} {p : f ∘ g ≡ a} where abstract
- apl' : ∀ {h' : Hom[ h ] y' z'} {q : h ∘ g ≡ a}
- → {f≡h : f ≡ h}
- → f' ≡[ f≡h ] h'
- → hom[ p ] (f' ∘' g') ≡ hom[ q ] (h' ∘' g')
+ apl'
+ : ∀ {h' : Hom[ h ] y' z'} {q : h ∘ g ≡ a}
+ → {f≡h : f ≡ h}
+ → f' ≡[ f≡h ] h'
+ → hom[ p ] (f' ∘' g') ≡ hom[ q ] (h' ∘' g')
apl' {h' = h'} {q = q} {f≡h = f≡h} f'≡h' =
hom[ p ] (f' ∘' g') ≡⟨ hom[]⟩⟨ (ap (_∘' g') (shiftr _ f'≡h')) ⟩
hom[ p ] (hom[ f≡h ]⁻ h' ∘' g') ≡⟨ smashl _ _ ⟩
hom[ ap (_∘ g) (sym f≡h) ∙ p ] (h' ∘' g') ≡⟨ reindex _ _ ⟩
hom[ q ] (h' ∘' g') ∎
- apr' : ∀ {h' : Hom[ h ] x' y'} {q : f ∘ h ≡ a}
- → {g≡h : g ≡ h}
- → g' ≡[ g≡h ] h'
- → hom[ p ] (f' ∘' g') ≡ hom[ q ] (f' ∘' h')
+ apr'
+ : ∀ {h' : Hom[ h ] x' y'} {q : f ∘ h ≡ a}
+ → {g≡h : g ≡ h}
+ → g' ≡[ g≡h ] h'
+ → hom[ p ] (f' ∘' g') ≡ hom[ q ] (f' ∘' h')
apr' {h' = h'} {q = q} {g≡h = g≡h} g'≡h' =
hom[ p ] (f' ∘' g') ≡⟨ hom[]⟩⟨ ap (f' ∘'_) (shiftr _ g'≡h') ⟩
hom[ p ] (f' ∘' hom[ g≡h ]⁻ h') ≡⟨ smashr _ _ ⟩
@@ -432,9 +434,10 @@ module _ {f' : Hom[ f ] x' y'} where abstract
id-comm[] : {p : id ∘ f ≡ f ∘ id} → hom[ p ] (id' ∘' f') ≡ f' ∘' id'
id-comm[] {p = p} = duplicate _ _ _ ∙ ap hom[] (from-pathp (idl' _)) ∙ from-pathp (symP (idr' _))
-assoc[] : ∀ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'}
- {p : a ∘ (b ∘ c) ≡ d} {q : (a ∘ b) ∘ c ≡ d}
- → hom[ p ] (a' ∘' (b' ∘' c')) ≡ hom[ q ] ((a' ∘' b') ∘' c')
+assoc[]
+ : ∀ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'}
+ → {p : a ∘ (b ∘ c) ≡ d} {q : (a ∘ b) ∘ c ≡ d}
+ → hom[ p ] (a' ∘' (b' ∘' c')) ≡ hom[ q ] ((a' ∘' b') ∘' c')
assoc[] {a = a} {b = b} {c = c} {a' = a'} {b' = b'} {c' = c'} {p = p} {q = q} =
hom[ p ] (a' ∘' b' ∘' c') ≡⟨ hom[]⟩⟨ shiftr (assoc a b c) (assoc' a' b' c') ⟩
hom[ p ] (hom[ assoc a b c ]⁻ ((a' ∘' b') ∘' c')) ≡⟨ hom[]-∙ _ _ ⟩
@@ -492,74 +495,85 @@ for categories.
module _ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] x' z'}
(p : a ∘ b ≡ c) (p' : a' ∘' b' ≡[ p ] c') where abstract
- pulll' : ∀ {f' : Hom[ f ] w' x'} {q : a ∘ (b ∘ f) ≡ c ∘ f}
- → a' ∘' (b' ∘' f') ≡[ q ] c' ∘' f'
+ pulll'
+ : ∀ {f' : Hom[ f ] w' x'} {q : a ∘ (b ∘ f) ≡ c ∘ f}
+ → a' ∘' (b' ∘' f') ≡[ q ] c' ∘' f'
pulll' {f = f} {f' = f'} {q = q} = to-pathp $
hom[ q ] (a' ∘' b' ∘' f') ≡⟨ assoc[] ⟩
hom[ sym (assoc a b f) ∙ q ] ((a' ∘' b') ∘' f') ≡⟨ apl' p' ⟩
hom[ refl ] (c' ∘' f') ≡⟨ liberate _ ⟩
c' ∘' f' ∎
- pulll[] : ∀ {f' : Hom[ f ] w' x'}
- → a' ∘' (b' ∘' f') ≡[ pulll p ] c' ∘' f'
+ pulll[]
+ : ∀ {f' : Hom[ f ] w' x'}
+ → a' ∘' (b' ∘' f') ≡[ pulll p ] c' ∘' f'
pulll[] = pulll'
- pullr' : ∀ {f' : Hom[ f ] z' w'} {q : (f ∘ a) ∘ b ≡ f ∘ c}
- → (f' ∘' a') ∘' b' ≡[ q ] f' ∘' c'
+ pullr'
+ : ∀ {f' : Hom[ f ] z' w'} {q : (f ∘ a) ∘ b ≡ f ∘ c}
+ → (f' ∘' a') ∘' b' ≡[ q ] f' ∘' c'
pullr' {f = f} {f' = f'} {q = q} = to-pathp $
hom[ q ] ((f' ∘' a') ∘' b') ≡˘⟨ assoc[] ⟩
hom[ assoc f a b ∙ q ] (f' ∘' a' ∘' b') ≡⟨ apr' p' ⟩
hom[ refl ] (f' ∘' c') ≡⟨ liberate _ ⟩
f' ∘' c' ∎
- pullr[] : ∀ {f' : Hom[ f ] z' w'}
- → (f' ∘' a') ∘' b' ≡[ pullr p ] f' ∘' c'
+ pullr[]
+ : ∀ {f' : Hom[ f ] z' w'}
+ → (f' ∘' a') ∘' b' ≡[ pullr p ] f' ∘' c'
pullr[] = pullr'
module _ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] x' z'}
(p : c ≡ a ∘ b) (p' : c' ≡[ p ] a' ∘' b') where abstract
- pushl' : ∀ {f' : Hom[ f ] w' x'} {q : c ∘ f ≡ a ∘ (b ∘ f)}
- → c' ∘' f' ≡[ q ] a' ∘' (b' ∘' f')
+ pushl'
+ : ∀ {f' : Hom[ f ] w' x'} {q : c ∘ f ≡ a ∘ (b ∘ f)}
+ → c' ∘' f' ≡[ q ] a' ∘' (b' ∘' f')
pushl' {f' = f'} {q = q} i =
pulll' (sym p) (λ j → p' (~ j)) {f' = f'} {q = sym q} (~ i)
- pushl[] : ∀ {f' : Hom[ f ] w' x'}
- → c' ∘' f' ≡[ pushl p ] a' ∘' (b' ∘' f')
+ pushl[]
+ : ∀ {f' : Hom[ f ] w' x'}
+ → c' ∘' f' ≡[ pushl p ] a' ∘' (b' ∘' f')
pushl[] = pushl'
- pushr' : ∀ {f' : Hom[ f ] z' w'} {q : f ∘ c ≡ (f ∘ a) ∘ b}
- → f' ∘' c' ≡[ q ] (f' ∘' a') ∘' b'
+ pushr'
+ : ∀ {f' : Hom[ f ] z' w'} {q : f ∘ c ≡ (f ∘ a) ∘ b}
+ → f' ∘' c' ≡[ q ] (f' ∘' a') ∘' b'
pushr' {f' = f'} {q = q} i =
pullr' (sym p) (λ j → p' (~ j)) {f' = f'} {q = sym q} (~ i)
- pushr[] : ∀ {f' : Hom[ f ] z' w'}
- → f' ∘' c' ≡[ pushr p ] (f' ∘' a') ∘' b'
+ pushr[]
+ : ∀ {f' : Hom[ f ] z' w'}
+ → f' ∘' c' ≡[ pushr p ] (f' ∘' a') ∘' b'
pushr[] = pushr'
module _ {f' : Hom[ f ] y' z'} {h' : Hom[ h ] x' y'}
{g' : Hom[ g ] y'' z'} {i' : Hom[ i ] x' y''}
(p : f ∘ h ≡ g ∘ i) (p' : f' ∘' h' ≡[ p ] g' ∘' i') where abstract
- extendl' : ∀ {b' : Hom[ b ] w' x'} {q : f ∘ (h ∘ b) ≡ g ∘ (i ∘ b)}
- → f' ∘' (h' ∘' b') ≡[ q ] g' ∘' (i' ∘' b')
+ extendl'
+ : ∀ {b' : Hom[ b ] w' x'} {q : f ∘ (h ∘ b) ≡ g ∘ (i ∘ b)}
+ → f' ∘' (h' ∘' b') ≡[ q ] g' ∘' (i' ∘' b')
extendl' {b = b} {b' = b'} {q = q} = to-pathp $
hom[ q ] (f' ∘' h' ∘' b') ≡⟨ assoc[] ⟩
hom[ sym (assoc f h b) ∙ q ] ((f' ∘' h') ∘' b') ≡⟨ apl' p' ⟩
hom[ sym (assoc g i b) ] ((g' ∘' i') ∘' b') ≡⟨ shiftl _ (λ j → (assoc' g' i' b') (~ j)) ⟩
g' ∘' i' ∘' b' ∎
- extendr' : ∀ {a' : Hom[ a ] z' w'} {q : (a ∘ f) ∘ h ≡ (a ∘ g) ∘ i}
- → (a' ∘' f') ∘' h' ≡[ q ] (a' ∘' g') ∘' i'
+ extendr'
+ : ∀ {a' : Hom[ a ] z' w'} {q : (a ∘ f) ∘ h ≡ (a ∘ g) ∘ i}
+ → (a' ∘' f') ∘' h' ≡[ q ] (a' ∘' g') ∘' i'
extendr' {a = a} {a' = a'} {q = q} = to-pathp $
hom[ q ] ((a' ∘' f') ∘' h') ≡˘⟨ assoc[] ⟩
hom[ assoc a f h ∙ q ] (a' ∘' f' ∘' h') ≡⟨ apr' p' ⟩
hom[ assoc a g i ] (a' ∘'(g' ∘' i')) ≡⟨ shiftl _ (assoc' a' g' i') ⟩
(a' ∘' g') ∘' i' ∎
- extend-inner' : ∀ {a' : Hom[ a ] z' u'} {b' : Hom[ b ] w' x'}
- {q : a ∘ f ∘ h ∘ b ≡ a ∘ g ∘ i ∘ b}
- → a' ∘' f' ∘' h' ∘' b' ≡[ q ] a' ∘' g' ∘' i' ∘' b'
+ extend-inner'
+ : ∀ {a' : Hom[ a ] z' u'} {b' : Hom[ b ] w' x'}
+ → {q : a ∘ f ∘ h ∘ b ≡ a ∘ g ∘ i ∘ b}
+ → a' ∘' f' ∘' h' ∘' b' ≡[ q ] a' ∘' g' ∘' i' ∘' b'
extend-inner' {a = a} {b = b} {a' = a'} {b' = b'} {q = q} = to-pathp $
hom[ q ] (a' ∘' f' ∘' h' ∘' b') ≡⟨ apr' (assoc' f' h' b') ⟩
hom[ ap (a ∘_) (sym (assoc f h b)) ∙ q ] (a' ∘' (f' ∘' h') ∘' b') ≡⟨ apr' (λ j → p' j ∘' b') ⟩
@@ -570,8 +584,9 @@ module _ {f' : Hom[ f ] y' z'} {h' : Hom[ h ] x' y'}
→ f' ∘' (h' ∘' b') ≡[ extendl p ] g' ∘' (i' ∘' b')
extendl[] = extendl'
- extendr[] : ∀ {a' : Hom[ a ] z' w'}
- → (a' ∘' f') ∘' h' ≡[ extendr p ] (a' ∘' g') ∘' i'
+ extendr[]
+ : ∀ {a' : Hom[ a ] z' w'}
+ → (a' ∘' f') ∘' h' ≡[ extendr p ] (a' ∘' g') ∘' i'
extendr[] = extendr'
```
@@ -586,42 +601,95 @@ for categories
module _ {a' : Hom[ a ] y' x'} {b' : Hom[ b ] x' y'}
(p : a ∘ b ≡ id) (p' : a' ∘' b' ≡[ p ] id') where abstract
- cancell' : ∀ {f' : Hom[ f ] z' x'} {q : a ∘ b ∘ f ≡ f}
- → a' ∘' b' ∘' f' ≡[ q ] f'
+ cancell'
+ : ∀ {f' : Hom[ f ] z' x'} {q : a ∘ b ∘ f ≡ f}
+ → a' ∘' b' ∘' f' ≡[ q ] f'
cancell' {f = f} {f' = f'} {q = q} = to-pathp $
hom[ q ] (a' ∘' b' ∘' f') ≡⟨ assoc[] ⟩
hom[ sym (assoc a b f) ∙ q ] ((a' ∘' b') ∘' f') ≡⟨ shiftl _ (eliml' p p') ⟩
f' ∎
- cancell[] : ∀ {f' : Hom[ f ] z' x'}
- → a' ∘' b' ∘' f' ≡[ cancell p ] f'
+ cancell[]
+ : ∀ {f' : Hom[ f ] z' x'}
+ → a' ∘' b' ∘' f' ≡[ cancell p ] f'
cancell[] = cancell'
- cancelr' : ∀ {f' : Hom[ f ] x' z'} {q : (f ∘ a) ∘ b ≡ f}
- → (f' ∘' a') ∘' b' ≡[ q ] f'
+ cancelr'
+ : ∀ {f' : Hom[ f ] x' z'} {q : (f ∘ a) ∘ b ≡ f}
+ → (f' ∘' a') ∘' b' ≡[ q ] f'
cancelr' {f = f} {f' = f'} {q = q} = to-pathp $
hom[ q ] ((f' ∘' a') ∘' b') ≡˘⟨ assoc[] ⟩
hom[ assoc f a b ∙ q ] (f' ∘' a' ∘' b') ≡⟨ shiftl _ (elimr' p p') ⟩
f' ∎
- cancelr[] : ∀ {f' : Hom[ f ] x' z'}
- → (f' ∘' a') ∘' b' ≡[ cancelr p ] f'
+ cancelr[]
+ : ∀ {f' : Hom[ f ] x' z'}
+ → (f' ∘' a') ∘' b' ≡[ cancelr p ] f'
cancelr[] = cancelr'
- cancel-inner' : ∀ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
+ cancel-inner'
+ : ∀ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
→ {q : (f ∘ a) ∘ (b ∘ g) ≡ f ∘ g}
→ (f' ∘' a') ∘' (b' ∘' g') ≡[ q ] f' ∘' g'
cancel-inner' = cast[] $ pullr[] _ cancell[]
- cancel-inner[] : ∀ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
+ cancel-inner[]
+ : ∀ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
→ (f' ∘' a') ∘' (b' ∘' g') ≡[ cancel-inner p ] f' ∘' g'
cancel-inner[] = cancel-inner'
- insertl' : ∀ {f' : Hom[ f ] z' x'} {q : f ≡ a ∘ b ∘ f }
- → f' ≡[ q ] a' ∘' b' ∘' f'
+ insertl'
+ : ∀ {f' : Hom[ f ] z' x'} {q : f ≡ a ∘ b ∘ f }
+ → f' ≡[ q ] a' ∘' b' ∘' f'
insertl' {f = f} {f' = f'} {q = q} i = cancell' {f' = f'} {q = sym q} (~ i)
- insertr' : ∀ {f' : Hom[ f ] x' z'} {q : f ≡ (f ∘ a) ∘ b }
- → f' ≡[ q ] (f' ∘' a') ∘' b'
+ insertr'
+ : ∀ {f' : Hom[ f ] x' z'} {q : f ≡ (f ∘ a) ∘ b }
+ → f' ≡[ q ] (f' ∘' a') ∘' b'
insertr' {f = f} {f' = f'} {q = q} i = cancelr' {f' = f'} {q = sym q} (~ i)
+
+ insertl[]
+ : ∀ {f' : Hom[ f ] z' x'}
+ → f' ≡[ insertl p ] a' ∘' b' ∘' f'
+ insertl[] = insertl'
+
+ insertr[]
+ : ∀ {f' : Hom[ f ] x' z'}
+ → f' ≡[ insertr p ] (f' ∘' a') ∘' b'
+ insertr[] = insertr'
+
+abstract
+ lswizzle'
+ : ∀ {f' : Hom[ f ] z' y'} {g' : Hom[ g ] x' z'} {h' : Hom[ h ] y' z'} {i' : Hom[ i ] x' y'}
+ → (p : g ≡ h ∘ i) (q : f ∘ h ≡ id) {r : f ∘ g ≡ i}
+ → g' ≡[ p ] h' ∘' i'
+ → f' ∘' h' ≡[ q ] id'
+ → f' ∘' g' ≡[ r ] i'
+ lswizzle' {f' = f'} p q p' q' =
+ cast[] (apd (λ i g' → f' ∘' g') p' ∙[] cancell[] q q')
+
+ lswizzle[]
+ : ∀ {f' : Hom[ f ] z' y'} {g' : Hom[ g ] x' z'} {h' : Hom[ h ] y' z'} {i' : Hom[ i ] x' y'}
+ → (p : g ≡ h ∘ i) (q : f ∘ h ≡ id)
+ → g' ≡[ p ] h' ∘' i'
+ → f' ∘' h' ≡[ q ] id'
+ → f' ∘' g' ≡[ lswizzle p q ] i'
+ lswizzle[] p q p' q' = lswizzle' p q p' q'
+
+ rswizzle'
+ : {f' : Hom[ f ] y' x'} {g' : Hom[ g ] x' z'} {h' : Hom[ h ] x' y'} {i' : Hom[ i ] y' z'}
+ → (p : g ≡ i ∘ h) (q : h ∘ f ≡ id) {r : g ∘ f ≡ i}
+ → g' ≡[ p ] i' ∘' h'
+ → h' ∘' f' ≡[ q ] id'
+ → g' ∘' f' ≡[ r ] i'
+ rswizzle' {f' = f'} p q p' q' =
+ cast[] (apd (λ i g' → g' ∘' f') p' ∙[] cancelr[] q q')
+
+ rswizzle[]
+ : {f' : Hom[ f ] y' x'} {g' : Hom[ g ] x' z'} {h' : Hom[ h ] x' y'} {i' : Hom[ i ] y' z'}
+ → (p : g ≡ i ∘ h) (q : h ∘ f ≡ id)
+ → g' ≡[ p ] i' ∘' h'
+ → h' ∘' f' ≡[ q ] id'
+ → g' ∘' f' ≡[ rswizzle p q ] i'
+ rswizzle[] {f' = f'} p q p' q' = rswizzle' p q p' q'
```
diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md
index dfa7e006e..6088df5f4 100644
--- a/src/Cat/Morphism.lagda.md
+++ b/src/Cat/Morphism.lagda.md
@@ -259,6 +259,17 @@ has-section→epic {f = f} f-sect g h p =
h ∎
```
+
+
+
A section that is also epic is a retract.
```agda
diff --git a/src/Cat/Reasoning.lagda.md b/src/Cat/Reasoning.lagda.md
index 6ac3b1b01..4794dcd7e 100644
--- a/src/Cat/Reasoning.lagda.md
+++ b/src/Cat/Reasoning.lagda.md
@@ -1,6 +1,6 @@