From 24ad1e4193d1ac116afa15d08a4a37676f5645f0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 11:31:14 -0400 Subject: [PATCH 01/17] chore: formatting pass on Cat.Displayed.Reasoning, new combinators --- src/Cat/Displayed/Reasoning.lagda.md | 212 +++++++++++++++------------ 1 file changed, 122 insertions(+), 90 deletions(-) diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index 0578544ae..c897372bf 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,29 +601,34 @@ 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[] @@ -617,11 +637,23 @@ module _ {a' : Hom[ a ] y' x'} {b' : Hom[ b ] x' y'} → (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' ``` From a69afa56c80790a8fd32f086db64d3046a103100 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 11:50:38 -0400 Subject: [PATCH 02/17] chore: reasoning with sections/retracts --- src/Cat/Morphism.lagda.md | 23 ++++++++++++++++++++++- src/Cat/Reasoning.lagda.md | 34 ++++++++++++++++++++++++++++++++-- 2 files changed, 54 insertions(+), 3 deletions(-) diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index 3d5c01827..98924a9c9 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 af45fbb0a..3a9b11200 100644 --- a/src/Cat/Reasoning.lagda.md +++ b/src/Cat/Reasoning.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index c897372bf..90d1763b8 100644 --- a/src/Cat/Displayed/Reasoning.lagda.md +++ b/src/Cat/Displayed/Reasoning.lagda.md @@ -633,7 +633,8 @@ module _ {a' : Hom[ a ] y' x'} {b' : Hom[ b ] x' y'} → (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' @@ -656,4 +657,39 @@ module _ {a' : Hom[ a ] y' x'} {b' : Hom[ b ] x' y'} : ∀ {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' ``` From 897dfb402f3c68215f5c4633d37dd7901ac03156 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 12:15:24 -0400 Subject: [PATCH 04/17] def: jointly weak monomorphic families --- src/Cat/Displayed/Morphism.lagda.md | 112 +++++++++++++++++++++++++++- 1 file changed, 110 insertions(+), 2 deletions(-) diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index 59456bd62..230d11a39 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"} 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 @@ -109,6 +114,109 @@ 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 = + g'-weak-monic h' k' $ f'-weak-monic (g' ∘' h') (g' ∘' k') $ 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 = + cast[] $ f'-monic g' h' refl 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 = + fg-weak-monic h' k' $ extendr' refl 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' +``` + +### 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 : Hom x a} + → (g' g'' : Hom[ g ] x' a') + → (∀ ix → fᵢ' ix ∘' g' ≡ fᵢ' ix ∘' g'') + → g' ≡ g'' +``` + +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 = + g'-joint-mono h' h'' $ + fᵢ'-joint-mono (g' ∘' h') (g' ∘' h'') λ 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 = + fᵢ'-joint-mono h' h'' λ _ → extendr' refl p +``` + ## Epis Displayed [epimorphisms] are defined in a similar fashion. From 80b919d75e0df0163fb2126bd74e1cded8ea3398 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 13:11:01 -0400 Subject: [PATCH 05/17] refactor: generalize type of weak monos --- src/Cat/Displayed/Morphism.lagda.md | 67 +++++++++++++++-------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index 230d11a39..fdc1c8dfa 100644 --- a/src/Cat/Displayed/Morphism.lagda.md +++ b/src/Cat/Displayed/Morphism.lagda.md @@ -89,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 ]) @@ -122,10 +121,12 @@ 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 = - g'-weak-monic h' k' $ f'-weak-monic (g' ∘' h') (g' ∘' k') $ cast[] $ +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') ∘' h' ≡[]⟨ p' ⟩ (f' ∘' g') ∘' k' ≡[]˘⟨ assoc' f' g' k' ⟩ f' ∘' g' ∘' k' ∎ @@ -133,8 +134,8 @@ 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 = - cast[] $ f'-monic g' h' refl p +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'$. @@ -143,8 +144,8 @@ If $f' \circ g'$ is weakly monic, then so is $g'$. 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 = - fg-weak-monic h' k' $ extendr' refl p +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]]. @@ -158,7 +159,7 @@ weak-monic-postcomp-embedding → 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' + injective→is-embedding (hlevel 2) (f' ∘'_) λ {g'} {h'} → f'-weak-monic g' h' refl ``` ### Jointly weak monos @@ -178,10 +179,11 @@ is-jointly-weak-monic → (fᵢ' : (ix : Ix) → Hom[ fᵢ ix ] a' (bᵢ' ix)) → Type _ is-jointly-weak-monic {a = a} {a' = a'} {fᵢ = fᵢ} fᵢ' = - ∀ {x x'} {g : Hom x a} - → (g' g'' : Hom[ g ] x' a') - → (∀ ix → fᵢ' ix ∘' g' ≡ fᵢ' ix ∘' g'') - → g' ≡ g'' + ∀ {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 @@ -194,12 +196,12 @@ jointly-weak-monic-∘ → 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 = - g'-joint-mono h' h'' $ - fᵢ'-joint-mono (g' ∘' h') (g' ∘' h'') λ ix → +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' ≡[]⟨ p' ix ⟩ (fᵢ' ix ∘' g') ∘' h'' ≡[]˘⟨ assoc' (fᵢ' ix) g' h'' ⟩ fᵢ' ix ∘' g' ∘' h'' ∎ ``` @@ -213,8 +215,8 @@ jointly-weak-monic-cancell → {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 = - fᵢ'-joint-mono h' h'' λ _ → extendr' refl p +jointly-weak-monic-cancell fᵢ'-joint-mono h' h'' p p' = + fᵢ'-joint-mono h' h'' p λ _ → extendr' (ap₂ _∘_ refl p) p' ``` ## Epis @@ -266,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 ]) From e2cd6298f2cefd4ab722f1ca8ffa6cfbba4488dd Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 13:11:26 -0400 Subject: [PATCH 06/17] def: use weak monos in cancellation property --- src/Cat/Displayed/Cartesian.lagda.md | 122 ++++++++++++++++++--------- 1 file changed, 81 insertions(+), 41 deletions(-) diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index 8bdd4f235..5fe5fbd8e 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -217,6 +217,36 @@ is-cartesian-is-prop {f' = f'} cart cart' = worker where ``` + + We also provide a bundled form of cartesian morphisms. ```agda @@ -360,10 +390,8 @@ cartesian→weak-monic → ∀ {x' y'} {f' : Hom[ f ] x' y'} → is-cartesian f f' → is-weak-monic f' -cartesian→weak-monic {f' = f'} f-cart g' g'' p = - g' ≡⟨ unique g' p ⟩ - universal _ (f' ∘' g'') ≡˘⟨ unique g'' refl ⟩ - g'' ∎ +cartesian→weak-monic {f = f} {f' = f'} f-cart g' g'' p p' = + uniquep₂ (ap (f ∘_) p) p refl g' g'' p' refl where open is-cartesian f-cart ``` @@ -438,28 +466,29 @@ cartesian-domain-unique cartesian-domain-unique {f' = f'} {f'' = f''} f'-cart f''-cart = make-iso[ id-iso ] to* from* invl* invr* where - open is-cartesian + module f' = is-cartesian f'-cart + module f'' = is-cartesian f''-cart - to* = universal' f''-cart (B .Precategory.idr _) f' - from* = universal' f'-cart (B .Precategory.idr _) f'' + to* = f''.universalv f' + from* = f'.universalv f'' invl* : to* ∘' from* ≡[ idl id ] id' - invl* = to-pathp⁻ $ cartesian→weak-monic f''-cart _ _ $ - f'' ∘' to* ∘' from* ≡⟨ shiftr (assoc _ _ _) (pulll' _ (f''-cart .commutes _ _)) ⟩ - hom[] (hom[] f' ∘' from*) ≡⟨ smashl _ _ ⟩ - hom[] (f' ∘' from*) ≡⟨ (hom[]⟩⟨ f'-cart .commutes _ _) ∙ hom[]-∙ _ _ ⟩ - hom[] f'' ≡⟨ weave _ (sym $ idr _) (ap (_ ∘_) (sym $ idl _)) (symP $ idr' f'') ⟩ - hom[] (f'' ∘' id') ≡˘⟨ whisker-r _ ⟩ - f'' ∘' hom[] id' ∎ + invl* = + cartesian→weak-monic f''-cart (to* ∘' from*) id' (idl id) $ + cast[] $ + f'' ∘' to* ∘' from* ≡[]⟨ pulll[] _ (f''.commutesv f') ⟩ + f' ∘' from* ≡[]⟨ f'.commutesv f'' ⟩ + f'' ≡[]˘⟨ idr' f'' ⟩ + f'' ∘' id' ∎ invr* : from* ∘' to* ≡[ idl id ] id' - invr* = to-pathp⁻ $ cartesian→weak-monic f'-cart _ _ $ - f' ∘' from* ∘' to* ≡⟨ shiftr (assoc _ _ _) (pulll' _ (f'-cart .commutes _ _)) ⟩ - hom[] (hom[] f'' ∘' to*) ≡⟨ smashl _ _ ⟩ - hom[] (f'' ∘' to*) ≡⟨ (hom[]⟩⟨ f''-cart .commutes _ _) ∙ hom[]-∙ _ _ ⟩ - hom[] f' ≡⟨ weave _ (sym $ idr _) (ap (_ ∘_) (sym $ idl _)) (symP $ idr' f') ⟩ - hom[] (f' ∘' id') ≡˘⟨ whisker-r _ ⟩ - f' ∘' hom[] id' ∎ + invr* = + cartesian→weak-monic f'-cart (from* ∘' to*) id' (idl id) $ + cast[] $ + f' ∘' from* ∘' to* ≡[]⟨ pulll[] _ (f'.commutesv f'') ⟩ + f'' ∘' to* ≡[]⟨ f''.commutesv f' ⟩ + f' ≡[]˘⟨ idr' f' ⟩ + f' ∘' id' ∎ ``` Cartesian morphisms are also stable under vertical retractions. @@ -503,28 +532,45 @@ cartesian-vertical-retraction-stable {f' = f'} {f''} {ϕ} f-cart ϕ-sect factor h' ∎ ``` -We also have the following extremely useful pasting lemma, which -generalizes the [[pasting law for pullbacks]]. +If $f' \circ g'$ is cartesian and $f'$ is a [[weak monomorphism]], +then $g'$ is cartesian. ```agda -cartesian-pasting +cartesian-weak-monic-cancell : ∀ {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-cartesian f f' + → is-weak-monic f' → is-cartesian (f ∘ g) (f' ∘' g') → is-cartesian g g' -cartesian-pasting {f = f} {g = g} {f' = f'} {g' = g'} f-cart fg-cart = g-cart where +cartesian-weak-monic-cancell {f = f} {g = g} {f' = f'} {g' = g'} f-weak-mono fg-cart = g-cart where + module fg = is-cartesian fg-cart open is-cartesian g-cart : is-cartesian g g' g-cart .universal m h' = - universal' fg-cart (sym (assoc _ _ _)) (f' ∘' h') + fg.universal' (sym (assoc f g m)) (f' ∘' h') g-cart .commutes m h' = - g' ∘' universal' fg-cart (sym (assoc _ _ _)) (f' ∘' h') ≡⟨ f-cart .unique _ (from-pathp⁻ (assoc' _ _ _) ∙ from-pathp (commutesp fg-cart _ _)) ⟩ - f-cart .universal _ (f' ∘' h') ≡˘⟨ f-cart .unique h' refl ⟩ - h' ∎ - g-cart .unique {m = m} {h' = h'} m' p = - uniquep fg-cart (sym (assoc _ _ _)) refl (sym (assoc _ _ _)) m' (pullr' refl p) + f-weak-mono (g' ∘' fg.universal' _ (f' ∘' h')) h' refl $ + cast[] $ + f' ∘' g' ∘' fg.universal' _ (f' ∘' h') ≡[]⟨ assoc' _ _ _ ⟩ + (f' ∘' g') ∘' fg.universal' _ (f' ∘' h') ≡[]⟨ fg.commutesp (sym (assoc f g m)) (f' ∘' h') ⟩ + f' ∘' h' ∎ + g-cart .unique {m = m} m' p = + fg.uniquep (sym (assoc f g m)) refl (sym (assoc f g m)) m' (pullr' refl p) +``` + +As a corollary, we get the following useful pasting lemma, which +generalizes the [[pasting law for pullbacks]]. + +```agda +cartesian-cancell + : ∀ {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-cartesian f f' + → is-cartesian (f ∘ g) (f' ∘' g') + → is-cartesian g g' +cartesian-cancell f-cart fg-cart = + cartesian-weak-monic-cancell (cartesian→weak-monic f-cart) fg-cart ``` We can prove a similar fact for bundled cartesian morphisms. @@ -543,15 +589,9 @@ cart-paste {x' = x'} {y' = y'} {f = f} {g = g} f' fg' = g' where g' : Cartesian-morphism g x' y' g' .hom' = f'.universal g (fg' .hom') - g' .cartesian .universal m h' = - fg'.universal' (sym (assoc _ _ _)) (f' .hom' ∘' h') - g' .cartesian .commutes m h' = - f'.uniquep₂ _ _ (assoc _ _ _) _ _ - (pulll[] _ (f'.commutes _ _) ∙[] fg'.commutes _ _) - (to-pathp refl) - g' .cartesian .unique m' p = - fg'.uniquep _ refl (sym (assoc _ _ _)) m' - (ap (_∘' m') (symP (f'.commutes _ _)) ∙[] pullr[] _ p) + g' .cartesian = + cartesian-cancell (f' .cartesian) $ + subst-is-cartesian refl (sym (f'.commutes g (fg' .hom'))) (fg' .cartesian) ``` If a morphism is both vertical and cartesian, then it must be an From b49878fdf8ac22c0d959a9a1f6ac5562a887e666 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 13:11:46 -0400 Subject: [PATCH 07/17] fix: update uses of weak monos --- src/Cat/Displayed/Cartesian/Indexing.lagda.md | 2 +- src/Cat/Displayed/Cocartesian.lagda.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 312355410..b8d5ff329 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -148,7 +148,7 @@ base along a composite. : ∀ {a b c} {f : Hom b c} {g : Hom a b} {x y : Ob[ c ]} (f' : Hom[ id ] x y) → rebase g (rebase f f') Fib.∘ ^*-comp-to ≡ ^*-comp-to Fib.∘ rebase (f ∘ g) f' ^*-comp-to-natural {f = f} {g = g} f' = - ap hom[] $ cartesian→weak-monic E (π*.cartesian) _ _ $ cast[] $ + ap hom[] $ cartesian→weak-monic E (π*.cartesian) _ _ _ $ cast[] $ pulll[] _ (π*.commutesp id-comm _) ∙[] pullr[] _ (π*.commutesv _) ∙[] π*.uniquep₂ _ id-comm-sym _ _ _ 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) From 7a80d55e2edce0da7543d355dff99af953fc8587 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 13:51:39 -0400 Subject: [PATCH 08/17] chore: improve proofs for cartesian maps --- src/Cat/Displayed/Cartesian.lagda.md | 146 +++++++++++++-------------- 1 file changed, 71 insertions(+), 75 deletions(-) diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index 5fe5fbd8e..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$, @@ -302,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} @@ -351,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') ∎ ``` -# 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 From ac5633ee9009d3d3d6449c1764604660a6be0c36 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 21:52:57 -0400 Subject: [PATCH 10/17] def: joint cartesian morphisms --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 607 +++++++++++++++++++++ 1 file changed, 607 insertions(+) create mode 100644 src/Cat/Displayed/Cartesian/Joint.lagda.md diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md new file mode 100644 index 000000000..d685f0dbd --- /dev/null +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -0,0 +1,607 @@ +--- +description: | + Joint cartesian families +--- + +```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]] 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ᵢ +``` + + + + + +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$ are +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. + +## 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 discrete 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 discrete spaces. + +```agda +empty-jointly-cartesian→discrete + : ∀ {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→discrete ¬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 +``` + +## Closure properties of jointly cartesian families + +Jointly cartesian families are closed under precomposition with [[cartesian maps]]. + +```agda +jointly-cartesian-cartesian-∘ + : is-jointly-cartesian uᵢ fᵢ + → is-cartesian v g + → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g) +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) +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 [[weakly monic family]]. + +```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} \circ g_{i}$ is jointly cartesian, and each $f_{i}$ is +[[weakly monic]], then $g_{i}$ must be jointly cartesian. + +```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-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)) +``` + +We can sharpen the previous result when $g_{i}$ is a constant family. +In particular, if $f_{i} \circ g$ is jointly cartesian, and $f_{i}$ is a +[[jointly weak monic family]], then $g$ must be cartesian. + +```agda +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-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) +``` + +As corollaries, we get a pair of cancellation properties for jointly +cartesian families. + +```agda +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-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 + : is-jointly-cartesian uᵢ fᵢ + → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g) + → is-cartesian v g +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 +``` + +## 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 discrete +spaces arising from lifts of empty families. + +```agda + opaque + Disc* : ∀ (x : Ob) → Ob[ x ] + Disc* x = ⋂* (Lift _ ⊥) {yᵢ = λ ()} (λ ()) (λ ()) + + disc* + : ∀ {x y : Ob} + → (u : Hom x y) (x' : Ob[ x ]) + → Hom[ u ] x' (Disc* y) + disc* u x' = π*.universal u (λ ()) + + disc*-unique + : ∀ {x y : Ob} + → {u : Hom x y} {x' : Ob[ x ]} + → (other : Hom[ u ] x' (Disc* y)) + → other ≡ disc* u x' + disc*-unique other = π*.unique other (λ ()) +``` From 3a2fd2af85e0597dce57593569965e3ae95580ee Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 22:18:29 -0400 Subject: [PATCH 11/17] prose: nomenclature warning for jointly cartesian families --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 9 ++++++-- src/bibliography.bibtex | 25 +++++++++++++++++++++- 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index d685f0dbd..e3ce6b2c5 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -36,10 +36,8 @@ open Displayed E 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]] map. - ::: - ```agda record is-jointly-cartesian {ℓi} {Ix : Type ℓi} @@ -169,6 +167,13 @@ private variable ``` --> +::: 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]] diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex index 456148fb1..7eb47c2b0 100644 --- a/src/bibliography.bibtex +++ b/src/bibliography.bibtex @@ -271,4 +271,27 @@ journal={Log. Methods Comput. Sci.}, author={Kraus, Nicolai and Escardó, M. and Coquand, T. and Altenkirch, Thorsten}, year={2016}, language={en} -} \ No newline at end of file +} + +@book{Adamek-Herrlich-Strecker:2004, + address={Mineola, NY}, + series={Dover books on mathematics}, + title={Abstract and concrete categories: the joy of cats}, + ISBN={978-0-486-46934-8}, + publisher={Dover Publ}, + author={Adámek, Jiří and Herrlich, Horst and Strecker, George E.}, + year={2004}, + collection={Dover books on mathematics}, + language={eng} +} + +@article{Dubuc-Espanol:2006, + title={Topological functors as familiarly-fibrations}, + url={http://arxiv.org/abs/math/0611701}, + DOI={10.48550/arXiv.math/0611701}, + note={arXiv:math/0611701}, + number={arXiv:math/0611701}, + author={Dubuc, Eduardo J. and Español, Luis}, + year={2006}, + month=nov +} From 25635d0965d2bc2cf1063b96fd61a94b0b8a6980 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 22:28:56 -0400 Subject: [PATCH 12/17] fix: meant to type \; --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index e3ce6b2c5..a383e4baf 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -212,7 +212,7 @@ cartesian→jointly-cartesian {u = u} {f = f} ix-contr f-cart = f-joint-cart whe f.unique other (p (ix-contr .centre)) ``` -Conversely, if the constant family $\lambda i\. f$ is a jointly cartesian +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 From 17e9fba1544bc669699d9db64a7a67947c2a2fae Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 1 Apr 2025 22:32:03 -0400 Subject: [PATCH 13/17] prose: fix link targets --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 4 ++-- src/Cat/Displayed/Morphism.lagda.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index a383e4baf..2717d968c 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -35,7 +35,7 @@ open Displayed E :::{.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]] map. +property of a [[cartesian|cartesian-morphism]] map. ::: ```agda @@ -369,7 +369,7 @@ jointly-cartesian-vertical-retraction-stable ## Cancellation properties of jointly cartesian families -Every jointly cartesian family is a [[weakly monic family]]. +Every jointly cartesian family is a [[jointly weak monic family]]. ```agda jointly-cartesian→jointly-weak-monic diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index fdc1c8dfa..d2be91a54 100644 --- a/src/Cat/Displayed/Morphism.lagda.md +++ b/src/Cat/Displayed/Morphism.lagda.md @@ -76,7 +76,7 @@ record _↪[_]_ open _↪[_]_ public ``` -## Weak monos {defines="weak-monomorphism"} +## 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 From 9c5ada0426da5c3de79a57824e0c71f0dcf5dd25 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 2 Apr 2025 13:49:14 -0400 Subject: [PATCH 14/17] def: more general composition and cancellation properties --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 221 +++++++++++++++++---- 1 file changed, 185 insertions(+), 36 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index 2717d968c..fbbbe6a85 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -154,16 +154,19 @@ such that $f_{i} \circ \langle v , h_{i} \rangle = h_{i}$. @@ -252,13 +255,79 @@ empty-jointly-cartesian→discrete ¬ix fᵢ-cart v x' = ## Closure properties of jointly cartesian families -Jointly cartesian families are closed under precomposition with [[cartesian maps]]. +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 @@ -278,6 +347,7 @@ jointly-cartesian-cartesian-∘ {uᵢ = uᵢ} {fᵢ = fᵢ} {v = v} {g = g} fᵢ 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}$ @@ -288,6 +358,12 @@ 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) @@ -307,6 +383,7 @@ pointwise-cartesian-jointly-cartesian-∘ 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. @@ -334,7 +411,8 @@ so we omit the details. ```agda jointly-cartesian-vertical-retraction-stable - {uᵢ = uᵢ} {fᵢ = fᵢ} {fᵢ' = fᵢ'} {ϕ = ϕ} fᵢ-cart ϕ-sect factor = fᵢ'-cart + {uᵢ = uᵢ} {fᵢ = fᵢ} {fᵢ' = fᵢ'} {ϕ = ϕ} fᵢ-cart ϕ-sect factor + = fᵢ'-cart where module fᵢ = is-jointly-cartesian fᵢ-cart module ϕ = has-section[_] ϕ-sect @@ -369,7 +447,9 @@ jointly-cartesian-vertical-retraction-stable ## Cancellation properties of jointly cartesian families -Every jointly cartesian family is a [[jointly weak monic family]]. +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 @@ -380,16 +460,105 @@ jointly-cartesian→jointly-weak-monic {fᵢ = fᵢ} fᵢ-cart {g = w} g h p p' where module fᵢ = is-jointly-cartesian fᵢ-cart ``` -If $f_{i} \circ g_{i}$ is jointly cartesian, and each $f_{i}$ is -[[weakly monic]], then $g_{i}$ must be jointly cartesian. +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 + {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 @@ -406,19 +575,10 @@ jointly-cartesian-pointwise-weak-monic-cancell fᵢ ix ∘' hᵢ ix ∎ gᵢ-cart .unique other p = fᵢ∘gᵢ.uniquep _ _ _ other (λ ix → pullr[] _ (p ix)) -``` - -We can sharpen the previous result when $g_{i}$ is a constant family. -In particular, if $f_{i} \circ g$ is jointly cartesian, and $f_{i}$ is a -[[jointly weak monic family]], then $g$ must be cartesian. -```agda 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-jointly-weak-monic-cancell - {uᵢ = uᵢ} {fᵢ = fᵢ} {v = v} {g = g} fᵢ-weak-monic fᵢ∘g-cart = g-cart + {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 @@ -434,30 +594,19 @@ jointly-cartesian-jointly-weak-monic-cancell fᵢ ix ∘' h ∎ g-cart .unique other p = fᵢ∘g.uniquep _ _ _ other (λ ix → pullr[] _ p) -``` - -As corollaries, we get a pair of cancellation properties for jointly -cartesian families. -```agda -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-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 - : is-jointly-cartesian uᵢ fᵢ - → is-jointly-cartesian (λ ix → uᵢ ix ∘ v) (λ ix → fᵢ ix ∘' g) - → is-cartesian v g 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 + ``` +
## Universal properties @@ -565,7 +714,7 @@ cartesian fibrations, but is a bit verbose. where open Joint-cartesian-lift (fib Ix uᵢ yᵢ') using () - renaming (x' to ⋂*) + renaming (x' to ∏*) public module _ @@ -595,7 +744,7 @@ spaces arising from lifts of empty families. ```agda opaque Disc* : ∀ (x : Ob) → Ob[ x ] - Disc* x = ⋂* (Lift _ ⊥) {yᵢ = λ ()} (λ ()) (λ ()) + Disc* x = ∏* (Lift _ ⊥) {yᵢ = λ ()} (λ ()) (λ ()) disc* : ∀ {x y : Ob} From 5777528986acfb8d05e22bd2a03ce35b423fa790 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 2 Apr 2025 17:01:05 -0400 Subject: [PATCH 15/17] def: more results, minor fixes --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 139 ++++++++++++++++++--- 1 file changed, 122 insertions(+), 17 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index fbbbe6a85..2744ebc90 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -154,8 +154,8 @@ such that $f_{i} \circ \langle v , h_{i} \rangle = h_{i}$. @@ -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. From 35ddb0476b71efafd2d4f88b737a2607e10b176b Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 8 Apr 2025 11:31:39 -0400 Subject: [PATCH 17/17] prose: fix typos --- src/Cat/Displayed/Cartesian/Joint.lagda.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index 2b4a6f8de..3c956586b 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -243,7 +243,7 @@ const-jointly-cartesian→cartesian {Ix = Ix} {u = u} {f = f} ∥ix∥ f-joint-c 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 discrete spaces. +category of topological spaces, such maps are precisely the codiscrete spaces. ```agda empty-jointly-cartesian→codiscrete @@ -669,9 +669,10 @@ $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, 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$ -thin. We can then easily extend the family $f_{i}$ along an arbitrary map +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