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

--------------------------------------------------------------------------------
-- Lemma 5.10.  If, for all A,B : 𝓤, the comparison map  idtoeqv_{A,B} : (A = B) → (A ≃ B)
-- has a section  s_{A,B},  then 𝓤 is univalent (every idtoeqv_{A,B} is an
-- equivalence).
--
-- This is the engine of Licata's gluing⇒univalence argument.  Proof: idtoeqv is
-- a fibrewise map out of the based-path family, so by the fundamental theorem of
-- identity types (`FundamentalId.fundamental-id`) it is a fibrewise equivalence
-- as soon as its total space  Σ(B). A ≃ B  is contractible.  That total space is
-- a retract of the contractible singleton  Σ(B). A = B  (via the totalised
-- idtoeqv and its totalised section), hence contractible.
--------------------------------------------------------------------------------

module Extension.UAFromSection where

open import Extension.Prelude
open import Extension.FundamentalId using (fundamental-id)
open import Extension.PiTruncation using (fwd-path-contr)

private
  variable
    𝓤 : Level

module _ (s    : (A B : UU 𝓤) → (A ≃ B) → Id A B)
         (sect : (A B : UU 𝓤) (g : A ≃ B) → Id (idtoeqv (s A B g)) g)
       where

  ua-from-section : (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})
  ua-from-section A B = fundamental-id (λ B' → idtoeqv {A = A} {B = B'}) contr-A B
    where
    Θ : Σ (UU 𝓤) (λ B' → Id A B') → Σ (UU 𝓤) (λ B' → A ≃ B')
    Θ (B' , p) = B' , idtoeqv p

    S : Σ (UU 𝓤) (λ B' → A ≃ B') → Σ (UU 𝓤) (λ B' → Id A B')
    S (B' , g) = B' , s A B' g

    rs : (w : Σ (UU 𝓤) (λ B' → A ≃ B')) → Id (Θ (S w)) w
    rs (B' , g) = dep-pair⁼ _ _ (refl , sect A B' g)

    contr-A : is-contr (Σ (UU 𝓤) (λ B' → A ≃ B'))
    contr-A = retract-of-singleton (Θ , (S , rs)) (fwd-path-contr A)

{- References:

  [Licata]     Daniel R. Licata.  weak univalence with "beta" implies full
               univalence.  Message of 7 September 2016 to the Homotopy Type Theory
               mailing list.
               https://groups.google.com/g/homotopytypetheory/c/j2KBIvDw53s

-}