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

--------------------------------------------------------------------------------
-- Univalence and gluing: the computational heart of Theorem 5.4, Step 3.
--
-- A map between contractible types is an equivalence, hence its homotopy fibre
-- is contractible.  Combined with `Extension.Fibre` (the match of a strict fibre
-- is the homotopy fibre) this gives contractibility of the strict extension type
-- of a pointwise-contractible family, which is what makes GlueData contractible
-- once univalence makes the glue family pointwise contractible and cofibrancy
-- makes the products contractible.  There is no univalence postulate here;
-- paper-facing uses take an explicit `Extension.Univalence.Univalence` witness.
--
-- Theorem 5.15 (univalence ⇔ gluing) also needs a path interval and the
-- weak-Glue-to-univalence direction; it is checked in
-- `Extension.GlueSandwichFull` and exposed in `src/index.agda`.
--------------------------------------------------------------------------------

module Extension.GlueUA where

open import Extension.Prelude
open import Extension.Core
open import Extension.Fibre

private
  variable
    ℓ ℓ' : Level

contr-contr-isEquiv : {A : UU ℓ} {B : UU ℓ'} → is-contr A → is-contr B
                    → (f : A → B) → isEquiv f
contr-contr-isEquiv {A = A} {B} cA cB f =
  invertibles-are-equiv f
    ( (λ _ → center A cA)
    , ( (λ a → (centrality A cA a) ⁻¹)
      , (λ b → centrality B cB (f (center A cA)) · (centrality B cB b) ⁻¹) ) )

contr-map-fibre-contr : {A : UU ℓ} {B : UU ℓ'} → is-contr A → is-contr B
                      → (f : A → B) (b : B) → is-contr (fiber f b)
contr-map-fibre-contr cA cB f b = contr-contr-isEquiv cA cB f b

-- With `Extension.Fibre.strict-fibre-match`, the strict fibre of such a map is a
-- fibrant type whose fibrant match is this contractible homotopy fibre, the
-- strict extension type / GlueData is therefore contractible.