From ab4476134a9c05b6a7f106c04e20745d2c1bff4c Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sat, 13 Jan 2024 21:21:01 -0500 Subject: [PATCH 1/2] Left and right lifts along a displayed cat. --- src/Cat/Displayed/Base.lagda.md | 7 ++ src/Cat/Displayed/Instances/Lifting.lagda.md | 73 +++++++++++++++++++- 2 files changed, 79 insertions(+), 1 deletion(-) diff --git a/src/Cat/Displayed/Base.lagda.md b/src/Cat/Displayed/Base.lagda.md index 6c88ff16e..208fd3ac6 100644 --- a/src/Cat/Displayed/Base.lagda.md +++ b/src/Cat/Displayed/Base.lagda.md @@ -120,6 +120,13 @@ For convenience, we also introduce displayed analogues for equational chain reas → g' ≡[ q ] h' → f' ≡[ p ] g' → f' ≡[ p ∙ q ] h' ≡[-]⟨⟩-syntax f' p q' p' = p' ∙[] q' + ≡[]˘_ : ∀ {x} {y} {f} {g} + {p : f ≡ g} { x' : Ob[ x ] } { y' : Ob[ y ] } + {f' : Hom[ f ] x' y' } {g' : Hom[ g ] x' y' } + ( q : ( f' ≡[ p ] g' )) → (g' ≡[ (sym p) ] f') + + ≡[]˘ q = symP q + _≡[]˘⟨_⟩_ : ∀ {a b x y} {f g h : Hom a b} {p : g ≡ f} {q : g ≡ h} → (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y} → g' ≡[ p ] f' → g' ≡[ q ] h' → f' ≡[ sym p ∙ q ] h' diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index c69fd0bd5..277327699 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -3,16 +3,19 @@ open import Cat.Displayed.Cartesian open import Cat.Functor.Equivalence open import Cat.Instances.Functor +open import Cat.Instances.Product open import Cat.Displayed.Total open import Cat.Functor.Compose open import Cat.Displayed.Base open import Cat.Prelude +import 1Lab.Path + import Cat.Displayed.Reasoning +import Cat.Functor.Bifunctor as Bi import Cat.Reasoning ``` --> - ```agda module Cat.Displayed.Instances.Lifting where ``` @@ -22,6 +25,7 @@ module Cat.Displayed.Instances.Lifting where open Functor open _=>_ open Total-hom + ``` --> @@ -142,6 +146,73 @@ higher level of strictness than usual. ni .natural _ _ _ = id-comm ``` +The distinguished projection `πᶠ` has a canonical choice of lifting. +```agda +module _ {o ℓ o' ℓ'} + {B : Precategory o ℓ} + (E : Displayed B o' ℓ') + where + open Cat.Reasoning B + open Displayed E + open Cat.Displayed.Reasoning E + + πᶠ-lifting : Lifting E (πᶠ E) + πᶠ-lifting .Lifting.F₀' (_ , a)= a + πᶠ-lifting .Lifting.F₁' f = preserves f + πᶠ-lifting .Lifting.F-id' = refl + πᶠ-lifting .Lifting.F-∘' f g = refl +``` + +```agda +module Bifunctor {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} + {B : Precategory o₁ ℓ₁} + (E : Displayed B o₂ ℓ₂) + (C : Precategory o₃ ℓ₃) + (D : Precategory o₄ ℓ₄) + (F : Functor (C ×ᶜ D) B) + (F' : Lifting E F) + where + private + module C = Precategory C + module D = Precategory D + module E = Displayed E + module F' = Lifting F' + + sym_lemma_dep : ∀ {x} {y} {f} {g} + {p : f ≡ g} { x' : E.Ob[ x ] } { y' : E.Ob[ y ] } + {f' : E.Hom[ f ] x' y' } {g' : E.Hom[ g ] x' y' } + ( q : ( f' E.≡[ p ] g' )) → (g' E.≡[ (sym p) ] f') + + sym_lemma_dep q = symP q + + + Left : ∀ (d : D.Ob) → Lifting E (Bi.Left F d) + Left d .Lifting.F₀' c = Lifting.F₀' F' (c , d) + Left d .Lifting.F₁' f = Lifting.F₁' F' ( f , D.id ) + Left d .Lifting.F-id' = Lifting.F-id' F' + + Left d .Lifting.F-∘' f g = E.≡[]˘ + ((F'.F₁' (f , D.id) E.∘' + F'.F₁' (g , D.id)) + E.≡[]˘⟨ F'.F-∘' (f , D.id) (g , D.id) ⟩ + (ap (F' .Lifting.F₁') + (λ i → C._∘_ f g , D.idl (D.id) i) + E.∙[] refl)) + + Right : ∀ (c : C.Ob) → Lifting E (Bi.Right F c) + Right c .Lifting.F₀' d = Lifting.F₀' F' (c , d) + Right c .Lifting.F₁' f = Lifting.F₁' F' (C.id , f) + Right c .Lifting.F-id' = Lifting.F-id' F' + Right c .Lifting.F-∘' f g = E.≡[]˘ + ((F'.F₁' (C.id , f) E.∘' F'.F₁' (C.id , g)) + E.≡[]˘⟨ F'.F-∘' (C.id , f) (C.id , g) ⟩ + (ap (F' .Lifting.F₁') + (λ i → (C.idl (C.id) i , D._∘_ f g )) + E.∙[] refl + ) + ) +``` + ## Natural transformations between liftings As liftings are a reorganization of functors, it is reasonable to expect From f3d7152f8c700ead02102d7168276e914982d3a4 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sun, 28 Jan 2024 15:49:07 -0500 Subject: [PATCH 2/2] Fixed reviewer requests. --- src/Cat/Displayed/Base.lagda.md | 7 ---- src/Cat/Displayed/Instances/Lifting.lagda.md | 43 +++++++++----------- 2 files changed, 19 insertions(+), 31 deletions(-) diff --git a/src/Cat/Displayed/Base.lagda.md b/src/Cat/Displayed/Base.lagda.md index 208fd3ac6..6c88ff16e 100644 --- a/src/Cat/Displayed/Base.lagda.md +++ b/src/Cat/Displayed/Base.lagda.md @@ -120,13 +120,6 @@ For convenience, we also introduce displayed analogues for equational chain reas → g' ≡[ q ] h' → f' ≡[ p ] g' → f' ≡[ p ∙ q ] h' ≡[-]⟨⟩-syntax f' p q' p' = p' ∙[] q' - ≡[]˘_ : ∀ {x} {y} {f} {g} - {p : f ≡ g} { x' : Ob[ x ] } { y' : Ob[ y ] } - {f' : Hom[ f ] x' y' } {g' : Hom[ g ] x' y' } - ( q : ( f' ≡[ p ] g' )) → (g' ≡[ (sym p) ] f') - - ≡[]˘ q = symP q - _≡[]˘⟨_⟩_ : ∀ {a b x y} {f g h : Hom a b} {p : g ≡ f} {q : g ≡ h} → (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y} → g' ≡[ p ] f' → g' ≡[ q ] h' → f' ≡[ sym p ∙ q ] h' diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index 277327699..e18f8e611 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -9,8 +9,6 @@ open import Cat.Functor.Compose open import Cat.Displayed.Base open import Cat.Prelude -import 1Lab.Path - import Cat.Displayed.Reasoning import Cat.Functor.Bifunctor as Bi import Cat.Reasoning @@ -147,6 +145,11 @@ higher level of strictness than usual. ``` The distinguished projection `πᶠ` has a canonical choice of lifting. +Later, we will prove that for any functor $F$ valued in +$\cE$, $\pi^f$ has a canonical choice of lifting; however, this later +theorem cannot be applied here, as $\pi^f \circ \operatorname{id}_{\cE}$ +is not definitionally equal to $\pi^f$. + ```agda module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} @@ -157,12 +160,14 @@ module _ {o ℓ o' ℓ'} open Cat.Displayed.Reasoning E πᶠ-lifting : Lifting E (πᶠ E) - πᶠ-lifting .Lifting.F₀' (_ , a)= a + πᶠ-lifting .Lifting.F₀' (_ , a) = a πᶠ-lifting .Lifting.F₁' f = preserves f πᶠ-lifting .Lifting.F-id' = refl πᶠ-lifting .Lifting.F-∘' f g = refl ``` +Let $F: \cC\times \cD\to \cB$ be a functor and $\cE\liesover\cB$ a displayed category. Let $F' : \cC\times \cD\to \cE$ be a lift of $F$ along $F'$. We show that $F'(c-,)$ is a lift of $F(c,-)$ for any $c$, similarly $F'(-,d)$ is a lift of $F(-,d)$ for any $d$. + ```agda module Bifunctor {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} {B : Precategory o₁ ℓ₁} @@ -178,20 +183,12 @@ module Bifunctor {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} module E = Displayed E module F' = Lifting F' - sym_lemma_dep : ∀ {x} {y} {f} {g} - {p : f ≡ g} { x' : E.Ob[ x ] } { y' : E.Ob[ y ] } - {f' : E.Hom[ f ] x' y' } {g' : E.Hom[ g ] x' y' } - ( q : ( f' E.≡[ p ] g' )) → (g' E.≡[ (sym p) ] f') - - sym_lemma_dep q = symP q - - - Left : ∀ (d : D.Ob) → Lifting E (Bi.Left F d) - Left d .Lifting.F₀' c = Lifting.F₀' F' (c , d) - Left d .Lifting.F₁' f = Lifting.F₁' F' ( f , D.id ) - Left d .Lifting.F-id' = Lifting.F-id' F' + Left' : ∀ (d : D.Ob) → Lifting E (Bi.Left F d) + Left' d .Lifting.F₀' c = Lifting.F₀' F' (c , d) + Left' d .Lifting.F₁' f = Lifting.F₁' F' ( f , D.id ) + Left' d .Lifting.F-id' = Lifting.F-id' F' - Left d .Lifting.F-∘' f g = E.≡[]˘ + Left' d .Lifting.F-∘' f g = symP ((F'.F₁' (f , D.id) E.∘' F'.F₁' (g , D.id)) E.≡[]˘⟨ F'.F-∘' (f , D.id) (g , D.id) ⟩ @@ -199,18 +196,16 @@ module Bifunctor {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} (λ i → C._∘_ f g , D.idl (D.id) i) E.∙[] refl)) - Right : ∀ (c : C.Ob) → Lifting E (Bi.Right F c) - Right c .Lifting.F₀' d = Lifting.F₀' F' (c , d) - Right c .Lifting.F₁' f = Lifting.F₁' F' (C.id , f) - Right c .Lifting.F-id' = Lifting.F-id' F' - Right c .Lifting.F-∘' f g = E.≡[]˘ + Right' : ∀ (c : C.Ob) → Lifting E (Bi.Right F c) + Right' c .Lifting.F₀' d = Lifting.F₀' F' (c , d) + Right' c .Lifting.F₁' f = Lifting.F₁' F' (C.id , f) + Right' c .Lifting.F-id' = Lifting.F-id' F' + Right' c .Lifting.F-∘' f g = symP ((F'.F₁' (C.id , f) E.∘' F'.F₁' (C.id , g)) E.≡[]˘⟨ F'.F-∘' (C.id , f) (C.id , g) ⟩ (ap (F' .Lifting.F₁') (λ i → (C.idl (C.id) i , D._∘_ f g )) - E.∙[] refl - ) - ) + E.∙[] refl)) ``` ## Natural transformations between liftings