------------------------------------------------------------------------
-- The univalence axiom
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module Univalence-axiom
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Bijection eq as Bijection using (_↔_)
open import Bool eq
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq
  using (_≃_; ⟨_,_⟩; Is-equivalence) renaming (_∘_ to _⊚_)
import Equivalence.Contractible-preimages eq as CP
import Equivalence.Half-adjoint eq as HA
open import Extensionality eq
open import Function-universe eq as F hiding (id; _∘_)
open import Groupoid eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Injection eq using (Injective)
open import Logical-equivalence using (_⇔_)
import Nat eq as Nat
open import Prelude hiding (swap)
open import Surjection eq using (_↠_)

------------------------------------------------------------------------
-- The univalence axiom

-- If two sets are equal, then they are equivalent.

≡⇒≃ :  {} {A B : Type }  A  B  A  B
≡⇒≃ = ≡⇒↝ equivalence

-- The univalence axiom states that ≡⇒≃ is an equivalence.

record Univalence′ {} (A B : Type ) : Type (lsuc ) where
  no-eta-equality
  pattern
  field
    univalence : Is-equivalence (≡⇒≃ {A = A} {B = B})

Univalence :    Type (lsuc )
Univalence  = {A B : Type }  Univalence′ A B

-- An immediate consequence is that equalities are equivalent to
-- equivalences.

≡≃≃ :  {} {A B : Type }  Univalence′ A B  (A  B)  (A  B)
≡≃≃ univ =  ≡⇒≃ , Univalence′.univalence univ 

-- In the case of sets equalities are equivalent to bijections (if we
-- add the assumption of extensionality).

≡≃↔ :  {} {A B : Type } 
      Univalence′ A B 
      Extensionality   
      Is-set A 
      (A  B)  (A  B)
≡≃↔ {A} {B} univ ext A-set =
  (A  B)  ↝⟨ ≡≃≃ univ 
  (A  B)  ↔⟨ inverse $ Eq.↔↔≃ ext A-set ⟩□
  (A  B)  

-- Some abbreviations.

≡⇒→ :  {} {A B : Type }  A  B  A  B
≡⇒→ = _≃_.to  ≡⇒≃

≡⇒← :  {} {A B : Type }  A  B  B  A
≡⇒← = _≃_.from  ≡⇒≃

≃⇒≡ :  {} {A B : Type }  Univalence′ A B  A  B  A  B
≃⇒≡ univ = _≃_.from (≡≃≃ univ)

-- Univalence′ can be expressed without the record type.

Univalence′≃Is-equivalence-≡⇒≃ :
   {} {A B : Type } 
  Univalence′ A B  Is-equivalence (≡⇒≃ {A = A} {B = B})
Univalence′≃Is-equivalence-≡⇒≃ =
  Eq.↔→≃
    Univalence′.univalence
     eq  record { univalence = eq })
    refl
     { (record { univalence = _ })  refl _ })

------------------------------------------------------------------------
-- Propositional extensionality

-- Propositional extensionality.
--
-- Basically as defined by Chapman, Uustalu and Veltri in "Quotienting
-- the Delay Monad by Weak Bisimilarity".

Propositional-extensionality : ( : Level)  Type (lsuc )
Propositional-extensionality  =
  {A B : Type }  Is-proposition A  Is-proposition B  A  B  A  B

-- Propositional extensionality is equivalent to univalence restricted
-- to propositions (assuming extensionality).
--
-- I took the statement of this result from Chapman, Uustalu and
-- Veltri's "Quotienting the Delay Monad by Weak Bisimilarity", and
-- Nicolai Kraus helped me with the proof.

Propositional-extensionality-is-univalence-for-propositions :
   {} 
  Extensionality (lsuc ) (lsuc ) 

  Propositional-extensionality 
    
  ({A B : Type } 
   Is-proposition A  Is-proposition B  Univalence′ A B)

Propositional-extensionality-is-univalence-for-propositions {} ext =
  Propositional-extensionality                           ↝⟨ lemma 

  ({A B : Type } 
   Is-proposition A  Is-proposition B 
   Is-equivalence (≡⇒≃ {A = A} {B = B}))                  ↝⟨ (implicit-∀-cong ext $
                                                              implicit-∀-cong ext $
                                                              ∀-cong ext′ λ _ 
                                                              ∀-cong ext′ λ _ 
                                                              inverse Univalence′≃Is-equivalence-≡⇒≃) ⟩□
  ({A B : Type } 
   Is-proposition A  Is-proposition B  Univalence′ A B) 
  where
  ext′ : Extensionality  (lsuc )
  ext′ = lower-extensionality _ lzero ext

  ext″ : Extensionality  
  ext″ = lower-extensionality _ _ ext

  ⇔≃≡ :
    Propositional-extensionality  
    {A B : Type } 
    Is-proposition A  Is-proposition B 
    (A  B)  (A  B)
  ⇔≃≡ prop-ext {A} {B} A-prop B-prop =
    A  B                        ↝⟨ proj₂ (Eq.propositional-identity≃≡
                                              (A B : Proposition )  proj₁ A  proj₁ B)
                                              { (A , A-prop) (B , B-prop) 
                                                  ⇔-closure ext″ 1 A-prop B-prop })
                                              _  F.id)
                                              { (A , A-prop) (B , B-prop) A⇔B 
                                                  Σ-≡,≡→≡ (prop-ext A-prop B-prop A⇔B)
                                                          (H-level-propositional ext″ 1 _ _) }))
                                          ext 
    (A , A-prop)  (B , B-prop)  ↔⟨ inverse $ ignore-propositional-component
                                                (H-level-propositional ext″ 1) ⟩□
    A  B                        

  ≡-closure :
    Propositional-extensionality  
    {A B : Type } 
    Is-proposition A  Is-proposition B  Is-proposition (A  B)
  ≡-closure prop-ext A-prop B-prop =
    H-level.respects-surjection
      (_≃_.surjection (⇔≃≡ prop-ext A-prop B-prop))
      1
      (⇔-closure ext″ 1 A-prop B-prop)

  lemma =
    Eq.⇔→≃
      ([inhabited⇒+]⇒+ 0 λ prop-ext 
       implicit-Π-closure ext 1 λ _ 
       implicit-Π-closure ext 1 λ _ 
       Π-closure ext′ 1 λ A-prop 
       Π-closure ext′ 1 λ B-prop 
       Π-closure ext′ 1 λ _ 
       ≡-closure (prop-ext {_}) A-prop B-prop)
      (implicit-Π-closure ext 1 λ _ 
       implicit-Π-closure ext 1 λ _ 
       Π-closure ext′ 1 λ _ 
       Π-closure ext′ 1 λ _ 
       Is-equivalence-propositional ext)
       prop-ext A-prop B-prop 
         _⇔_.from HA.Is-equivalence⇔Is-equivalence-CP $ λ A≃B 
         ( prop-ext A-prop B-prop (_≃_.logical-equivalence A≃B)
         , Eq.left-closure ext″ 0 A-prop _ _
         ) , λ _  Σ-≡,≡→≡
               (≡-closure prop-ext A-prop B-prop _ _)
               (mono₁ 1 (Eq.left-closure ext″ 0 A-prop) _ _))
       univ {A B} A-prop B-prop 
         A  B  ↔⟨ Eq.⇔↔≃ ext″ A-prop B-prop 
         A  B  ↔⟨ inverse  _ , univ A-prop B-prop  ⟩□
         A  B  )

------------------------------------------------------------------------
-- An alternative formulation of univalence

-- First some supporting lemmas.

-- A variant of a part of Theorem 5.8.2 from the HoTT book.

flip-subst-is-equivalence↔∃-is-contractible :
   {a pℓ} {A : Type a} {P : A  Type pℓ} {x : A} {p : P x} 
  (∀ y  Is-equivalence (flip (subst {y = y} P) p))
    ↝[ a  pℓ  a  pℓ ]
  Contractible ( P)
flip-subst-is-equivalence↔∃-is-contractible {pℓ} {P} {x} {p} =
  generalise-ext?-prop
    lemma
     ext  Π-closure (lower-extensionality pℓ lzero ext) 1 λ _ 
             Is-equivalence-propositional ext)
    Contractible-propositional
  where
  lemma :
    (∀ y  Is-equivalence (flip (subst {y = y} P) p))
      
    Contractible ( P)
  lemma = record
    { to = λ eq                          $⟨ other-singleton-contractible x 
        Contractible (Other-singleton x)  ↝⟨ id 
        Contractible ( (x ≡_))           ↝⟨ H-level.respects-surjection (∃-cong λ y  _≃_.surjection  _ , eq y ) 0 ⟩□
        Contractible ( P)                
    ; from = λ { ((y , q) , u) z 
        _≃_.is-equivalence (Eq.↔⇒≃ (record
          { surjection = record
            { logical-equivalence = record
              { from = λ r 
                  x  ≡⟨ cong proj₁ $ sym $ u (x , p) 
                  y  ≡⟨ cong proj₁ $ u (z , r) ⟩∎
                  z  
              }
            ; right-inverse-of = λ r 
                subst P (trans (cong proj₁ (sym (u (x , p))))
                               (cong proj₁ (u (z , r)))) p         ≡⟨ sym $ subst-subst _ _ _ _ 

                subst P (cong proj₁ (u (z , r)))
                  (subst P (cong proj₁ (sym (u (x , p)))) p)       ≡⟨ cong (subst P _) $ cong  p  subst P p _) $ sym $ proj₁-Σ-≡,≡←≡ _ 

                subst P (cong proj₁ (u (z , r)))
                  (subst P (proj₁ (Σ-≡,≡←≡ (sym (u (x , p))))) p)  ≡⟨ cong (subst P _) $ proj₂ $ Σ-≡,≡←≡ (sym (u (x , p))) 

                subst P (cong proj₁ (u (z , r))) q                 ≡⟨ cong  p  subst P p _) $ sym $ proj₁-Σ-≡,≡←≡ _ 

                subst P (proj₁ (Σ-≡,≡←≡ (u (z , r)))) q            ≡⟨ proj₂ $ Σ-≡,≡←≡ (u (z , r)) ⟩∎

                r                                                  
            }
          ; left-inverse-of = elim¹
               {z} x≡z  trans (cong proj₁ (sym (u (x , p))))
                                 (cong proj₁ (u (z , subst P x≡z p))) 
                           x≡z)
              (trans (cong proj₁ (sym (u (x , p))))
                     (cong proj₁ (u (x , subst P (refl x) p)))  ≡⟨ cong₂ trans (cong-sym _ _)
                                                                               (cong  p  cong proj₁ (u (x , p))) $ subst-refl _ _) 
               trans (sym (cong proj₁ (u (x , p))))
                     (cong proj₁ (u (x , p)))                   ≡⟨ trans-symˡ _ ⟩∎

               refl x                                           )
          })) }
    }

-- If f is an equivalence, then f ∘ sym is also an equivalence.

∘-sym-preserves-equivalences :
   {a b} {A : Type a} {B : Type b} {x y : A} {f : x  y  B} 
  Is-equivalence f ↝[ a  b  a  b ] Is-equivalence (f  sym)
∘-sym-preserves-equivalences {A} {B} =
  Is-equivalence≃Is-equivalence-∘ʳ
    (_≃_.is-equivalence $ Eq.↔⇒≃ ≡-comm)

-- An alternative formulation of univalence, due to Martin Escardo
-- (see the following post to the Homotopy Type Theory group from
-- 2018-04-05:
-- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ).

Other-univalence :    Type (lsuc )
Other-univalence  =
  {B : Type }  Contractible ( λ (A : Type )  A  B)

-- Univalence and Other-univalence are pointwise isomorphic (assuming
-- extensionality).

Univalence↔Other-univalence :
   {} 
  Univalence  ↝[ lsuc   lsuc  ] Other-univalence 
Univalence↔Other-univalence {} ext =
  Univalence                                                           ↝⟨ implicit-∀-cong ext $ implicit-∀-cong ext $
                                                                           from-equivalence Univalence′≃Is-equivalence-≡⇒≃ 
  ({A B : Type }  Is-equivalence (≡⇒≃ {A = A} {B = B}))               ↔⟨ Bijection.implicit-Π↔Π 
  ((A {B} : Type )  Is-equivalence (≡⇒≃ {A = A} {B = B}))             ↝⟨ (∀-cong ext λ _  from-bijection Bijection.implicit-Π↔Π) 
  ((A B : Type )  Is-equivalence (≡⇒≃ {A = A} {B = B}))               ↝⟨ (∀-cong ext λ _  ∀-cong ext λ _  ∘-sym-preserves-equivalences ext) 
  ((A B : Type )  Is-equivalence (≡⇒≃ {A = A} {B = B}  sym))         ↝⟨ (∀-cong ext λ _  ∀-cong ext λ B 
                                                                            Is-equivalence-cong ext  B≡A 
      ≡⇒≃ (sym B≡A)                                                           ≡⟨ ≡⇒↝-in-terms-of-subst-sym _ _ 
      subst (_≃ B) (sym (sym B≡A)) Eq.id                                      ≡⟨ cong (flip (subst _) _) $ sym-sym _ ⟩∎
      subst (_≃ B) B≡A Eq.id                                                  )) 

  ((A B : Type )  Is-equivalence (flip (subst {y = A} (_≃ B)) F.id))  ↔⟨ Π-comm 
  ((B A : Type )  Is-equivalence (flip (subst {y = A} (_≃ B)) F.id))  ↝⟨ (∀-cong ext λ _  flip-subst-is-equivalence↔∃-is-contractible ext) 
  ((B : Type )  Contractible ( λ (A : Type )  A  B))              ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
  ({B : Type }  Contractible ( λ (A : Type )  A  B))              

------------------------------------------------------------------------
-- Some simple lemmas

opaque

  -- "Evaluation rule" for ≡⇒≃.

  ≡⇒≃-refl :  {a} {A : Type a} 
             ≡⇒≃ (refl A)  Eq.id
  ≡⇒≃-refl = ≡⇒↝-refl

  -- "Evaluation rule" for ≡⇒→.

  ≡⇒→-refl :  {a} {A : Type a} 
             ≡⇒→ (refl A)  id
  ≡⇒→-refl = cong _≃_.to ≡⇒≃-refl

  -- "Evaluation rule" for ≡⇒←.

  ≡⇒←-refl :  {a} {A : Type a} 
             ≡⇒← (refl A)  id
  ≡⇒←-refl = cong _≃_.from ≡⇒≃-refl

  -- "Evaluation rule" (?) for ≃⇒≡.

  ≃⇒≡-id :  {a} {A : Type a}
           (univ : Univalence′ A A) 
           ≃⇒≡ univ Eq.id  refl A
  ≃⇒≡-id univ =
    ≃⇒≡ univ Eq.id           ≡⟨ sym $ cong (≃⇒≡ univ) ≡⇒≃-refl 
    ≃⇒≡ univ (≡⇒≃ (refl _))  ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    refl _                   

  -- A simplification lemma for ≃⇒≡.

  ≡⇒→-≃⇒≡ :  k {} {A B : Type } {eq : A  B}
            (univ : Univalence′ A B) 
            to-implication (≡⇒↝ k (≃⇒≡ univ eq))  _≃_.to eq
  ≡⇒→-≃⇒≡ k {eq} univ =
    to-implication (≡⇒↝ k (≃⇒≡ univ eq))  ≡⟨ to-implication-≡⇒↝ k _ 
    ≡⇒↝ implication (≃⇒≡ univ eq)         ≡⟨ sym $ to-implication-≡⇒↝ equivalence _ 
    ≡⇒→ (≃⇒≡ univ eq)                     ≡⟨ cong _≃_.to (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩∎
    _≃_.to eq                             

------------------------------------------------------------------------
-- Another alternative formulation of univalence

-- Univalence′ A B is pointwise equivalent to CP.Univalence′ A B
-- (assuming extensionality).

Univalence′≃Univalence′-CP :
   {} {A B : Type } 
  Extensionality (lsuc ) (lsuc ) 
  Univalence′ A B  CP.Univalence′ A B
Univalence′≃Univalence′-CP {} {A} {B} ext =
  Univalence′ A B                         ↝⟨ Univalence′≃Is-equivalence-≡⇒≃ 

  Is-equivalence ≡⇒≃                      ↝⟨ Is-equivalence-cong ext $
                                             elim
                                                A≡B  ≡⇒≃ A≡B  _≃_.from ≃≃≃ (CP.≡⇒≃ A≡B))
                                                C 
      ≡⇒≃ (refl _)                                ≡⟨ ≡⇒≃-refl 
      Eq.id                                       ≡⟨ Eq.lift-equality ext′ (refl _) 
      _≃_.from ≃≃≃ CP.id                          ≡⟨ cong (_≃_.from ≃≃≃) $ sym CP.≡⇒≃-refl ⟩∎
      _≃_.from ≃≃≃ (CP.≡⇒≃ (refl _))              ) 

  Is-equivalence (_≃_.from ≃≃≃  CP.≡⇒≃)  ↝⟨ Eq.⇔→≃
                                               (Is-equivalence-propositional ext)
                                               (Is-equivalence-propositional ext)
                                               (Eq.Two-out-of-three.g-g∘f (Eq.two-out-of-three _ _)
                                                  (_≃_.is-equivalence (inverse ≃≃≃)))
                                               (flip (Eq.Two-out-of-three.f-g (Eq.two-out-of-three _ _))
                                                  (_≃_.is-equivalence (inverse ≃≃≃))) 

  Is-equivalence CP.≡⇒≃                   ↝⟨ Is-equivalence≃Is-equivalence-CP ext ⟩□

  CP.Is-equivalence CP.≡⇒≃                
  where
  ext′ : Extensionality  
  ext′ = lower-extensionality _ _ ext

  ≃≃≃ : {A B : Type }  (A  B)  (A CP.≃ B)
  ≃≃≃ = ≃≃≃-CP ext′

-- Univalence ℓ is pointwise equivalent to CP.Univalence ℓ (assuming
-- extensionality).

Univalence≃Univalence-CP :
   {} 
  Extensionality (lsuc ) (lsuc ) 
  Univalence   CP.Univalence 
Univalence≃Univalence-CP {} ext =
  implicit-∀-cong ext $ implicit-∀-cong ext $
  Univalence′≃Univalence′-CP ext

------------------------------------------------------------------------
-- A consequence: Type is not a set

-- The univalence axiom implies that Type is not a set. (This was
-- pointed out to me by Thierry Coquand.)

module _ (univ : Univalence′ Bool Bool) where

  -- First note that the univalence axiom implies that there is an
  -- inhabitant of Bool ≡ Bool that is not equal to refl.

  swap-as-an-equality : Bool  Bool
  swap-as-an-equality = ≃⇒≡ univ (Eq.↔⇒≃ swap)

  opaque

    swap≢refl : swap-as-an-equality  refl Bool
    swap≢refl =
      swap-as-an-equality  refl _            ↝⟨ cong ≡⇒→ 
      ≡⇒→ swap-as-an-equality  ≡⇒→ (refl _)  ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) 
      not  id                                ↝⟨ cong (_$ false) 
      true  false                            ↝⟨ Bool.true≢false ⟩□
                                             

    -- This implies that Type is not a set.

    ¬-Type-set : ¬ Is-set Type
    ¬-Type-set =
      Is-set Type                      ↝⟨  h  h _ _) 
      swap-as-an-equality  refl Bool  ↝⟨ swap≢refl ⟩□
                                      

opaque

  -- The result can be generalised to arbitrary universe levels.

  ¬-Type-set-↑ :  {} 
                 Univalence′ (  Bool) (  Bool) 
                 ¬ Is-set (Type )
  ¬-Type-set-↑ {} univ =
    Is-set (Type )                          ↝⟨  h  h _ _) 
    swap-as-an-equality-↑  refl (  Bool)  ↝⟨ swap-↑≢refl ⟩□
                                            
    where
    swap-as-an-equality-↑ :   Bool    Bool
    swap-as-an-equality-↑ =
      ≃⇒≡ univ $
      Eq.↔⇒≃ $
      (Bijection.inverse Bijection.↑↔
         Bijection.∘
       swap
         Bijection.∘
       Bijection.↑↔)

    swap-↑≢refl : swap-as-an-equality-↑  refl (  Bool)
    swap-↑≢refl =
      swap-as-an-equality-↑  refl _            ↝⟨ cong ≡⇒→ 
      ≡⇒→ swap-as-an-equality-↑  ≡⇒→ (refl _)  ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) 
      lift  not  lower  id                   ↝⟨ cong (lower  (_$ lift false)) 
      true  false                              ↝⟨ Bool.true≢false ⟩□
                                               

------------------------------------------------------------------------
-- A consequence: some equality types have infinitely many inhabitants

opaque

  -- Some equality types have infinitely many inhabitants (assuming
  -- univalence).

  equality-can-have-infinitely-many-inhabitants :
    Univalence′   
     λ (A : Type)   λ (B : Type) 
     λ (p :   A  B)  Injective p
  equality-can-have-infinitely-many-inhabitants univ =
    ( ,  , cast  p , cast-preserves-injections p p-injective)
    where
    cast :       
    cast = ≃⇒≡ univ

    cast-preserves-injections :
      {A : Type} (f : A    ) 
      Injective f  Injective (cast  f)
    cast-preserves-injections f inj {x} {y} cast-f-x≡cast-f-y =
      inj (f x               ≡⟨ sym $ _≃_.right-inverse-of (≡≃≃ univ) (f x) 
           ≡⇒≃ (cast (f x))  ≡⟨ cong ≡⇒≃ cast-f-x≡cast-f-y 
           ≡⇒≃ (cast (f y))  ≡⟨ _≃_.right-inverse-of (≡≃≃ univ) (f y) ⟩∎
           f y               )

    swap_and-0 :     
    swap i and-0 zero    = i
    swap i and-0 (suc n) with i Nat.≟ suc n
    ... | yes i≡1+n = zero
    ... | no  i≢1+n = suc n

    swap∘swap :  i n  swap i and-0 (swap i and-0 n)  n
    swap∘swap zero    zero    = refl zero
    swap∘swap (suc i) zero    with i Nat.≟ i
    ... | yes _   = refl 0
    ... | no  i≢i = ⊥-elim $ i≢i (refl i)
    swap∘swap i       (suc n) with i Nat.≟ suc n
    ... | yes i≡1+n = i≡1+n
    ... | no  i≢1+n with i Nat.≟ suc n
    ...   | yes i≡1+n = ⊥-elim $ i≢1+n i≡1+n
    ...   | no  _     = refl (suc n)

    p :     
    p i = Eq.↔⇒≃ record
      { surjection = record
        { logical-equivalence = record { to   = swap i and-0
                                       ; from = swap i and-0
                                       }
        ; right-inverse-of    = swap∘swap i
        }
      ; left-inverse-of = swap∘swap i
      }

    p-injective : Injective p
    p-injective {x = i₁} {y = i₂} p-i₁≡p-i₂ =
      i₁               ≡⟨ refl i₁ 
      swap i₁ and-0 0  ≡⟨ cong  f  f 0) swap-i₁≡swap-i₂ 
      swap i₂ and-0 0  ≡⟨ refl i₂ ⟩∎
      i₂               
      where
      swap-i₁≡swap-i₂ : swap i₁ and-0  swap i₂ and-0
      swap-i₁≡swap-i₂ = cong _≃_.to p-i₁≡p-i₂

------------------------------------------------------------------------
-- A consequence: extensionality for functions

-- The transport theorem.

transport-theorem :
   {p₁ p₂} (P : Type p₁  Type p₂) 
  (resp :  {A B}  A  B  P A  P B) 
  (∀ {A} (p : P A)  resp Eq.id p  p) 
   {A B} (univ : Univalence′ A B) 
  (A≃B : A  B) (p : P A) 
  resp A≃B p  subst P (≃⇒≡ univ A≃B) p
transport-theorem P resp resp-id univ A≃B p =
  resp A≃B p              ≡⟨ sym $ cong  q  resp q p) (right-inverse-of A≃B) 
  resp (to (from A≃B)) p  ≡⟨ elim  {A B} A≡B   p 
                                     resp (≡⇒≃ A≡B) p  subst P A≡B p)
                                   A p 
                                     resp (≡⇒≃ (refl A)) p  ≡⟨ trans (cong  q  resp q p) ≡⇒↝-refl) (resp-id p) 
                                     p                      ≡⟨ sym $ subst-refl P p ⟩∎
                                     subst P (refl A) p     ) _ _ ⟩∎
  subst P (from A≃B) p    
  where open _≃_ (≡≃≃ univ)

opaque

  -- If the univalence axiom holds, then any "resp" function that
  -- preserves identity is an equivalence family.

  resp-is-equivalence :
     {p₁ p₂} (P : Type p₁  Type p₂) 
    (resp :  {A B}  A  B  P A  P B) 
    (∀ {A} (p : P A)  resp Eq.id p  p) 
     {A B} (univ : Univalence′ A B) 
    (A≃B : A  B)  Is-equivalence (resp A≃B)
  resp-is-equivalence P resp resp-id univ A≃B =
    Eq.respects-extensional-equality
       p  sym $ transport-theorem P resp resp-id univ A≃B p)
      (Eq.subst-is-equivalence P (≃⇒≡ univ A≃B))

  -- If f is an equivalence, then (non-dependent) precomposition with
  -- f is also an equivalence (assuming univalence).

  precomposition-is-equivalence :
     { c} {A B : Type } {C : Type c} 
    Univalence′ B A  (A≃B : A  B) 
    Is-equivalence  (g : B  C)  g  _≃_.to A≃B)
  precomposition-is-equivalence {} {c} {C} univ A≃B =
    resp-is-equivalence P resp refl univ (Eq.inverse A≃B)
    where
    P : Type   Type (  c)
    P X = X  C

    resp :  {A B}  A  B  P A  P B
    resp A≃B p = p  _≃_.from A≃B

-- If h is an equivalence, then one can cancel (non-dependent)
-- precompositions with h (assuming univalence).

precompositions-cancel :
   { c} {A B : Type } {C : Type c} 
  Univalence′ B A  (A≃B : A  B) {f g : B  C} 
  let open _≃_ A≃B in
  f  to  g  to  f  g
precompositions-cancel univ A≃B {f} {g} f∘to≡g∘to =
  f            ≡⟨ sym $ left-inverse-of f 
  from (to f)  ≡⟨ cong from f∘to≡g∘to 
  from (to g)  ≡⟨ left-inverse-of g ⟩∎
  g            
  where open _≃_ ( _ , precomposition-is-equivalence univ A≃B )

-- Pairs of equal elements.

_²/≡ :  {}  Type   Type 
A ²/≡ =  λ (x : A)   λ (y : A)  x  y

-- The set of such pairs is isomorphic to the underlying type.

-²/≡↔- :  {a} {A : Type a}  (A ²/≡)  A
-²/≡↔- {A} =
  ( λ (x : A)   λ (y : A)  x  y)  ↝⟨ ∃-cong  _  _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) 
  A ×                                 ↝⟨ ×-right-identity ⟩□
  A                                    

opaque

  -- The univalence axiom implies non-dependent functional
  -- extensionality.

  extensionality :
     {a b} {A : Type a} {B : Type b} 
    Univalence′ (B ²/≡) B 
    {f g : A  B}  (∀ x  f x  g x)  f  g
  extensionality {A} {B} univ {f} {g} f≡g =
    f          ≡⟨ refl f 
    f′  pair  ≡⟨ cong  (h : B ²/≡  B)  h  pair) f′≡g′ 
    g′  pair  ≡⟨ refl g ⟩∎
    g          
    where
    f′ : B ²/≡  B
    f′ = proj₁

    g′ : B ²/≡  B
    g′ = proj₁  proj₂

    f′≡g′ : f′  g′
    f′≡g′ = precompositions-cancel
              univ
              (Eq.↔⇒≃ $ Bijection.inverse -²/≡↔-)
              (refl id)

    pair : A  B ²/≡
    pair x = (f x , g x , f≡g x)

  -- The univalence axiom implies that contractibility is closed under
  -- Π A.

  Π-closure-contractible :
     {b}  Univalence′ (Type b ²/≡) (Type b) 
     {a} {A : Type a} {B : A  Type b} 
    (∀ x  Univalence′ ( b ) (B x)) 
    (∀ x  Contractible (B x))  Contractible ((x : A)  B x)
  Π-closure-contractible {b} univ₁ {A} {B} univ₂ contr =
    subst Contractible A→⊤≡[x:A]→Bx →⊤-contractible
    where
    const-⊤≡B : const ( b )  B
    const-⊤≡B = extensionality univ₁ λ x 
      _≃_.from (≡≃≃ (univ₂ x)) $ Eq.↔⇒≃ $
        Bijection.contractible-isomorphic
          (↑-closure 0 ⊤-contractible) (contr x)

    A→⊤≡[x:A]→Bx : (A   b )  ((x : A)  B x)
    A→⊤≡[x:A]→Bx = cong  X  (x : A)  X x) const-⊤≡B

    →⊤-contractible : Contractible (A   b )
    →⊤-contractible = (_ , λ _  refl _)

  -- Thus we also get extensionality for dependent functions.

  dependent-extensionality′ :
     {b}  Univalence′ (Type b ²/≡) (Type b) 
     {a} {A : Type a} 
    (∀ {B : A  Type b} x  Univalence′ ( b ) (B x)) 
    {B : A  Type b}  Function-extensionality′ A B
  dependent-extensionality′ univ₁ univ₂ =
    _⇔_.to [Π-Contractible→Contractible-Π]⇔Function-extensionality′
      (Π-closure-contractible univ₁ univ₂)

  dependent-extensionality :
     {b} 
    Univalence (lsuc b) 
    Univalence b 
     {a}  Extensionality a b
  dependent-extensionality univ₁ univ₂ =
    _⇔_.from Extensionality⇔Function-extensionality
      (dependent-extensionality′ univ₁  _  univ₂))

------------------------------------------------------------------------
-- Pow and Fam

-- Slightly different variants of Pow and Fam are described in
-- "Specifying interactions with dependent types" by Peter Hancock and
-- Anton Setzer (in APPSEM Workshop on Subtyping & Dependent Types in
-- Programming, DTP'00). The fact that Pow and Fam are logically
-- equivalent is proved in "Programming Interfaces and Basic Topology"
-- by Peter Hancock and Pierre Hyvernat (Annals of Pure and Applied
-- Logic, 2006). The results may be older than this.

-- Pow.

Pow :   {a}  Type a  Type (lsuc (a  ))
Pow  {a} A = A  Type (a  )

-- Fam.

Fam :   {a}  Type a  Type (lsuc (a  ))
Fam  {a} A =  λ (I : Type (a  ))  I  A

-- Pow and Fam are pointwise logically equivalent.

Pow⇔Fam :   {a} {A : Type a} 
          Pow  A  Fam  A
Pow⇔Fam _ = record
  { to   = λ P   P , proj₁
  ; from = λ { (I , f) a   λ i  f i  a }
  }

-- Pow and Fam are pointwise isomorphic (assuming extensionality and
-- univalence).

Pow↔Fam :   {a} {A : Type a} 
          Extensionality a (lsuc (a  )) 
          Univalence (a  ) 
          Pow  A  Fam  A
Pow↔Fam  {A} ext univ = record
  { surjection = record
    { logical-equivalence = Pow⇔Fam 
    ; right-inverse-of    = λ { (I , f) 
        let lemma₁ =
              ( λ a   λ i  f i  a)  ↔⟨ ∃-comm 
              ( λ i   λ a  f i  a)  ↔⟨ ∃-cong  _  _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) 
              I ×                       ↔⟨ ×-right-identity ⟩□
              I                          

            lemma₂ =
              subst  I  I  A) (≃⇒≡ univ lemma₁) proj₁  ≡⟨ sym $ transport-theorem  I  I  A)  eq  _∘ _≃_.from eq) refl univ _ _ 
              proj₁  _≃_.from lemma₁                      ≡⟨ refl _ ⟩∎
              f                                            
        in
        ( λ a   λ i  f i  a) , proj₁  ≡⟨ Σ-≡,≡→≡ (≃⇒≡ univ lemma₁) lemma₂ ⟩∎
        I                         , f       }
    }
  ; left-inverse-of = λ P 
      let lemma = λ a 
            ( λ (i :  P)  proj₁ i  a)  ↔⟨ inverse Σ-assoc 
            ( λ a′  P a′ × a′  a)       ↔⟨ inverse $ ∃-intro _ _ ⟩□
            P a                            
      in
       a   λ (i :  P)  proj₁ i  a)  ≡⟨ apply-ext ext  a  ≃⇒≡ univ (lemma a)) ⟩∎
      P                                    
  }

-- An isomorphism that follows from Pow↔Fam.
--
-- This isomorphism was suggested to me by Paolo Capriotti.

→↔Σ≃Σ :
    {a b} {A : Type a} {B : Type b} 
  Extensionality (a  b  ) (lsuc (a  b  )) 
  Univalence (a  b  ) 
  (A  B)   λ (P : B  Type (a  b  ))  A  Σ B P
→↔Σ≃Σ  {a} {b} {A} {B} ext univ =
  (A  B)                                                    ↝⟨ →-cong₁ (lower-extensionality lzero _ ext) (inverse Bijection.↑↔) 
  ( (b  ) A  B)                                          ↝⟨ inverse ×-left-identity 
   × ( _ A  B)                                            ↝⟨ inverse $ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ×-cong F.id 
  ( λ (A′ : Type ℓ′)  A′   _ A) × ( _ A  B)            ↝⟨ inverse Σ-assoc 
  ( λ (A′ : Type ℓ′)  A′   _ A × ( _ A  B))            ↝⟨ (∃-cong λ _  ∃-cong λ eq  →-cong₁ (lower-extensionality lzero _ ext) (≡⇒≃ (sym eq))) 
  ( λ (A′ : Type ℓ′)  A′   _ A × (A′  B))               ↝⟨ (∃-cong λ _  ×-comm) 
  ( λ (A′ : Type ℓ′)  (A′  B) × A′   _ A)               ↝⟨ Σ-assoc 
  ( λ (p :  λ (A′ : Type ℓ′)  A′  B)  proj₁ p   _ A)  ↝⟨ inverse $ Σ-cong (Pow↔Fam (a  ) (lower-extensionality ℓ′ lzero ext) univ)  _  F.id) 
  ( λ (P : B  Type ℓ′)   P   _ A)                      ↔⟨ (∃-cong λ _  ≡≃≃ univ) 
  ( λ (P : B  Type ℓ′)   P   _ A)                      ↝⟨ (∃-cong λ _  Groupoid.⁻¹-bijection (Eq.groupoid (lower-extensionality ℓ′ _ ext))) 
  ( λ (P : B  Type ℓ′)   _ A   P)                      ↔⟨ (∃-cong λ _ 
                                                                 Eq.≃-preserves (lower-extensionality lzero _ ext) (Eq.↔⇒≃ Bijection.↑↔) F.id) ⟩□
  ( λ (P : B  Type ℓ′)  A   P)                          
  where
  ℓ′ = a  b  

------------------------------------------------------------------------
-- More lemmas

opaque
  unfolding ≡⇒≃-refl

  -- The univalence axiom is propositional (assuming extensionality).

  Univalence′-propositional :
     {}  Extensionality (lsuc ) (lsuc ) 
    {A B : Type }  Is-proposition (Univalence′ A B)
  Univalence′-propositional ext {A} {B} =                  $⟨ Is-equivalence-propositional ext 
    Is-proposition (Is-equivalence (≡⇒≃ {A = A} {B = B}))  ↝⟨ H-level-cong _ 1 (inverse Univalence′≃Is-equivalence-≡⇒≃)  (_  _) ⟩□
    Is-proposition (Univalence′ A B)                       

  Univalence-propositional :
     {}  Extensionality (lsuc ) (lsuc ) 
    Is-proposition (Univalence )
  Univalence-propositional ext =
    implicit-Π-closure ext 1 λ _ 
    implicit-Π-closure ext 1 λ _ 
    Univalence′-propositional ext

  -- ≡⇒≃ commutes with sym/Eq.inverse (assuming extensionality).

  ≡⇒≃-sym :
     {}  Extensionality   
    {A B : Type } (A≡B : A  B) 
    ≡⇒≃ (sym A≡B)  Eq.inverse (≡⇒≃ A≡B)
  ≡⇒≃-sym ext = elim¹

     eq  ≡⇒≃ (sym eq)  Eq.inverse (≡⇒≃ eq))

    (≡⇒≃ (sym (refl _))         ≡⟨ cong ≡⇒≃ sym-refl 
     ≡⇒≃ (refl _)               ≡⟨ ≡⇒≃-refl 
     Eq.id                      ≡⟨ sym $ Groupoid.identity (Eq.groupoid ext) 
     Eq.inverse Eq.id           ≡⟨ cong Eq.inverse $ sym ≡⇒≃-refl ⟩∎
     Eq.inverse (≡⇒≃ (refl _))  )

  -- ≃⇒≡ univ commutes with Eq.inverse/sym (assuming extensionality).

  ≃⇒≡-inverse :
     {} (univ : Univalence )  Extensionality   
    {A B : Type } (A≃B : A  B) 
    ≃⇒≡ univ (Eq.inverse A≃B)  sym (≃⇒≡ univ A≃B)
  ≃⇒≡-inverse univ ext A≃B =
    ≃⇒≡ univ (Eq.inverse A≃B)                   ≡⟨ sym $ cong  p  ≃⇒≡ univ (Eq.inverse p)) (_≃_.right-inverse-of (≡≃≃ univ) _) 
    ≃⇒≡ univ (Eq.inverse (≡⇒≃ (≃⇒≡ univ A≃B)))  ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-sym ext _ 
    ≃⇒≡ univ (≡⇒≃ (sym (≃⇒≡ univ A≃B)))         ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    sym (≃⇒≡ univ A≃B)                          

  -- ≡⇒≃ commutes with trans/_⊚_ (assuming extensionality).

  ≡⇒≃-trans :
     {}  Extensionality   
    {A B C : Type } (A≡B : A  B) (B≡C : B  C) 
    ≡⇒≃ (trans A≡B B≡C)  ≡⇒≃ B≡C  ≡⇒≃ A≡B
  ≡⇒≃-trans ext A≡B = elim¹

     eq  ≡⇒≃ (trans A≡B eq)  ≡⇒≃ eq  ≡⇒≃ A≡B)

    (≡⇒≃ (trans A≡B (refl _))  ≡⟨ cong ≡⇒≃ $ trans-reflʳ _ 
     ≡⇒≃ A≡B                   ≡⟨ sym $ Groupoid.left-identity (Eq.groupoid ext) _ 
     Eq.id  ≡⇒≃ A≡B           ≡⟨ sym $ cong  eq  eq  ≡⇒≃ A≡B) ≡⇒≃-refl ⟩∎
     ≡⇒≃ (refl _)  ≡⇒≃ A≡B    )

  -- ≃⇒≡ univ commutes with _⊚_/flip trans (assuming extensionality).

  ≃⇒≡-∘ :
     {} (univ : Univalence )  Extensionality   
    {A B C : Type } (A≃B : A  B) (B≃C : B  C) 
    ≃⇒≡ univ (B≃C  A≃B)  trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)
  ≃⇒≡-∘ univ ext A≃B B≃C =
    ≃⇒≡ univ (B≃C  A≃B)                                  ≡⟨ sym $ cong₂  p q  ≃⇒≡ univ (p  q)) (_≃_.right-inverse-of (≡≃≃ univ) _)
                                                                                                    (_≃_.right-inverse-of (≡≃≃ univ) _) 
    ≃⇒≡ univ (≡⇒≃ (≃⇒≡ univ B≃C)  ≡⇒≃ (≃⇒≡ univ A≃B))    ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-trans ext _ _ 
    ≃⇒≡ univ (≡⇒≃ (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)))  ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
    trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)                   

  -- A variant of the transport theorem.

  transport-theorem′ :
     {a p r} {A : Type a}
    (P : A  Type p) (R : A  A  Type r)
    (≡↠R :  {x y}  (x  y)  R x y)
    (resp :  {x y}  R x y  P x  P y) 
    (∀ x p  resp (_↠_.to ≡↠R (refl x)) p  p) 
     {x y} (r : R x y) (p : P x) 
    resp r p  subst P (_↠_.from ≡↠R r) p
  transport-theorem′ P R ≡↠R resp hyp r p =
    resp r p              ≡⟨ sym $ cong  r  resp r p) (right-inverse-of r) 
    resp (to (from r)) p  ≡⟨ elim  {x y} x≡y   p 
                                     resp (_↠_.to ≡↠R x≡y) p  subst P x≡y p)
                                   x p 
                                     resp (_↠_.to ≡↠R (refl x)) p  ≡⟨ hyp x p 
                                     p                             ≡⟨ sym $ subst-refl P p ⟩∎
                                     subst P (refl x) p            ) _ _ ⟩∎
    subst P (from r) p    
    where open _↠_ ≡↠R

  -- Simplification (?) lemma for transport-theorem′.

  transport-theorem′-refl :
     {a p r} {A : Type a}
    (P : A  Type p) (R : A  A  Type r)
    (≡≃R :  {x y}  (x  y)  R x y)
    (resp :  {x y}  R x y  P x  P y) 
    (resp-refl :  x p  resp (_≃_.to ≡≃R (refl x)) p  p) 
     {x} (p : P x) 
    transport-theorem′ P R (_≃_.surjection ≡≃R) resp resp-refl
                       (_≃_.to ≡≃R (refl x)) p 
    trans (trans (resp-refl x p) (sym $ subst-refl P p))
          (sym $ cong  eq  subst P eq p)
                      (_≃_.left-inverse-of ≡≃R (refl x)))
  transport-theorem′-refl P R ≡≃R resp resp-refl {x} p =

    let body = λ x p  trans (resp-refl x p) (sym $ subst-refl P p)

        lemma =
          trans (sym $ cong  r  resp (to r) p) $ refl (refl x))
                (elim  {x y} x≡y 
                          p  resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                       x p  trans (resp-refl x p)
                                     (sym $ subst-refl P p))
                      (refl x) p)                                        ≡⟨ cong₂  q r  trans q (r p))
                                                                                  (sym $ cong-sym  r  resp (to r) p) _)
                                                                                  (elim-refl  {x y} x≡y   p 
                                                                                                resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p) _) 
          trans (cong  r  resp (to r) p) $ sym $ refl (refl x))
                (body x p)                                               ≡⟨ cong  q  trans (cong  r  resp (to r) p) q) (body x p))
                                                                                 sym-refl 
          trans (cong  r  resp (to r) p) $ refl (refl x)) (body x p)  ≡⟨ cong  q  trans q (body x p)) $
                                                                                 cong-refl  r  resp (to r) p) 
          trans (refl (resp (to (refl x)) p)) (body x p)                 ≡⟨ trans-reflˡ _ 

          body x p                                                       ≡⟨ sym $ trans-reflʳ _ 

          trans (body x p) (refl (subst P (refl x) p))                   ≡⟨ cong (trans (body x p)) $ sym $
                                                                                 cong-refl  eq  subst P eq p) 
          trans (body x p)
                (cong  eq  subst P eq p) (refl (refl x)))             ≡⟨ cong (trans (body x p)  cong  eq  subst P eq p)) $
                                                                                 sym sym-refl 
          trans (body x p)
                (cong  eq  subst P eq p) (sym (refl (refl x))))       ≡⟨ cong (trans (body x p)) $ cong-sym  eq  subst P eq p) _ ⟩∎

          trans (body x p)
                (sym $ cong  eq  subst P eq p) (refl (refl x)))       
    in

    trans (sym $ cong  r  resp r p) $ right-inverse-of (to (refl x)))
          (elim  {x y} x≡y 
                    p  resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ cong  eq  trans (sym $ cong  r  resp r p) eq)
                                                                                                (elim  {x y} x≡y   p 
                                                                                                         resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                                                                                                      body (from (to (refl x))) p)) $
                                                                                  sym $ left-right-lemma (refl x) 
    trans (sym $ cong  r  resp r p) $ cong to $
             left-inverse-of (refl x))
          (elim  {x y} x≡y 
                    p  resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ cong  eq  trans (sym eq)
                                                                                                (elim  {x y} x≡y   p 
                                                                                                         resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                                                                                                      body (from (to (refl x))) p)) $
                                                                                  cong-∘  r  resp r p) to _ 
    trans (sym $ cong  r  resp (to r) p) $ left-inverse-of (refl x))
          (elim  {x y} x≡y 
                    p  resp (_≃_.to ≡≃R x≡y) p  subst P x≡y p)
                body (from (to (refl x))) p)                              ≡⟨ elim₁  {q} eq  trans (sym $ cong  r  resp (to r) p) eq)
                                                                                                     (elim  {x y} x≡y   p 
                                                                                                              resp (_≃_.to ≡≃R x≡y) p 
                                                                                                              subst P x≡y p)
                                                                                                           body q p) 
                                                                                               trans (body x p)
                                                                                                     (sym $ cong  eq  subst P eq p) eq))
                                                                                   lemma
                                                                                   (left-inverse-of (refl x)) ⟩∎

    trans (body x p)
          (sym $ cong  eq  subst P eq p) (left-inverse-of (refl x)))   

    where open _≃_ ≡≃R

  -- Simplification (?) lemma for transport-theorem.

  transport-theorem-≡⇒≃-refl :
     {p₁ p₂} (P : Type p₁  Type p₂)
    (resp :  {A B}  A  B  P A  P B)
    (resp-id :  {A} (p : P A)  resp Eq.id p  p)
    (univ : Univalence p₁) {A} (p : P A) 
    transport-theorem P resp resp-id univ (≡⇒≃ (refl A)) p 
    trans (trans (trans (cong  eq  resp eq p) ≡⇒≃-refl)
                    (resp-id p))
             (sym $ subst-refl P p))
      (sym $ cong  eq  subst P eq p)
                  (_≃_.left-inverse-of (≡≃≃ univ) (refl A)))
  transport-theorem-≡⇒≃-refl P resp resp-id univ {A} p =
    transport-theorem′-refl P _≃_ (≡≃≃ univ) resp
       _ p  trans (cong  eq  resp eq p) ≡⇒≃-refl) (resp-id p)) p

  -- A variant of resp-is-equivalence.

  resp-is-equivalence′ :
     {a p r} {A : Type a}
    (P : A  Type p) (R : A  A  Type r)
    (≡↠R :  {x y}  (x  y)  R x y)
    (resp :  {x y}  R x y  P x  P y) 
    (∀ x p  resp (_↠_.to ≡↠R (refl x)) p  p) 
     {x y} (r : R x y)  Is-equivalence (resp r)
  resp-is-equivalence′ P R ≡↠R resp hyp r =
    Eq.respects-extensional-equality
       p  sym $ transport-theorem′ P R ≡↠R resp hyp r p)
      (Eq.subst-is-equivalence P (_↠_.from ≡↠R r))

  -- A lemma relating ≃⇒≡, →-cong and cong₂.

  ≃⇒≡-→-cong :
     {} {A₁ A₂ B₁ B₂ : Type }
    (ext : Extensionality  ) 
    (univ : Univalence )
    (A₁≃A₂ : A₁  A₂) (B₁≃B₂ : B₁  B₂) 
    ≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂) 
      cong₂  A B  A  B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂)
  ≃⇒≡-→-cong {A₂} {B₁} ext univ A₁≃A₂ B₁≃B₂ =
    ≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂)                        ≡⟨ cong (≃⇒≡ univ) (Eq.lift-equality ext lemma) 

    ≃⇒≡ univ (≡⇒≃ (cong₂  A B  A  B) (≃⇒≡ univ A₁≃A₂)
                                         (≃⇒≡ univ B₁≃B₂)))  ≡⟨ left-inverse-of (≡≃≃ univ) _ ⟩∎

    cong₂  A B  A  B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂)  
    where
    open _≃_

    lemma :
       f  to B₁≃B₂  f  from A₁≃A₂) 
      to (≡⇒≃ (cong₂  A B  A  B) (≃⇒≡ univ A₁≃A₂)
                                     (≃⇒≡ univ B₁≃B₂)))
    lemma =
       f  to B₁≃B₂  f  from A₁≃A₂)                  ≡⟨ apply-ext ext  _  transport-theorem  B  A₂  B)  A≃B g  _≃_.to A≃B  g)
                                                                                                   refl univ B₁≃B₂ _) 
      subst  B  A₂  B) (≃⇒≡ univ B₁≃B₂) 
       f  f  from A₁≃A₂)                             ≡⟨ cong (_∘_ (subst  B  A₂  B) (≃⇒≡ univ B₁≃B₂))) (apply-ext ext λ f 
                                                              transport-theorem  A  A  B₁)  A≃B g  g  _≃_.from A≃B) refl univ A₁≃A₂ f) 
      subst  B  A₂  B) (≃⇒≡ univ B₁≃B₂) 
      subst  A  A  B₁) (≃⇒≡ univ A₁≃A₂)              ≡⟨ cong₂  g h f  g (h f))
                                                              (apply-ext ext $ subst-in-terms-of-≡⇒↝ equivalence _  B  A₂  B))
                                                              (apply-ext ext $ subst-in-terms-of-≡⇒↝ equivalence _  A  A  B₁)) 
      to (≡⇒≃ (cong  B  A₂  B) (≃⇒≡ univ B₁≃B₂))) 
      to (≡⇒≃ (cong  A  A  B₁) (≃⇒≡ univ A₁≃A₂)))    ≡⟨⟩

      to (≡⇒≃ (cong  B  A₂  B) (≃⇒≡ univ B₁≃B₂)) 
          ≡⇒≃ (cong  A  A  B₁) (≃⇒≡ univ A₁≃A₂)))    ≡⟨ cong to $ sym $ ≡⇒≃-trans ext _ _ ⟩∎

      to (≡⇒≃ (cong₂  A B  A  B) (≃⇒≡ univ A₁≃A₂)
                                     (≃⇒≡ univ B₁≃B₂)))  

  -- One can sometimes push cong through ≃⇒≡ (assuming
  -- extensionality).

  cong-≃⇒≡ :
     { p} {A B : Type } {A≃B : A  B} 
    Extensionality p p 
    (univ₁ : Univalence )
    (univ₂ : Univalence p)
    (P : Type   Type p)
    (P-cong :  {A B}  A  B  P A  P B) 
    (∀ {A} (p : P A)  _≃_.to (P-cong Eq.id) p  p) 
    cong P (≃⇒≡ univ₁ A≃B)  ≃⇒≡ univ₂ (P-cong A≃B)
  cong-≃⇒≡ {A≃B} ext univ₁ univ₂ P P-cong P-cong-id =
    cong P (≃⇒≡ univ₁ A≃B)                    ≡⟨ sym $ _≃_.left-inverse-of (≡≃≃ univ₂) _ 
    ≃⇒≡ univ₂ (≡⇒≃ (cong P (≃⇒≡ univ₁ A≃B)))  ≡⟨ cong (≃⇒≡ univ₂) $ Eq.lift-equality ext lemma ⟩∎
    ≃⇒≡ univ₂ (P-cong A≃B)                    
    where
    lemma : ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B))  _≃_.to (P-cong A≃B)
    lemma = apply-ext ext λ x 
      ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B)) x  ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence _ P x 
      subst P (≃⇒≡ univ₁ A≃B) x       ≡⟨ sym $ transport-theorem P (_≃_.to  P-cong) P-cong-id univ₁ A≃B x ⟩∎
      _≃_.to (P-cong A≃B) x           

  -- Any "resp" function that preserves identity also preserves
  -- compositions (assuming univalence and extensionality).

  resp-preserves-compositions :
     {p₁ p₂} (P : Type p₁  Type p₂) 
    (resp :  {A B}  A  B  P A  P B) 
    (∀ {A} (p : P A)  resp Eq.id p  p) 
    Univalence p₁  Extensionality p₁ p₁ 
     {A B C} (A≃B : A  B) (B≃C : B  C) p 
    resp (B≃C  A≃B) p  (resp B≃C  resp A≃B) p
  resp-preserves-compositions P resp resp-id univ ext A≃B B≃C p =
    resp (B≃C  A≃B) p                                 ≡⟨ transport-theorem P resp resp-id univ _ _ 
    subst P (≃⇒≡ univ (B≃C  A≃B)) p                   ≡⟨ cong  eq  subst P eq p) $ ≃⇒≡-∘ univ ext A≃B B≃C 
    subst P (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)) p    ≡⟨ sym $ subst-subst P _ _ _ 
    subst P (≃⇒≡ univ B≃C) (subst P (≃⇒≡ univ A≃B) p)  ≡⟨ sym $ transport-theorem P resp resp-id univ _ _ 
    resp B≃C (subst P (≃⇒≡ univ A≃B) p)                ≡⟨ sym $ cong (resp _) $ transport-theorem P resp resp-id univ _ _ ⟩∎
    resp B≃C (resp A≃B p)                              

  -- Any "resp" function that preserves identity also preserves
  -- inverses (assuming univalence and extensionality).

  resp-preserves-inverses :
     {p₁ p₂} (P : Type p₁  Type p₂) 
    (resp :  {A B}  A  B  P A  P B) 
    (∀ {A} (p : P A)  resp Eq.id p  p) 
    Univalence p₁  Extensionality p₁ p₁ 
     {A B} (A≃B : A  B) p q 
    resp A≃B p  q  resp (inverse A≃B) q  p
  resp-preserves-inverses P resp resp-id univ ext A≃B p q eq =
    let lemma =
          q                                     ≡⟨ sym eq 
          resp A≃B p                            ≡⟨ transport-theorem P resp resp-id univ _ _ 
          subst P (≃⇒≡ univ A≃B) p              ≡⟨ cong  eq  subst P eq p) $ sym $ sym-sym _ ⟩∎
          subst P (sym (sym (≃⇒≡ univ A≃B))) p  
    in

    resp (inverse A≃B) q                                                 ≡⟨ transport-theorem P resp resp-id univ _ _ 
    subst P (≃⇒≡ univ (inverse A≃B)) q                                   ≡⟨ cong  eq  subst P eq q) $ ≃⇒≡-inverse univ ext A≃B 
    subst P (sym (≃⇒≡ univ A≃B)) q                                       ≡⟨ cong (subst P (sym (≃⇒≡ univ A≃B))) lemma 
    subst P (sym (≃⇒≡ univ A≃B)) (subst P (sym (sym (≃⇒≡ univ A≃B))) p)  ≡⟨ subst-subst-sym P _ _ ⟩∎
    p                                                                    

-- Equality preserves equivalences (assuming extensionality and
-- univalence).

≡-preserves-≃ :
   {ℓ₁ ℓ₂}
    {A₁ : Type ℓ₁} {A₂ : Type ℓ₂} {B₁ : Type ℓ₁} {B₂ : Type ℓ₂} 
  Extensionality (ℓ₁  ℓ₂) (ℓ₁  ℓ₂) 
  Univalence′ A₁ B₁ 
  Univalence′ A₂ B₂ 
  A₁  A₂  B₁  B₂  (A₁  B₁)  (A₂  B₂)
≡-preserves-≃ {ℓ₁} {ℓ₂} {A₁} {A₂} {B₁} {B₂}
              ext univ₁ univ₂ A₁≃A₂ B₁≃B₂ = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  })
  where
  to = λ A₁≡B₁  ≃⇒≡ univ₂ (
    A₂  ↝⟨ inverse A₁≃A₂ 
    A₁  ↝⟨ ≡⇒≃ A₁≡B₁ 
    B₁  ↝⟨ B₁≃B₂ ⟩□
    B₂  )

  from = λ A₂≡B₂  ≃⇒≡ univ₁ (
    A₁  ↝⟨ A₁≃A₂ 
    A₂  ↝⟨ ≡⇒≃ A₂≡B₂ 
    B₂  ↝⟨ inverse B₁≃B₂ ⟩□
    B₁  )

  opaque

    to∘from :  eq  to (from eq)  eq
    to∘from A₂≡B₂ =
      let ext₂ = lower-extensionality ℓ₁ ℓ₁ ext in

      _≃_.to (Eq.≃-≡ (≡≃≃ univ₂)) (Eq.lift-equality ext₂ (

        ≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂  ≡⇒≃ (≃⇒≡ univ₁ ((inverse B₁≃B₂ 
                             ≡⇒≃ A₂≡B₂)  A₁≃A₂)))  inverse A₁≃A₂))  ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₂) _ 

        (_≃_.to B₁≃B₂ 
         ≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂  ≡⇒≃ A₂≡B₂)  A₁≃A₂)) 
         _≃_.from A₁≃A₂)                                              ≡⟨ cong  eq  _≃_.to B₁≃B₂  _≃_.to eq  _≃_.from A₁≃A₂) $
                                                                           _≃_.right-inverse-of (≡≃≃ univ₁) _ 
        ((_≃_.to B₁≃B₂  _≃_.from B₁≃B₂)  ≡⇒→ A₂≡B₂ 
         (_≃_.to A₁≃A₂  _≃_.from A₁≃A₂))                             ≡⟨ cong₂  f g  f  ≡⇒→ A₂≡B₂  g)
                                                                               (apply-ext ext₂ $ _≃_.right-inverse-of B₁≃B₂)
                                                                               (apply-ext ext₂ $ _≃_.right-inverse-of A₁≃A₂) ⟩∎
        ≡⇒→ A₂≡B₂                                                     ))

    from∘to :  eq  from (to eq)  eq
    from∘to A₁≡B₁ =
      let ext₁ = lower-extensionality ℓ₂ ℓ₂ ext in

      _≃_.to (Eq.≃-≡ (≡≃≃ univ₁)) (Eq.lift-equality ext₁ (

        ≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂  ≡⇒≃ (≃⇒≡ univ₂ ((B₁≃B₂ 
                             ≡⇒≃ A₁≡B₁)  inverse A₁≃A₂)))  A₁≃A₂))  ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₁) _ 

        (_≃_.from B₁≃B₂ 
         ≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂  ≡⇒≃ A₁≡B₁)  inverse A₁≃A₂)) 
         _≃_.to A₁≃A₂)                                                ≡⟨ cong  eq  _≃_.from B₁≃B₂  _≃_.to eq  _≃_.to A₁≃A₂) $
                                                                           _≃_.right-inverse-of (≡≃≃ univ₂) _ 
        ((_≃_.from B₁≃B₂  _≃_.to B₁≃B₂)  ≡⇒→ A₁≡B₁ 
         (_≃_.from A₁≃A₂  _≃_.to A₁≃A₂))                             ≡⟨ cong₂  f g  f  ≡⇒→ A₁≡B₁  g)
                                                                               (apply-ext ext₁ $ _≃_.left-inverse-of B₁≃B₂)
                                                                               (apply-ext ext₁ $ _≃_.left-inverse-of A₁≃A₂) ⟩∎
        ≡⇒→ A₁≡B₁                                                     ))

-- Singletons expressed using equivalences instead of equalities,
-- where the types are required to live in the same universe, are
-- contractible (assuming univalence).

singleton-with-≃-contractible :
   {b} {B : Type b} 
  Univalence b 
  Contractible ( λ (A : Type b)  A  B)
singleton-with-≃-contractible univ =
  H-level.respects-surjection
    (∃-cong λ _  _≃_.surjection (≡≃≃ univ))
    0
    (singleton-contractible _)

other-singleton-with-≃-contractible :
   {a} {A : Type a} 
  Univalence a 
  Contractible ( λ (B : Type a)  A  B)
other-singleton-with-≃-contractible univ =
  H-level.respects-surjection
    (∃-cong λ _  _≃_.surjection (≡≃≃ univ))
    0
    (other-singleton-contractible _)

-- Singletons expressed using equivalences instead of equalities are
-- isomorphic to the unit type (assuming extensionality and
-- univalence).

singleton-with-≃-↔-⊤ :
   {a b} {B : Type b} 
  Extensionality (a  b) (a  b) 
  Univalence (a  b) 
  ( λ (A : Type (a  b))  A  B)  
singleton-with-≃-↔-⊤ {a} {B} ext univ =
  ( λ A  A  B)      ↝⟨ inverse (∃-cong λ _  Eq.≃-preserves-bijections ext F.id Bijection.↑↔) 
  ( λ A  A   a B)  ↔⟨ inverse (∃-cong λ _  ≡≃≃ univ) 
  ( λ A  A   a B)  ↝⟨ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ⟩□
                      

other-singleton-with-≃-↔-⊤ :
   {a b} {A : Type a} 
  Extensionality (a  b) (a  b) 
  Univalence (a  b) 
  ( λ (B : Type (a  b))  A  B)  
other-singleton-with-≃-↔-⊤ {b} {A} ext univ =
  ( λ B  A  B)  ↝⟨ (∃-cong λ _  Eq.inverse-isomorphism ext) 
  ( λ B  B  A)  ↝⟨ singleton-with-≃-↔-⊤ {a = b} ext univ ⟩□
                  

-- Variants of the two lemmas above.

singleton-with-Π-≃-≃-⊤ :
   {a q} {A : Type a} {Q : A  Type q} 
  Extensionality a (lsuc q) 
  Univalence q 
  ( λ (P : A  Type q)   x  P x  Q x)  
singleton-with-Π-≃-≃-⊤ {a} {q} {A} {Q} ext univ =
  ( λ (P : A  Type q)   x  P x  Q x)  ↝⟨ (inverse $ ∃-cong λ _  ∀-cong ext λ _  ≡≃≃ univ) 
  ( λ (P : A  Type q)   x  P x  Q x)  ↝⟨ (∃-cong λ _  Eq.extensionality-isomorphism ext) 
  ( λ (P : A  Type q)  P  Q)            ↔⟨ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ⟩□
                                           

other-singleton-with-Π-≃-≃-⊤ :
   {a p} {A : Type a} {P : A  Type p} 
  Extensionality a (lsuc p) 
  Univalence p 
  ( λ (Q : A  Type p)   x  P x  Q x)  
other-singleton-with-Π-≃-≃-⊤ {a} {p} {A} {P} ext univ =
  ( λ (Q : A  Type p)   x  P x  Q x)  ↝⟨ (inverse $ ∃-cong λ _  ∀-cong ext λ _  ≡≃≃ univ) 
  ( λ (Q : A  Type p)   x  P x  Q x)  ↝⟨ (∃-cong λ _  Eq.extensionality-isomorphism ext) 
  ( λ (Q : A  Type p)  P  Q)            ↔⟨ _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _) ⟩□
                                           

-- ∃ Contractible is isomorphic to the unit type (assuming
-- extensionality and univalence).

∃Contractible↔⊤ :
   {a} 
  Extensionality a a 
  Univalence a 
  ( λ (A : Type a)  Contractible A)  
∃Contractible↔⊤ ext univ =
  ( λ A  Contractible A)  ↝⟨ (∃-cong λ _  contractible↔≃⊤ ext) 
  ( λ A  A  )           ↝⟨ singleton-with-≃-↔-⊤ ext univ 
                           

-- If two types have a certain h-level, then the type of equalities
-- between these types also has the given h-level (assuming
-- extensionality and univalence).

H-level-H-level-≡ :
   {a} {A₁ A₂ : Type a} 
  Extensionality a a 
  Univalence′ A₁ A₂ 
   n  H-level n A₁  H-level n A₂  H-level n (A₁  A₂)
H-level-H-level-≡ {A₁} {A₂} ext univ n = curry (
  H-level n A₁ × H-level n A₂  ↝⟨ uncurry (Eq.h-level-closure ext n) 
  H-level n (A₁  A₂)          ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) n 
  H-level n (A₁  A₂)          )

-- If a type has a certain positive h-level, then the types of
-- equalities between this type and other types also has the given
-- h-level (assuming extensionality and univalence).

H-level-H-level-≡ˡ :
   {a} {A₁ A₂ : Type a} 
  Extensionality a a 
  Univalence′ A₁ A₂ 
   n  H-level (1 + n) A₁  H-level (1 + n) (A₁  A₂)
H-level-H-level-≡ˡ {A₁} {A₂} ext univ n =
  H-level (1 + n) A₁         ↝⟨ Eq.left-closure ext n 
  H-level (1 + n) (A₁  A₂)  ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) 
  H-level (1 + n) (A₁  A₂)  

H-level-H-level-≡ʳ :
   {a} {A₁ A₂ : Type a} 
  Extensionality a a 
  Univalence′ A₁ A₂ 
   n  H-level (1 + n) A₂  H-level (1 + n) (A₁  A₂)
H-level-H-level-≡ʳ {A₁} {A₂} ext univ n =
  H-level (1 + n) A₂         ↝⟨ Eq.right-closure ext n 
  H-level (1 + n) (A₁  A₂)  ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) 
  H-level (1 + n) (A₁  A₂)  

-- ∃ λ A → H-level n A has h-level 1 + n (assuming extensionality and
-- univalence).

∃-H-level-H-level-1+ :
   {a} 
  Extensionality a a 
  Univalence a 
   n  H-level (1 + n) ( λ (A : Type a)  H-level n A)
∃-H-level-H-level-1+ ext univ n = ≡↔+ _ _ λ { (A₁ , h₁) (A₂ , h₂) 
                                     $⟨ h₁ , h₂ 
  H-level n A₁ × H-level n A₂        ↝⟨ uncurry (H-level-H-level-≡ ext univ n) 
  H-level n (A₁  A₂)                ↝⟨ H-level.respects-surjection
                                          (_↔_.surjection $ ignore-propositional-component
                                                              (H-level-propositional ext _)) n ⟩□
  H-level n ((A₁ , h₁)  (A₂ , h₂))   }

-- ∃ λ A → Is-proposition A is a set (assuming extensionality and
-- propositional extensionality).

Is-set-∃-Is-proposition :
   {a} 
  Extensionality (lsuc a) (lsuc a) 
  Propositional-extensionality a 
  Is-set ( λ (A : Type a)  Is-proposition A)
Is-set-∃-Is-proposition ext prop-ext
                        {x = A₁ , A₁-prop} {y = A₂ , A₂-prop} =
                                                    $⟨ _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
                                                         prop-ext A₁-prop A₂-prop 
  Univalence′ A₁ A₂                                 ↝⟨  univ  H-level-H-level-≡ ext′ univ 1 A₁-prop A₂-prop) 
  Is-proposition (A₁  A₂)                          ↝⟨ H-level.respects-surjection
                                                         (_↔_.surjection $ ignore-propositional-component
                                                                             (H-level-propositional ext′ 1)) 1 ⟩□
  Is-proposition ((A₁ , A₁-prop)  (A₂ , A₂-prop))  
  where
  ext′ = lower-extensionality _ _ ext

-- ∃ λ A → Contractible A is contractible (assuming extensionality
-- and propositional extensionality).

Contractible-∃-Contractible :
   {a} 
  Extensionality (lsuc a) (lsuc a) 
  Propositional-extensionality a 
  Contractible ( λ (A : Type a)  Contractible A)
Contractible-∃-Contractible ext prop-ext =
  propositional⇒inhabited⇒contractible
     (A₁ , c₁) (A₂ , c₂)    $⟨ _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
                                    prop-ext (H-level.mono₁ 0 c₁) (H-level.mono₁ 0 c₂) 
       Univalence′ A₁ A₂       →⟨  univ  H-level-H-level-≡ ext′ univ 0 c₁ c₂) 
       Contractible (A₁  A₂)  →⟨ proj₁ 
       A₁  A₂                 ↔⟨ ignore-propositional-component (H-level-propositional ext′ 0) ⟩□
       (A₁ , c₁)  (A₂ , c₂)   )
    ( _  , ↑-closure 0 ⊤-contractible)
  where
  ext′ = lower-extensionality _ _ ext

-- ∃ λ A → H-level n A does not in general have h-level n.
--
-- (Kraus and Sattler show that, for all n,
-- ∃ λ (A : Set (# n)) → H-level (2 + n) A does not have h-level
-- 2 + n, assuming univalence. See "Higher Homotopies in a Hierarchy
-- of Univalent Universes".)

¬-∃-H-level-H-level :
   {a} 
   λ n  ¬ H-level n ( λ (A : Type a)  H-level n A)
¬-∃-H-level-H-level =
  1 ,
  ( Is-proposition ( λ A  Is-proposition A)               ↔⟨⟩
    ((p q :  λ A  Is-proposition A)  p  q)              ↝⟨  f p q  cong proj₁ (f p q)) 
    ((p q :  λ A  Is-proposition A)  proj₁ p  proj₁ q)  ↝⟨ (_$ ( , ⊥-propositional)) 
                                                               (_$ ( _  , ↑-closure 1 (mono₁ 0 ⊤-contractible))) 
     _                                                  ↝⟨ flip (subst id) _ 
                                                           ↝⟨ ⊥-elim ⟩□
    ⊥₀                                                      )

-- A certain type of uninhabited types is isomorphic to the unit type
-- (assuming extensionality and univalence).

∃¬↔⊤ :
   {a} 
  Extensionality a a 
  Univalence a 
  ( λ (A : Type a)  ¬ A)  
∃¬↔⊤ ext univ =
  ( λ A  ¬ A)     ↝⟨ inverse (∃-cong λ _  ≃⊥≃¬ ext) 
  ( λ A  A  ⊥₀)  ↔⟨ singleton-with-≃-↔-⊤ ext univ 
                   

-- The following three proofs are taken from or variants of proofs in
-- "Higher Homotopies in a Hierarchy of Univalent Universes" by Kraus
-- and Sattler (Section 3).

-- There is a function which, despite having the same type, is not
-- equal to a certain instance of reflexivity (assuming extensionality
-- and univalence).

∃≢refl :
  Extensionality (# 1) (# 1) 
  Univalence (# 0) 
   λ (A : Type₁)   λ (f : (x : A)  x  x)  f  refl
∃≢refl ext univ =
    ( λ (A : Type)  A  A)
  , _↔_.from iso f
  , (_↔_.from iso f  refl                                      ↝⟨ cong (_↔_.to iso) 

     _↔_.to iso (_↔_.from iso f)  _↔_.to iso refl              ↝⟨  eq  f                            ≡⟨ sym (_↔_.right-inverse-of iso f) 
                                                                           _↔_.to iso (_↔_.from iso f)  ≡⟨ eq ⟩∎
                                                                           _↔_.to iso refl              ) 
     f  _↔_.to iso refl                                        ↝⟨ cong  f  proj₁ (f Bool (swap-as-an-equality univ))) 

     swap-as-an-equality univ  proj₁ (_↔_.to iso refl Bool _)  ↝⟨  eq  swap-as-an-equality univ        ≡⟨ eq 
                                                                           proj₁ (_↔_.to iso refl Bool _)  ≡⟨ cong proj₁ Σ-≡,≡←≡-refl ⟩∎
                                                                           refl Bool                       ) 

     swap-as-an-equality univ  refl Bool                       ↝⟨ swap≢refl univ ⟩□

                                                               )
  where
  f = λ A p  p , refl (trans p p)

  iso =
    ((p :  λ A  A  A)  p  p)                      ↝⟨ currying 

    (∀ A (p : A  A)  (A , p)  (A , p))              ↝⟨ (∀-cong ext λ _  ∀-cong ext λ _ 
                                                             inverse $ Bijection.Σ-≡,≡↔≡ {a = # 1}) 
    ((A : Type) (p : A  A) 
        λ (q : A  A)  subst  A  A  A) q p  p)  ↝⟨ (∀-cong ext λ _  ∀-cong ext λ _ 
                                                             ∃-cong λ _  ≡⇒↝ _ [subst≡]≡[trans≡trans]) ⟩□
    ((A : Type) (p : A  A) 
        λ (q : A  A)  trans p q  trans q p)        

-- The type (a : A) → a ≡ a is not necessarily a proposition (assuming
-- extensionality and univalence).

¬-type-of-refl-propositional :
  Extensionality (# 1) (# 1) 
  Univalence (# 0) 
   λ (A : Type₁)  ¬ Is-proposition ((a : A)  a  a)
¬-type-of-refl-propositional ext univ =
  let A , f , f≢refl = ∃≢refl ext univ in
  A ,
  (Is-proposition (∀ x  x  x)  ↝⟨  irr  irr _ _) 
   f  refl                      ↝⟨ f≢refl ⟩□
                                )

-- Type₁ does not have h-level 3 (assuming extensionality and
-- univalence).

¬-Type₁-groupoid :
  Extensionality (# 1) (# 1) 
  Univalence (# 1) 
  Univalence (# 0) 
  ¬ H-level 3 Type₁
¬-Type₁-groupoid ext univ₁ univ₀ =
  let L = _ in

  H-level 3 Type₁                       ↝⟨  h  h) 
  Is-set (L  L)                        ↝⟨ H-level.respects-surjection (_≃_.surjection $ ≡≃≃ univ₁) 2 
  Is-set (L  L)                        ↝⟨  h  h) 
  Is-proposition (F.id  F.id)          ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Eq.≃-as-Σ) 1 
  Is-proposition ((id , _)  (id , _))  ↝⟨ H-level.respects-surjection
                                             (_↔_.surjection $ inverse $ ignore-propositional-component (Is-equivalence-propositional ext)) 1 
  Is-proposition (id  id)              ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ Eq.extensionality-isomorphism ext) 1 
  Is-proposition ((l : L)  l  l)      ↝⟨ proj₂ $ ¬-type-of-refl-propositional ext univ₀ ⟩□
                                       

-- For propositional types there is a split surjection from equality
-- to logical equivalence (assuming univalence).

≡↠⇔ :  {} {A B : Type } 
      Univalence′ A B 
      Is-proposition A  Is-proposition B 
      (A  B)  (A  B)
≡↠⇔ {A} {B} univ A-prop B-prop =
  A  B  ↔⟨ ≡≃≃ univ 
  A  B  ↝⟨ Eq.≃↠⇔ A-prop B-prop ⟩□
  A  B  

-- For propositional types logical equivalence is isomorphic to
-- equality (assuming extensionality and univalence).

⇔↔≡ :  {} {A B : Type } 
      Extensionality   
      Univalence′ A B 
      Is-proposition A  Is-proposition B 
      (A  B)  (A  B)
⇔↔≡ {A} {B} ext univ A-prop B-prop =
  A  B  ↝⟨ Eq.⇔↔≃ ext A-prop B-prop 
  A  B  ↔⟨ inverse $ ≡≃≃ univ ⟩□
  A  B  

-- A variant of the previous statement.

⇔↔≡′ :  {} {A B : Proposition } 
       Extensionality   
       Univalence′ (proj₁ A) (proj₁ B) 
       (proj₁ A  proj₁ B)  (A  B)
⇔↔≡′ {A} {B} ext univ =
  proj₁ A  proj₁ B  ↝⟨ ⇔↔≡ ext univ (proj₂ A) (proj₂ B) 
  proj₁ A  proj₁ B  ↝⟨ ignore-propositional-component (H-level-propositional ext 1) ⟩□
  A  B              

-- A variant of the previous statement.

⇔↔≡″ :  {} {A B : Proposition } 
       Extensionality (lsuc ) (lsuc ) 
       Propositional-extensionality  
       (proj₁ A  proj₁ B)  (A  B)
⇔↔≡″ {} {A} {B} ext =
  Propositional-extensionality    ↝⟨  prop-ext  _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
                                                           prop-ext (proj₂ A) (proj₂ B)) 
  Univalence′ (proj₁ A) (proj₁ B)  ↝⟨ ⇔↔≡′ (lower-extensionality _ _ ext) ⟩□
  (proj₁ A  proj₁ B)  (A  B)    

------------------------------------------------------------------------
-- Variants of J for equivalences

-- Two variants of the J rule for equivalences, along with
-- "computation" rules.
--
-- The types of the eliminators are similar to the statement of
-- Corollary 5.8.5 from the HoTT book (where the motive takes two type
-- arguments). The type and code of ≃-elim₁ are based on code from the
-- cubical library written by Matthew Yacavone, which was possibly
-- based on code written by Anders Mörtberg.

≃-elim₁ :
   { p} {A B : Type } 
  Univalence  
  (P : {A : Type }  A  B  Type p) 
  P (Eq.id {A = B}) 
  (A≃B : A  B)  P A≃B
≃-elim₁ univ P p A≃B =
  subst
     (_ , A≃B)  P A≃B)
    (mono₁ 0 (singleton-with-≃-contractible univ) _ _)
    p

≃-elim₁-id :
   { p} {B : Type }
  (univ : Univalence )
  (P : {A : Type }  A  B  Type p)
  (p : P (Eq.id {A = B})) 
  ≃-elim₁ univ P p Eq.id  p
≃-elim₁-id univ P p =
  subst
     (_ , A≃B)  P A≃B)
    (mono₁ 0 (singleton-with-≃-contractible univ) _ _)
    p                                                   ≡⟨ cong  eq  subst  (_ , A≃B)  P A≃B) eq _) $
                                                           mono₁ 1 (mono₁ 0 (singleton-with-≃-contractible univ)) _ _ 

  subst  (_ , A≃B)  P A≃B) (refl _) p                ≡⟨ subst-refl _ _ ⟩∎

  p                                                     

≃-elim¹ :
   { p} {A B : Type } 
  Univalence  
  (P : {B : Type }  A  B  Type p) 
  P (Eq.id {A = A}) 
  (A≃B : A  B)  P A≃B
≃-elim¹ univ P p A≃B =
  subst
     (_ , A≃B)  P A≃B)
    (mono₁ 0 (other-singleton-with-≃-contractible univ) _ _)
    p

≃-elim¹-id :
   { p} {A : Type }
  (univ : Univalence )
  (P : {B : Type }  A  B  Type p)
  (p : P (Eq.id {A = A})) 
  ≃-elim¹ univ P p Eq.id  p
≃-elim¹-id univ P p =
  subst
     (_ , A≃B)  P A≃B)
    (mono₁ 0 (other-singleton-with-≃-contractible univ) _ _)
    p                                                         ≡⟨ cong  eq  subst  (_ , A≃B)  P A≃B) eq _) $
                                                                 mono₁ 1 (mono₁ 0 (other-singleton-with-≃-contractible univ)) _ _ 

  subst  (_ , A≃B)  P A≃B) (refl _) p                      ≡⟨ subst-refl _ _ ⟩∎

  p