Left and right lifts along a displayed cat.

src/Cat/Displayed/Instances/Lifting.lagda.md

@@ -3,16 +3,17 @@
 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 Cat.Displayed.Reasoning
+import Cat.Functor.Bifunctor as Bi
 import Cat.Reasoning
 ```
 -->
-
 ```agda
 module Cat.Displayed.Instances.Lifting where
 ```
@@ -22,6 +23,7 @@ module Cat.Displayed.Instances.Lifting where
 open Functor
 open _=>_
 open Total-hom
+
 ```
 -->
 
@@ -142,6 +144,70 @@ higher level of strictness than usual.
     ni .natural _ _ _ = id-comm
 ```
 
+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 ℓ}
+  (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
+```
+
+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₁ ℓ₁}
+  (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'
+
+  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 = symP
+                   ((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 = 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))
+```
+
 ## Natural transformations between liftings
 
 As liftings are a reorganization of functors, it is reasonable to expect