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

--------------------------------------------------------------------------------
-- An interface for outer pushouts, which 2LTT does not provide and the paper
-- assumes where it needs them (Lemma 3.5 and Lemma 3.8).
--
-- `is-exo-pushout f g inlᴾ inrᴾ glueᴾ ℓE` says that the strict cocone on P
-- under L ← Φ → R has a dependent eliminator with pointwise strict β.
-- Dependent elimination is the right form here: the lemmas need sections of
-- families over the pushout, not just maps out of it, and uniqueness of
-- dependent cocones then comes for free by eliminating into a family of
-- strict equalities (`po-η`).  No rule over `glueᴾ` is needed, since any such
-- rule is an equality between strict equalities and holds by UIPᵉ.
--
-- Derived: `po-rec`, `po-η`, and `po-section-≅`, the isomorphism between
-- sections over the pushout and compatible pairs of sections, which is the
-- form the proofs use.
--------------------------------------------------------------------------------

module Extension.ExoPushout where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓ ℓ' ℓΦ ℓL ℓR ℓP ℓE ℓX ℓB ℓA : Level

--------------------------------------------------------------------------------
-- General strict-equality helpers (used here and in the pushout lemmas).
--------------------------------------------------------------------------------

-- Transport along e in a family is injective (it is an iso with inverse
-- transport along exo-inv e).
exo-tr-inj : {X : UUᵉ ℓ} (Q : X → UUᵉ ℓ') {x y : X} (e : x =ᵉ y) {u v : Q x}
           → exo-tr Q e u =ᵉ exo-tr Q e v → u =ᵉ v
exo-tr-inj Q reflᵉ q = q

-- A section h of a reindexed family  A ∘ q  takes strictly equal values, up to
-- transport, at strictly equal points whose q-images are identified with a
-- common b.  (With UIPᵉ the two identifications need not be compared.)
tr-section-compat : {X : UUᵉ ℓX} {B : UUᵉ ℓB} (q : X → B) (A : B → UUᵉ ℓA)
                    (h : (x : X) → A (q x)) {x₁ x₂ : X} (e : x₁ =ᵉ x₂)
                    {b : B} (α : q x₁ =ᵉ b) (β : q x₂ =ᵉ b)
                  → exo-tr A α (h x₁) =ᵉ exo-tr A β (h x₂)
tr-section-compat q A h reflᵉ α β = exo-ap-tr (UIPᵉ α β)

private
  -- Transport in a constant family is the identity.
  exo-tr-const' : {X : UUᵉ ℓ} {B : UUᵉ ℓ'} {x y : X} (e : x =ᵉ y) (b : B)
                → exo-tr (λ _ → B) e b =ᵉ b
  exo-tr-const' reflᵉ b = reflᵉ

--------------------------------------------------------------------------------
-- The interface.
--------------------------------------------------------------------------------

record is-exo-pushout
    {Φ : UUᵉ ℓΦ} {L : UUᵉ ℓL} {R : UUᵉ ℓR}
    (f : Φ → L) (g : Φ → R)
    {P : UUᵉ ℓP} (inlᴾ : L → P) (inrᴾ : R → P)
    (glueᴾ : (w : Φ) → inlᴾ (f w) =ᵉ inrᴾ (g w))
    (ℓE : Level)
    : UUᵉ (ℓΦ ⊔ ℓL ⊔ ℓR ⊔ ℓP ⊔ lsuc ℓE) where
  field
    po-elim : (E : P → UUᵉ ℓE)
              (l : (x : L) → E (inlᴾ x))
              (r : (y : R) → E (inrᴾ y))
              (coh : (w : Φ) → exo-tr E (glueᴾ w) (l (f w)) =ᵉ r (g w))
            → (p : P) → E p
    po-βl : (E : P → UUᵉ ℓE)
            (l : (x : L) → E (inlᴾ x))
            (r : (y : R) → E (inrᴾ y))
            (coh : (w : Φ) → exo-tr E (glueᴾ w) (l (f w)) =ᵉ r (g w))
            (x : L)
          → po-elim E l r coh (inlᴾ x) =ᵉ l x
    po-βr : (E : P → UUᵉ ℓE)
            (l : (x : L) → E (inlᴾ x))
            (r : (y : R) → E (inrᴾ y))
            (coh : (w : Φ) → exo-tr E (glueᴾ w) (l (f w)) =ᵉ r (g w))
            (y : R)
          → po-elim E l r coh (inrᴾ y) =ᵉ r y
  -- No glue-computation rule: its type is a strict prop by UIPᵉ.

open is-exo-pushout public

--------------------------------------------------------------------------------
-- Dependent cocones, and derived UMP material.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {L : UUᵉ ℓL} {R : UUᵉ ℓR}
         {f : Φ → L} {g : Φ → R}
         {P : UUᵉ ℓP} {inlᴾ : L → P} {inrᴾ : R → P}
         {glueᴾ : (w : Φ) → inlᴾ (f w) =ᵉ inrᴾ (g w)}
       where

  -- Compatible cocone data for a family E over P: a pair of sections over the
  -- two legs, agreeing (up to transport along glueᴾ) on Φ.
  Coconeᵈ : (E : P → UUᵉ ℓE) → UUᵉ (ℓΦ ⊔ ℓL ⊔ ℓR ⊔ ℓE)
  Coconeᵈ E = Σᵉ ((x : L) → E (inlᴾ x)) (λ l →
              Σᵉ ((y : R) → E (inrᴾ y)) (λ r →
                (w : Φ) → exo-tr E (glueᴾ w) (l (f w)) =ᵉ r (g w)))

  -- Equality of cocones from equality of the two section components: the
  -- coherence component is a strict proposition (funextᵉ + UIPᵉ).
  cocone-=ᵉ : {E : P → UUᵉ ℓE} {z z' : Coconeᵈ E}
            → pr1ᵉ z =ᵉ pr1ᵉ z'
            → pr1ᵉ (pr2ᵉ z) =ᵉ pr1ᵉ (pr2ᵉ z')
            → z =ᵉ z'
  cocone-=ᵉ {E = E} {l ,ᵉ (r ,ᵉ coh)} {.l ,ᵉ (.r ,ᵉ coh')} reflᵉ reflᵉ =
    exo-ap (λ z → l ,ᵉ (r ,ᵉ z)) (funextᵉ (λ w → UIPᵉ (coh w) (coh' w)))

  module _ (po : is-exo-pushout f g inlᴾ inrᴾ glueᴾ ℓE) where

    -- Uniqueness (dependent η): two sections agreeing on both legs agree.
    -- Derived by eliminating into the strict-equality family; the coherence
    -- over glueᴾ is free by UIPᵉ.
    po-η : {E : P → UUᵉ ℓE} (h k : (p : P) → E p)
         → ((x : L) → h (inlᴾ x) =ᵉ k (inlᴾ x))
         → ((y : R) → h (inrᴾ y) =ᵉ k (inrᴾ y))
         → (p : P) → h p =ᵉ k p
    po-η {E = E} h k hl hr =
      po-elim po (λ p → h p =ᵉ k p) hl hr (λ w → UIPᵉ _ _)

    private
      rec-coh : {X : UUᵉ ℓE} (l : L → X) (r : R → X)
              → ((w : Φ) → l (f w) =ᵉ r (g w))
              → (w : Φ) → exo-tr (λ _ → X) (glueᴾ w) (l (f w)) =ᵉ r (g w)
      rec-coh l r coh w = exo-concat (exo-tr-const' (glueᴾ w) (l (f w))) (coh w)

    -- The recursor and its β-rules (constant families).
    po-rec : {X : UUᵉ ℓE} (l : L → X) (r : R → X)
           → ((w : Φ) → l (f w) =ᵉ r (g w)) → P → X
    po-rec {X = X} l r coh = po-elim po (λ _ → X) l r (rec-coh l r coh)

    po-rec-βl : {X : UUᵉ ℓE} (l : L → X) (r : R → X)
                (coh : (w : Φ) → l (f w) =ᵉ r (g w)) (x : L)
              → po-rec l r coh (inlᴾ x) =ᵉ l x
    po-rec-βl {X = X} l r coh = po-βl po (λ _ → X) l r (rec-coh l r coh)

    po-rec-βr : {X : UUᵉ ℓE} (l : L → X) (r : R → X)
                (coh : (w : Φ) → l (f w) =ᵉ r (g w)) (y : R)
              → po-rec l r coh (inrᴾ y) =ᵉ r y
    po-rec-βr {X = X} l r coh = po-βr po (λ _ → X) l r (rec-coh l r coh)

    -- The master strict isomorphism: sections of a family over the pushout
    -- are the compatible pairs of sections over the legs.  This is
    -- the working form of the UMP in the paper's proofs of RS 4.2 / 4.5 and
    -- of closure of cofibrations under pushout.
    po-section-≅ : (E : P → UUᵉ ℓE) → ((p : P) → E p) ≅ Coconeᵈ E
    po-section-≅ E = to ,ᵉ (from ,ᵉ (linv ,ᵉ rinv))
      where
      to : ((p : P) → E p) → Coconeᵈ E
      to h = (λ x → h (inlᴾ x))
           ,ᵉ ((λ y → h (inrᴾ y))
           ,ᵉ (λ w → exo-apd h (glueᴾ w)))

      from : Coconeᵈ E → (p : P) → E p
      from (l ,ᵉ (r ,ᵉ coh)) = po-elim po E l r coh

      linv : (h : (p : P) → E p) → from (to h) =ᵉ h
      linv h = funextᵉ
        (po-η (from (to h)) h
          (po-βl po E (λ x → h (inlᴾ x)) (λ y → h (inrᴾ y)) (λ w → exo-apd h (glueᴾ w)))
          (po-βr po E (λ x → h (inlᴾ x)) (λ y → h (inrᴾ y)) (λ w → exo-apd h (glueᴾ w))))

      rinv : (z : Coconeᵈ E) → to (from z) =ᵉ z
      rinv (l ,ᵉ (r ,ᵉ coh)) =
        cocone-=ᵉ (funextᵉ (po-βl po E l r coh)) (funextᵉ (po-βr po E l r coh))

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

-}