{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- Lemma 3.14: triangle strictification.  For a full cofibration i : Φ ↪ Ψ,
-- fibrant Y, and a triangle f, g commuting weakly by H : Πφ. f φ = g (i φ),
-- there is h : Ψ → Y with h ∘ i =ᵉ f (`top-strict`), a globe
-- G : Πψ. h ψ = g ψ, and G ∘ i =ᵉ H (`globe-restricts-strictly`), the last
-- stated as a transport along `top-strict`, which in the paper is invisible
-- because there h ∘ i holds judgmentally.  The globe cannot be made strict:
-- h =ᵉ g would force g ∘ i =ᵉ f (`no-strict-globe`).
--
-- This is the homotopy extension property for the constant family Y, so we
-- instantiate `HEP-holds` of Extension.RS411, which keeps the strict boundary
-- of the extended homotopy that RS410 does not export.
--------------------------------------------------------------------------------

module Extension.TriangleStrictification where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RS411 using (HEP-holds)
open import Extension.RelFunext using (satisfies-rel-funext)

private
  variable
    ℓ ℓΦ ℓΨ : Level

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (triv : satisfies-rel-funext cof)
         (Y : UU ℓ)
         (f : Φ → C Y) (g : Ψ → C Y)
         (H : (φ : Φ) → Id (ic (f φ)) (ic (g (i φ))))
       where

  private
    -- RS 4.10 for the constant family Y over Ψ, with b ≔ g, a ≔ f, e ≔ H
    hepInst :
      Σᵉ (Ext i (λ _ → C Y) f) (λ a' →
        Ext i (λ ψ → C (Id (ic (ext-app a' ψ)) (ic (g ψ))))
              (λ φ → exo-tr (λ v → C (Id (ic v) (ic (g (i φ)))))
                            (exo-inv (ext-bdry a' φ)) (c (H φ))))
    hepInst = HEP-holds cof triv (λ _ → Y) g f H

  -- h ≔ a', bundled: an element of the extension type of f along i, i.e.
  -- a total map with strict top triangle.
  h-ext : Ext i (λ _ → C Y) f
  h-ext = pr1ᵉ hepInst

  h : Ψ → C Y
  h = ext-app h-ext

  -- the top triangle commutes strictly:  h ∘ i =ᵉ f
  top-strict : (λ φ → h (i φ)) =ᵉ f
  top-strict = pr2ᵉ h-ext

  -- G ≔ e', the weak globe between h and g
  G : (ψ : Ψ) → Id (ic (h ψ)) (ic (g ψ))
  G ψ = ic (ext-app (pr2ᵉ hepInst) ψ)

  -- G, bundled: an element of the extension type over (the transported) H,
  -- RS-style, the globe lives in an extension type with boundary H.
  globe-ext : Ext i (λ ψ → C (Id (ic (h ψ)) (ic (g ψ))))
                    (λ φ → exo-tr (λ v → C (Id (ic v) (ic (g (i φ)))))
                                  (exo-inv (happlyᵉ top-strict φ)) (c (H φ)))
  globe-ext = pr2ᵉ hepInst

  -- the restriction of the globe to Φ is strictly the original filler:
  -- G ∘ i =ᵉ H, well-typed via transport along (the pointwise) top-strict.
  globe-restricts-strictly :
    (λ φ → c (G (i φ)))
    =ᵉ (λ φ → exo-tr (λ v → C (Id (ic v) (ic (g (i φ)))))
                     (exo-inv (happlyᵉ top-strict φ)) (c (H φ)))
  globe-restricts-strictly = pr2ᵉ globe-ext

  -- the paper's closing remark: the globe itself cannot be made strict in
  -- general, for any total map h' with strict top triangle, a strict globe
  -- h' =ᵉ g would force the original triangle to commute strictly.
  no-strict-globe : (h' : Ψ → C Y)
                  → ((λ φ → h' (i φ)) =ᵉ f)
                  → h' =ᵉ g
                  → (λ φ → g (i φ)) =ᵉ f
  no-strict-globe h' topEq E =
    exo-concat (exo-ap (λ k → (λ φ → k (i φ))) (exo-inv E)) topEq

{- References:

  [RS]         Emily Riehl and Michael Shulman.  A type theory for synthetic
               ∞-categories.  Higher Structures 1(1):147-224, 2017.
               doi:10.21136/hs.2017.06

-}