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

--------------------------------------------------------------------------------
-- Corollary 5.5: univalence gives the homotopy Glue rules, contractibly
-- unique Glue data, and the complete constructor package up to homotopy.
--------------------------------------------------------------------------------

module Extension.Corollary55 where

open import Extension.Prelude
open import Extension.Univalence using (Univalence)
open import Extension.CofibFibration using (is-cofib)
open import Extension.RelFunext using (is-cofib-2LTT)
open import Extension.CofibClosure using (cofib-codomain-cofibrant)
open import Extension.GlueRules using (satisfies-homotopy-glue-rules)
open import Extension.GlueStructure using (has-strictly-coherent-glue)
open import Extension.GlueDataFibrant
  using (has-strong-glue-structure ; strong-to-strict)
open import Extension.GlueSandwich using (ua-strong-glue)
open import Extension.GlueHomotopySemantic using (strict-coh-to-homotopy-rules)
import Extension.GlueConstructorPackage as Constructor

private
  variable
    ℓS 𝓤 : Level

ConstructorConsequence : {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
  (cof : is-cofib i 𝓤) (cofΦ : isCofibrant Φ 𝓤)
  (cofΨ : isCofibrant Ψ 𝓤) →
  satisfies-homotopy-glue-rules i 𝓤 →
  UUᵉ (ℓS ⊔ lsuc 𝓤)
ConstructorConsequence {ℓS = ℓS} {𝓤 = 𝓤} {Φ = Φ} {Ψ} {i} cof cofΦ cofΨ rules =
  (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤)
  (f : (φ : Φ) → C (T φ ≃ A (i φ))) →
  let r = rules A T f
      G = pr1ᵉ r
      p = pr1ᵉ (pr2ᵉ r)
      ung = pr1ᵉ (pr2ᵉ (pr2ᵉ r))
      ubd = pr1ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ r)))
      invw = pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ r)))
  in Constructor.ThetaAnalysis.Package2.HomotopyConstructorPackage
       cof cofΦ cofΨ A T f G p ung ubd invw

homotopy-rules-give-constructors :
  {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
  (cof : is-cofib i 𝓤) (cofΦ : isCofibrant Φ 𝓤)
  (cofΨ : isCofibrant Ψ 𝓤)
  (rules : satisfies-homotopy-glue-rules i 𝓤) →
  ConstructorConsequence cof cofΦ cofΨ rules
homotopy-rules-give-constructors cof cofΦ cofΨ rules A T f =
  Constructor.ThetaAnalysis.Package2.homotopy-constructor-package
    cof cofΦ cofΨ A T f G p ung ubd invw
  where
  r = rules A T f
  G = pr1ᵉ r
  p = pr1ᵉ (pr2ᵉ r)
  ung = pr1ᵉ (pr2ᵉ (pr2ᵉ r))
  ubd = pr1ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ r)))
  invw = pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ r)))

record Corollary55
    {Φ Ψ : UUᵉ ℓS} (i : Φ → Ψ)
    (cof-small : is-cofib i 𝓤)
    (cof-large : is-cofib i (lsuc 𝓤))
    (cofΦ-small : isCofibrant Φ 𝓤)
    (cofΦ-large : isCofibrant Φ (lsuc 𝓤))
    : UUᵉ (lsuc (ℓS ⊔ lsuc 𝓤)) where
  field
    cofΨ-small : isCofibrant Ψ 𝓤
    cofΨ-large : isCofibrant Ψ (lsuc 𝓤)
    contractible-data : has-strong-glue-structure i 𝓤 cof-large
    homotopy-form : satisfies-homotopy-glue-rules i 𝓤
    constructors-up-to-homotopy :
      ConstructorConsequence cof-small cofΦ-small cofΨ-small homotopy-form

univalence-gives-homotopy-form :
  {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ} →
  Univalence 𝓤 →
  (c2-small : is-cofib-2LTT i 𝓤) →
  (c2-large : is-cofib-2LTT i (lsuc 𝓤)) →
  (cofΦ-small : isCofibrant Φ 𝓤) →
  (cofΦ-large : isCofibrant Φ (lsuc 𝓤)) →
  Corollary55 i (pr1ᵉ c2-small) (pr1ᵉ c2-large)
    cofΦ-small cofΦ-large
univalence-gives-homotopy-form {ℓS = ℓS} {𝓤 = 𝓤} {i = i} U c2-small c2-large
    cofΦ-small cofΦ-large = record
  { cofΨ-small = cofΨ-small
  ; cofΨ-large = cofΨ-large
  ; contractible-data = strong
  ; homotopy-form = rules
  ; constructors-up-to-homotopy =
      homotopy-rules-give-constructors
        (pr1ᵉ c2-small) cofΦ-small cofΨ-small rules
  }
  where
  cofΨ-small = cofib-codomain-cofibrant c2-small cofΦ-small
  cofΨ-large = cofib-codomain-cofibrant c2-large cofΦ-large
  strong = ua-strong-glue U (pr1ᵉ c2-large) (pr2ᵉ c2-large)
  strict : has-strictly-coherent-glue i 𝓤
  strict = strong-to-strict i 𝓤 (pr1ᵉ c2-large) strong
  rules : satisfies-homotopy-glue-rules i 𝓤
  rules = strict-coh-to-homotopy-rules i 𝓤 strict