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

--------------------------------------------------------------------------------
-- Corollary 3.12, strict realignment of propositional components.
--
-- For a full 2LTT cofibration i : Φ ↪ Ψ, a fibrant family of data D and a
-- fibrant family of propositions P over it, write S ψ = Σ (d : D ψ). P ψ d.
-- Given a total section s and a partial section s₀ whose data agree strictly,
-- the type of realignments
--
--     Σ (s' : Πψ. S ψ). (π₁ ∘ s' =ᵉ π₁ ∘ s) ×ᵉ (s' ∘ i =ᵉ s₀)
--
-- is contractible.  It is an exo type, so this is read through the fibrant
-- match: `realign-iso` gives Realign ≅ Extᵢ(P', l) with P' ψ = P ψ (π₁ (s ψ)),
-- each P' ψ contractible, and the trivial half of the cofibration finishes
-- (Lemma 3.11; no cofibrancy of Φ or Ψ).  Hence `realign-contr`,
-- `realignment` with its three components, and `realign-unique`.
--------------------------------------------------------------------------------

module Extension.PropRealign where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext

private
  variable
    ℓ ℓΦ ℓΨ : Level

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (c2 : is-cofib-2LTT i ℓ)
         (D : Ψ → UU ℓ)                            -- data
         (P : (ψ : Ψ) → D ψ → UU ℓ)                -- property
         (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
       where

  private
    cof : is-cofib i ℓ
    cof = pr1ᵉ c2

  -- the bundled family
  S : Ψ → UU ℓ
  S ψ = Σ (D ψ) (P ψ)

  private
    -- the property, as an exo family over the coerced data
    CP : (ψ : Ψ) → C (D ψ) → UUᵉ ℓ
    CP ψ w = C (P ψ (ic w))

    -- Strict Σ-splitting bookkeeping (a).  Fibre components of strictly equal
    -- pairs, transported to a common data point, agree, any two transport
    -- paths do the job, by UIPᵉ.
    snd-cong : {ψ : Ψ} {u v : C (S ψ)} (E : u =ᵉ v) {w : C (D ψ)}
               (q₁ : c (pr1 (ic u)) =ᵉ w) (q₂ : c (pr1 (ic v)) =ᵉ w)
             → exo-tr (CP ψ) q₁ (c (pr2 (ic u))) =ᵉ exo-tr (CP ψ) q₂ (c (pr2 (ic v)))
    snd-cong reflᵉ q₁ q₂ = exo-ap-tr (UIPᵉ q₁ q₂)

    -- Strict Σ-splitting bookkeeping (b).  Moving the property component of a
    -- pair along a strict equality of the data components.
    pair-tr : {ψ : Ψ} {w w' : C (D ψ)} (E : w =ᵉ w') (z : CP ψ w)
            → c {A = S ψ} (ic w , ic z) =ᵉ c (ic w' , ic (exo-tr (CP ψ) E z))
    pair-tr reflᵉ z = reflᵉ

    -- Transport of an ×ᵉ-pair splits componentwise (as in Extension.HomFillers).
    tr-×ᵉ : {ℓa ℓf ℓg : Level} {A : UUᵉ ℓa} {F : A → UUᵉ ℓf} {G : A → UUᵉ ℓg}
            {x y : A} (e : x =ᵉ y) (u : F x) (v : G x)
          → exo-tr (λ z → F z ×ᵉ G z) e (u ,ᵉ v) =ᵉ (exo-tr F e u ,ᵉ exo-tr G e v)
    tr-×ᵉ reflᵉ u v = reflᵉ

  ------------------------------------------------------------------------------
  -- The statement, for a total section s and a strictly-data-compatible
  -- partial section s₀.
  ------------------------------------------------------------------------------

  module _ (s  : (ψ : Ψ) → C (S ψ))
           (s₀ : (φ : Φ) → C (S (i φ)))
           (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ))))
         where

    -- the paper's type of realignments (an exo type)
    Realign : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓ)
    Realign = Σᵉ ((ψ : Ψ) → C (S ψ)) (λ s' →
                ((λ ψ → c (pr1 (ic (s' ψ)))) =ᵉ (λ ψ → c (pr1 (ic (s ψ)))))
                ×ᵉ ((λ φ → s' (i φ)) =ᵉ s₀))

    -- the property family along the data of s, and the transported partial
    -- section of it induced by s₀
    P' : Ψ → UU ℓ
    P' ψ = P ψ (pr1 (ic (s ψ)))

    l : (φ : Φ) → C (P' (i φ))
    l φ = exo-tr (CP (i φ)) (exo-inv (agr φ)) (c (pr2 (ic (s₀ φ))))

    private
      -- both strict-equality components of a realignment are strict
      -- propositions (UIPᵉ), so realignments with strictly equal underlying
      -- sections are strictly equal
      Realign-≡ : {r₁ r₂ : Realign} → pr1ᵉ r₁ =ᵉ pr1ᵉ r₂ → r₁ =ᵉ r₂
      Realign-≡ {r₁} {r₂} p =
        dep-pair-=ᵉ r₁ r₂
          (p ,ᵉ exo-concat (tr-×ᵉ p (pr1ᵉ (pr2ᵉ r₁)) (pr2ᵉ (pr2ᵉ r₁)))
                           (pair-=ᵉ _ _ (UIPᵉ _ _ ,ᵉ UIPᵉ _ _)))

    -- The paper's proof, step 1: realignments are strictly isomorphic to
    -- strict extensions of l in the fibrewise contractible family P'.
    realign-iso : Realign ≅ Ext i (λ ψ → C (P' ψ)) l
    realign-iso = to' ,ᵉ (from' ,ᵉ (from-to ,ᵉ to-from))
      where
      to' : Realign → Ext i (λ ψ → C (P' ψ)) l
      to' (s' ,ᵉ (q ,ᵉ r)) =
        (λ ψ → exo-tr (CP ψ) (happlyᵉ q ψ) (c (pr2 (ic (s' ψ)))))
        ,ᵉ funextᵉ (λ φ → snd-cong (happlyᵉ r φ) (happlyᵉ q (i φ)) (exo-inv (agr φ)))

      from' : Ext i (λ ψ → C (P' ψ)) l → Realign
      from' (F ,ᵉ p) =
        (λ ψ → c (pr1 (ic (s ψ)) , ic (F ψ)))
        ,ᵉ ( reflᵉ
           ,ᵉ funextᵉ (λ φ →
                exo-concat
                  (exo-ap (λ z → c {A = S (i φ)} (pr1 (ic (s (i φ))) , ic z))
                          (happlyᵉ p φ))
                  (exo-concat
                    (pair-tr (agr φ) (l φ))
                    (exo-ap (λ z → c {A = S (i φ)} (pr1 (ic (s₀ φ)) , ic z))
                            (exo-concat
                              (exo-tr-concat (exo-inv (agr φ)) (agr φ))
                              (exo-tr-left-law (CP (i φ)) (agr φ)))))) )

      from-to : (r : Realign) → from' (to' r) =ᵉ r
      from-to (s' ,ᵉ (q ,ᵉ r)) =
        Realign-≡ (funextᵉ (λ ψ →
          exo-inv (pair-tr (happlyᵉ q ψ) (c (pr2 (ic (s' ψ)))))))

      to-from : (w : Ext i (λ ψ → C (P' ψ)) l) → to' (from' w) =ᵉ w
      to-from (F ,ᵉ p) = ext-≡ reflᵉ

    -- Realign is fibrant, with the same match as the extension type.
    Realign-isFibrant : isFibrant Realign
    Realign-isFibrant =
      isfibrant (fibrant-match (Ext-isFibrant cof P' l))
                (≅-trans realign-iso (fibrant-witness (Ext-isFibrant cof P' l)))

    private
      -- each P' ψ is an inhabited proposition, hence contractible
      P'-contr : (ψ : Ψ) → is-contr (P' ψ)
      P'-contr ψ =
        is-proof-irrelevant-all-elements-equal
          (all-elements-equal-is-prop (propP ψ (pr1 (ic (s ψ)))))
          (pr2 (ic (s ψ)))

    -- Corollary 3.12: the type of realignments is contractible (as a
    -- fibrant type: its match is contractible), by the trivial-fibration
    -- half of the full 2LTT cofibration, no cofibrancy of Φ or Ψ.
    realign-contr : is-contr (fibrant-match Realign-isFibrant)
    realign-contr = rel-funext-holds-2LTT c2 P' P'-contr l

    -- In particular a realignment exists ...
    realignment : Realign
    realignment =
      pr1ᵉ (pr2ᵉ (fibrant-witness Realign-isFibrant)) (c (center _ realign-contr))

    -- ... changing only the property components of s (the data agree
    -- strictly with those of s) and restricting strictly to s₀:
    realigned : (ψ : Ψ) → C (S ψ)
    realigned = pr1ᵉ realignment

    realign-data : (λ ψ → c (pr1 (ic (realigned ψ)))) =ᵉ (λ ψ → c (pr1 (ic (s ψ))))
    realign-data = pr1ᵉ (pr2ᵉ realignment)

    realign-boundary : (λ φ → realigned (i φ)) =ᵉ s₀
    realign-boundary = pr2ᵉ (pr2ᵉ realignment)

    -- ... and it is unique up to homotopy: any two realignments become equal
    -- in the fibrant match.
    realign-unique : (r₁ r₂ : Realign)
      → Id (ic (pr1ᵉ (fibrant-witness Realign-isFibrant) r₁))
           (ic (pr1ᵉ (fibrant-witness Realign-isFibrant) r₂))
    realign-unique r₁ r₂ =
      all-elements-equal-is-prop (is-prop-is-contr _ realign-contr) _ _