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

{-# OPTIONS --without-K #-}

-- 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
  hiding (id; inverse) renaming (_∘_ to _⊚_)
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 hiding (id; _∘_; inverse)
import Nat eq as Nat
open import Prelude hiding (swap)
open import Surjection eq hiding (id; _∘_; ∃-cong)

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

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

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

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

Univalence′ :  {}  Set   Set   Set (lsuc )
Univalence′ A B = Is-equivalence (≡⇒≃ {A = A} {B = B})

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

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

≡≃≃ :  {} {A B : Set }  Univalence′ A B  (A  B)  (A  B)
≡≃≃ univ =  ≡⇒≃ , univ 

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

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

-- Some abbreviations.

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

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

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

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

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

Propositional-extensionality : ( : Level)  Set (lsuc )
Propositional-extensionality  =
  {A B : Set }  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 : Set } 
   Is-proposition A  Is-proposition B  Univalence′ A B)

Propositional-extensionality-is-univalence-for-propositions {} ext =
  _↔_.to (⇔↔≃ ext
              ([inhabited⇒+]⇒+ 0 λ prop-ext 
               implicit-Π-closure ext 1 λ _ 
               implicit-Π-closure ext 1 λ _ 
               Π-closure (lower-extensionality _ lzero ext) 1 λ A-prop 
               Π-closure (lower-extensionality _ lzero ext) 1 λ B-prop 
               Π-closure (lower-extensionality _ lzero ext) 1 λ _ 
               ≡-closure (prop-ext {_}) A-prop B-prop)
              (implicit-Π-closure ext 1 λ _ 
               implicit-Π-closure ext 1 λ _ 
               Π-closure (lower-extensionality _ lzero ext) 1 λ _ 
               Π-closure (lower-extensionality _ lzero ext) 1 λ _ 
               Eq.propositional ext _))
    (record
       { to   = λ prop-ext A-prop B-prop A≃B 
                  ( prop-ext A-prop B-prop (_≃_.logical-equivalence A≃B)
                  , _⇔_.to propositional⇔irrelevant
                      (Eq.left-closure (lower-extensionality _ _ ext)
                                       0 A-prop)
                      _ _
                  ) , λ _  Σ-≡,≡→≡
                        (_⇔_.to propositional⇔irrelevant
                           (≡-closure prop-ext A-prop B-prop)
                           _ _)
                        (_⇔_.to propositional⇔irrelevant
                           (mono₁ 1 (Eq.left-closure
                                       (lower-extensionality _ _ ext)
                                       0 A-prop)
                                  _ _)
                           _ _)
       ; from = λ univ {A B} A-prop B-prop 
                  A  B  ↔⟨ ⇔↔≃ (lower-extensionality _ _ ext) A-prop B-prop 
                  A  B  ↔⟨ inverse  _ , univ A-prop B-prop  ⟩□
                  A  B  
       })
  where
  ⇔≃≡ :
    Propositional-extensionality  
    {A B : Set } 
    Is-proposition A  Is-proposition B 
    (A  B)  (A  B)
  ⇔≃≡ prop-ext {A} {B} A-prop B-prop =
    A  B                        ↝⟨ proj₂ (propositional-identity≃≡
                                              (A B : Proposition )  proj₁ A  proj₁ B)
                                              { (A , A-prop) (B , B-prop) 
                                                  ⇔-closure (lower-extensionality _ _ ext)
                                                            1 A-prop B-prop })
                                              _  F.id)
                                              { (A , A-prop) (B , B-prop) A⇔B 
                                                  Σ-≡,≡→≡ (prop-ext A-prop B-prop A⇔B)
                                                          (_⇔_.to propositional⇔irrelevant
                                                             (H-level-propositional
                                                                (lower-extensionality _ _ ext) 1)
                                                             _ _) }))
                                          ext 
    (A , A-prop)  (B , B-prop)  ↔⟨ inverse $ ignore-propositional-component
                                                (H-level-propositional
                                                   (lower-extensionality _ _ ext) 1) ⟩□
    A  B                        

  ≡-closure :
    Propositional-extensionality  
    {A B : Set } 
    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 (lower-extensionality _ _ ext) 1 A-prop B-prop)

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

abstract

  -- "Evaluation rule" for ≡⇒≃.

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

  -- "Evaluation rule" for ≡⇒→.

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

  -- "Evaluation rule" for ≡⇒←.

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

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

  ≃⇒≡-id :  {a} {A : Set 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 : Set } {eq : A  B}
            (univ : Univalence′ A B) 
            to-implication (≡⇒↝ k (≃⇒≡ univ eq))  _≃_.to eq
  ≡⇒→-≃⇒≡ k {eq = 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                             

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

-- The univalence axiom implies that Set 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)

  abstract

    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 Set is not a set.

    ¬-Set-set : ¬ Is-set Set
    ¬-Set-set =
      Is-set Set                         ↝⟨ _⇔_.to set⇔UIP 
      Uniqueness-of-identity-proofs Set  ↝⟨  uip  uip _ _) 
      swap-as-an-equality  refl Bool    ↝⟨ swap≢refl ⟩□
                                        

abstract

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

  ¬-Set-set-↑ :  {} 
                Univalence′ (  Bool) (  Bool) 
                ¬ Is-set (Set )
  ¬-Set-set-↑ {} univ =
    Is-set (Set )                           ↝⟨ _⇔_.to set⇔UIP 
    Uniqueness-of-identity-proofs (Set )    ↝⟨  uip  uip _ _) 
    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

abstract

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

  equality-can-have-infinitely-many-inhabitants :
    Univalence′   
     λ (A : Set)   λ (B : Set) 
     λ (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 : Set} (f : A    ) 
      Injective f  Injective (cast  f)
    cast-preserves-injections f inj {x = x} {y = 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 = ↔⇒≃ 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

abstract

  -- The transport theorem.

  transport-theorem :
     {p₁ p₂} (P : Set p₁  Set 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)

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

  resp-is-equivalence :
     {p₁ p₂} (P : Set p₁  Set 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)
      (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 : Set } {C : Set c} 
    Univalence′ B A  (A≃B : A  B) 
    Is-equivalence  (g : B  C)  g  _≃_.to A≃B)
  precomposition-is-equivalence {} {c} {C = C} univ A≃B =
    resp-is-equivalence P resp refl univ (Eq.inverse A≃B)
    where
    P : Set   Set (  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 : Set } {C : Set 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.

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

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

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

abstract

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

  extensionality :
     {a b} {A : Set a} {B : Set b} 
    Univalence′ (B ²/≡) B 
    {f g : A  B}  (∀ x  f x  g x)  f  g
  extensionality {A = 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₁  proj₂

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

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

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

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

  Π-closure-contractible :
     {b}  Univalence′ (Set b ²/≡) (Set b) 
     {a} {A : Set a} {B : A  Set b} 
    (∀ x  Univalence′ ( b ) (B x)) 
    (∀ x  Contractible (B x))  Contractible ((x : A)  B x)
  Π-closure-contractible {b} univ₁ {A = 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)) $ ↔⇒≃ $
        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′ (Set b ²/≡) (Set b) 
     {a} {A : Set a} 
    (∀ {B : A  Set b} x  Univalence′ ( b ) (B x)) 
    {B : A  Set b}  Extensionality′ A B
  dependent-extensionality univ₁ univ₂ =
    _⇔_.to Π-closure-contractible⇔extensionality
      (Π-closure-contractible 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}  Set a  Set (lsuc (a  ))
Pow  {a} A = A  Set (a  )

-- Fam.

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

-- Pow and Fam are pointwise logically equivalent.

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

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

abstract

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

  Univalence′-propositional :
     {}  Extensionality (lsuc ) (lsuc ) 
    {A B : Set }  Is-proposition (Univalence′ A B)
  Univalence′-propositional ext =
    Eq.propositional ext ≡⇒≃

  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 : Set } (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 : Set } (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 : Set } (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 : Set } (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 : Set a}
    (P : A  Set p) (R : A  A  Set 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 : Set a}
    (P : A  Set p) (R : A  A  Set 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 : Set p₁  Set 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 : Set a}
    (P : A  Set p) (R : A  A  Set 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)
      (subst-is-equivalence P (_↠_.from ≡↠R r))

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

  ≃⇒≡-→-cong :
     {} {A₁ A₂ B₁ B₂ : Set }
    (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₂ = A₂} {B₁} ext univ A₁≃A₂ B₁≃B₂ =
    ≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂)                        ≡⟨ cong (≃⇒≡ univ) (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₂)                  ≡⟨ 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₂))) (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)) (ext $ subst-in-terms-of-≡⇒↝ equivalence _  B  A₂  B))
                                                                                      (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 : Set } {A≃B : A  B} 
    Extensionality p p 
    (univ₁ : Univalence )
    (univ₂ : Univalence p)
    (P : Set   Set 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 = 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₂) $ lift-equality ext lemma ⟩∎
    ≃⇒≡ univ₂ (P-cong A≃B)                    
    where
    lemma : ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B))  _≃_.to (P-cong A≃B)
    lemma = 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 : Set p₁  Set 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 : Set p₁  Set 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₁ : Set ℓ₁} {A₂ : Set ℓ₂} {B₁ : Set ℓ₁} {B₂ : Set ℓ₂} 
  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₂ = ↔⇒≃ (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₁  )

  abstract

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

      _≃_.to (≃-≡ (≡≃≃ univ₂)) (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)
                                                                               (ext₂ $ _≃_.right-inverse-of B₁≃B₂)
                                                                               (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 (≃-≡ (≡≃≃ univ₁)) (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)
                                                                               (ext₁ $ _≃_.left-inverse-of B₁≃B₂)
                                                                               (ext₁ $ _≃_.left-inverse-of A₁≃A₂) ⟩∎
        ≡⇒→ A₁≡B₁                                                     ))

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

singleton-with-≃-↔-⊤ :
   {a b} {B : Set b} 
  Extensionality (a  b) (a  b) 
  Univalence (a  b) 
  ( λ (A : Set (a  b))  A  B)  
singleton-with-≃-↔-⊤ {a} {B = 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 : Set a} 
  Extensionality (a  b) (a  b) 
  Univalence (a  b) 
  ( λ (B : Set (a  b))  A  B)  
other-singleton-with-≃-↔-⊤ {b = b} {A} ext univ =
  ( λ B  A  B)  ↝⟨ (∃-cong λ _  inverse-isomorphism ext) 
  ( λ B  B  A)  ↝⟨ singleton-with-≃-↔-⊤ {a = b} ext univ ⟩□
                  

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

∃Contractible↔⊤ :
   {a} 
  Extensionality a a 
  Univalence a 
  ( λ (A : Set 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₂ : Set 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₁} {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₂ : Set 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₁} {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₂ : Set 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₁} {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 : Set 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 : Set a)  Is-proposition A)
Is-set-∃-Is-proposition {a} ext prop-ext (A₁ , A₁-prop) (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 ⟩□
  Is-proposition ((A₁ , A₁-prop)  (A₂ , A₂-prop))  
  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 : Set a)  H-level n A)
¬-∃-H-level-H-level =
  1 ,
  ( Is-proposition ( λ A  Is-proposition A)               ↝⟨ _⇔_.to propositional⇔irrelevant 
    ((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 : Set 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 : Set₁)   λ (f : (x : A)  x  x)  f  refl
∃≢refl ext univ =
    ( λ (A : Set)  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 : Set) (p : A  A) 
        λ (q : A  A)  subst  A  A  A) q p  p)  ↝⟨ (∀-cong ext λ _  ∀-cong ext λ _ 
                                                             ∃-cong λ _  ≡⇒↝ _ [subst≡]≡[trans≡trans]) ⟩□
    ((A : Set) (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 : Set₁)  ¬ 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)    ↝⟨ _⇔_.to propositional⇔irrelevant 
   Proof-irrelevant (∀ x  x  x)  ↝⟨  irr  irr _ _) 
   f  refl                        ↝⟨ f≢refl ⟩□
                                  )

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

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

  H-level 3 Set₁                        ↝⟨  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 $ ≃-≡ $ ↔⇒≃ ≃-as-Σ) 1 
  Is-proposition ((id , _)  (id , _))  ↝⟨ H-level.respects-surjection
                                             (_↔_.surjection $ inverse $ ignore-propositional-component (Eq.propositional ext id)) 1 
  Is-proposition (id  id)              ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ 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 : Set } 
      Univalence′ A B 
      Is-proposition A  Is-proposition B 
      (A  B)  (A  B)
≡↠⇔ {A = A} {B} univ A-prop B-prop =
  A  B  ↔⟨ ≡≃≃ univ 
  A  B  ↝⟨ ≃↠⇔ A-prop B-prop ⟩□
  A  B  

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

⇔↔≡ :  {} {A B : Set } 
      Extensionality   
      Univalence′ A B 
      Is-proposition A  Is-proposition B 
      (A  B)  (A  B)
⇔↔≡ {A = A} {B} ext univ A-prop B-prop =
  A  B  ↝⟨ ⇔↔≃ 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 = 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)