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

--------------------------------------------------------------------------------
-- RS 4.5 : union of cofibrations  (Lemma 3.8 of the paper).
--
-- The paper assumes the cofibration class is closed under binary meets, so
-- that  Φ∧Ψ ↪ Φ  is a cofibration and  Φ∨Ψ  is the pushout of
-- Φ ←– Φ∧Ψ –→ Ψ.  We parametrize accordingly: an exo-type M ("Φ∧Ψ") with two
-- maps  u : M → Φ,  v : M → Ψ,  and an assumed outer pushout P ("Φ∨Ψ") of the
-- span  Φ ←u– M –v→ Ψ  in the sense of Extension.ExoPushout (outer pushouts
-- do not exist in plain 2LTT; the paper takes them as input).  Then, for a
-- family A over P and a total boundary  a : Πψ.A(inrᴾ ψ)  on the Ψ-leg,
--
--     Ext_{Ψ ↪ Φ∨Ψ}(A , a)  ≅  Ext_{Φ∧Ψ ↪ Φ}(A|_Φ , a|_{Φ∧Ψ}) ,
--
-- where  a|_{Φ∧Ψ}  is a restricted along v and pulled back across the glue.
-- Pure UMP bookkeeping, following the paper's proof: a section over Φ∨Ψ is a
-- pair of sections over Φ and Ψ agreeing on Φ∧Ψ; fixing the Ψ-component to a
-- leaves a section over Φ agreeing with a on Φ∧Ψ.  The maps are restriction
-- and the copairing (the eliminator), inverse by β/η.
--
-- As everywhere in this development, we work with a general exo family
-- A : P → UUᵉ and arbitrary exo-maps u, v (no cofibrancy/fibrancy is used);
-- the paper's fibrant statement is the special case A := C ∘ A₀.  Note the
-- iso itself does not need  Φ∧Ψ ↪ Φ  to be a cofibration, that hypothesis
-- only matters for the well-formedness discussion in the paper (whether the
-- right-hand side is an extension type along a cofibration).
--------------------------------------------------------------------------------

module Extension.RS45 where

open import Extension.Prelude
open import Extension.Core
open import Extension.ExoPushout

private
  variable
    ℓM ℓΦ ℓΨ ℓP ℓA : Level

module _ {M : UUᵉ ℓM} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
         (u : M → Φ) (v : M → Ψ)
         {P : UUᵉ ℓP} (inlᴾ : Φ → P) (inrᴾ : Ψ → P)
         (glueᴾ : (m : M) → inlᴾ (u m) =ᵉ inrᴾ (v m))
         (A : P → UUᵉ ℓA) (a : (ψ : Ψ) → A (inrᴾ ψ))
       where

  -- a|_{Φ∧Ψ} : the boundary a, restricted along v to the meet and transported
  -- backwards across the glue so that it lives over the Φ-leg.
  a∧ : (m : M) → A (inlᴾ (u m))
  a∧ m = exo-tr A (exo-inv (glueᴾ m)) (a (v m))

  module _ (po : is-exo-pushout u v inlᴾ inrᴾ glueᴾ ℓA) where

    RS45 : Ext inrᴾ A a ≅ Ext u (λ x → A (inlᴾ x)) a∧
    RS45 = to ,ᵉ (from ,ᵉ (linv ,ᵉ rinv))
      where
      -- restriction to the Φ-leg; its boundary on M comes from the glue and
      -- the boundary of h on the Ψ-leg.
      to : Ext inrᴾ A a → Ext u (λ x → A (inlᴾ x)) a∧
      to (h ,ᵉ ph) =
        (λ x → h (inlᴾ x))
        ,ᵉ funextᵉ (λ m → move-tr (glueᴾ m)
             (exo-concat (exo-apd h (glueᴾ m)) (happlyᵉ ph (v m))))

      -- copairing (the eliminator) of k and a; the coherence over M is the
      -- boundary of k, pushed across the glue.
      from : Ext u (λ x → A (inlᴾ x)) a∧ → Ext inrᴾ A a
      from (k ,ᵉ pk) =
        po-elim po A k a (λ m → move-tr' (glueᴾ m) (happlyᵉ pk m))
        ,ᵉ funextᵉ (po-βr po A k a (λ m → move-tr' (glueᴾ m) (happlyᵉ pk m)))

      -- η: the copairing of the two restrictions of h is h (uniqueness po-η,
      -- i.e. dependent elimination into the strict-equality family).
      linv : (z : Ext inrᴾ A a) → from (to z) =ᵉ z
      linv (h ,ᵉ ph) = ext-≡ (funextᵉ (po-η po _ h
        (po-βl po A _ a _)
        (λ ψ → exo-concat (po-βr po A _ a _ ψ) (exo-inv (happlyᵉ ph ψ)))))

      -- β: restricting the copairing to the Φ-leg gives back k.
      rinv : (z : Ext u (λ x → A (inlᴾ x)) a∧) → to (from z) =ᵉ z
      rinv (k ,ᵉ pk) = ext-≡ (funextᵉ (po-βl po A k a _))

{- 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

-}