###############################
        # Universe n is not an n-Type #
        ###############################

       Nicolai Kraus    Christian Sattler

                  April 20, 2013

  In basic MLTT with a sequence of univalent universes, 
  the first universe is not a set (i.e. not a 0-type). 
  This is one of the most basic consequences of univalence, 
  but already the next step is surprisingly difficult. 
  We give a proof for the general case and show that
  Universe n is not an n-type. At the same time, we 
  solve one of the question on the list of open problems
  of the Univalent Foundations program in Princeton 12/13,
  namely, the construction of an (n+1)-Type that is not
  an n-Type.
  This Agda file contains the formalization of a proof 
  that we have presented in April 2013 at the IAS in 
  Princeton.


This file requires (at least) Agda 2.3.2 to be loaded. We use 
parts of (an older version of) the HoTT Agda library, see
https://github.com/HoTT/HoTT-Agda. These parts are the module
'Base', imported below, and everything it imports itself.

\begin{code}
{-# OPTIONS --without-K #-}

open import Base

module Hierarchy where

\end{code}

Warm-up: We use the standard proof to show that the first universe
is not an h-set.

\begin{code}

-- negation on bool
negation :  {i}  bool {i}  bool {i}
negation true = false
negation false = true

-- negation is an equivalence
negation-equiv :  {i}  bool {i}  bool {i}
negation-equiv = let
                   self-inverse :  {i}  (b : bool {i})  negation (negation b)  b
                   self-inverse = λ { true  refl ; false  refl}
                 in 
                   negation , iso-is-eq negation negation self-inverse self-inverse

-- this equivalence is not the same as the identity
id≢negation-equiv :  {i}  id-equiv (bool {i = i})  negation-equiv {i = i}
id≢negation-equiv id≡¬ = 
  let
    true≡false : true  false
    true≡false = ap  (e : bool  bool)  π₁ e true) id≡¬
  in
    bool-true≢false true≡false 
    
-- and finally, U₀ is not a set
U₀-not-a-set : ¬ (is-set Set)
U₀-not-a-set = λ U₀-is-set  
  let
    bool≃bool           = (_≃_ {i = zero} (bool {i = zero}) (bool {i = zero}))
    bool≡bool          = bool {i = zero }  bool
    bool≡bool-is-prop  : is-prop bool≡bool
    bool≡bool-is-prop  = U₀-is-set bool bool
    bool≃bool-is-prop   : is-prop bool≃bool
    bool≃bool-is-prop   = equiv-types-truncated (S ⟨-2⟩) path-to-eq-equiv bool≡bool-is-prop
  in
    id≢negation-equiv (π₁ (bool≃bool-is-prop (id-equiv {i = zero} bool) negation-equiv))

\end{code}

We now proceed with the development of the machinery that is 
needed for the generalization of the above statement. Our first 
goal is to show that, for any type X, the types
                 reflⁿ⁺¹X ≡ reflⁿ⁺¹X 
and
            ∀ x → reflⁿx ≡ reflⁿx
are equivalent.

\begin{code}
-- We relate (paths between paths) with (paths between equivalences) .
paths≃eqs :  {i} {X : Set i} 
   (refl {a = X}  refl {a = X}) 
      
     (id-equiv X  id-equiv X)
paths≃eqs {i} {X} = equiv-ap {i = suc i} {A = X  X} {B = X  X} (path-to-eq-equiv) (refl {a = X}) (refl {a = X})

-- We say that an equivalence is 'stable' if it maps trivial inhabitants to trivial inhabitants. 
paths≃eqs-stable :  {i} {X : Set i}
   paths≃eqs  (refl {a = refl {a = X}})  refl {a = id-equiv X}
paths≃eqs-stable = refl


Σ-lemma-applied :  {i} {X : Set i} 
   (id-equiv X  id-equiv X) 
      
     (Σ (id X  id X) 
         p  
          transport  f  is-equiv f) p (id-is-equiv X)  (id-is-equiv X))) 
Σ-lemma-applied = total-Σ-eq-equiv ⁻¹

Σ-drop-contr :  {i j} {Y : Set i} {P : Y  Set j} 
   ((y : Y)  is-contr (P y))
   (Σ Y λ y  P y)  Y
Σ-drop-contr h = 
  (π₁ , iso-is-eq π₁  y  (y , π₁ (h y)))  y  refl)  yp  total-Σ-eq (refl , !((π₂ (h (π₁ yp))) (π₂ yp)))) ) 

Σ-drop-prop :  {i j} {Y : Set i} {P : Y  Set j} 
   ((y : Y)  is-prop (P y)) 
   (y₁ y₂ : Y)  (p₁ : P y₁)  (p₂ : P y₂) 
   (Σ (y₁  y₂) λ q  transport _ q p₁  p₂) 
      
     (y₁  y₂)
Σ-drop-prop h y₁ y₂ p₁ p₂ = Σ-drop-contr {Y = y₁  y₂}  yy  h y₂ _ _)

Σ-drop-prop-applied :  {i} {X : Set i} 
   (Σ (id X  id X) λ q  transport  f  is-equiv f) q (id-is-equiv X)  (id-is-equiv X)) 
      
     (id X  id X)
Σ-drop-prop-applied {i} {X} = Σ-drop-prop {P = λ f  is-equiv f}  f   is-equiv-is-prop f) (id X) (id X) (id-is-equiv X) (id-is-equiv X)


isotopies≃homotopies :  {i} {X : Set i}  (id-equiv X  id-equiv X)  (id X  id X)
isotopies≃homotopies = equiv-compose Σ-lemma-applied Σ-drop-prop-applied 

total-Σ-eq-stable-2 :  {i j} {A : Set i} {P : A  Set j} {x : Σ A P}
   (total-Σ-eq {xu = x} {yv = x} (refl , refl))  refl
total-Σ-eq-stable-2 = refl

total-Σ-inv-stable-2 :  {i j} {A : Set i} {P : A  Set j} {x : Σ A P}
   (π₁ (π₁ (total-Σ-eq-is-equiv {x = x} {y = x} refl)))  (refl , refl)
total-Σ-inv-stable-2 {i} {j} {A} {P} {x} =
  ! (ap π₁ (π₂ (total-Σ-eq-is-equiv {x = x} {y = x} refl) (( (refl , refl) , total-Σ-eq-stable-2 ))))

isotopies≃homotopies-stable :  {i} {X : Set i}  isotopies≃homotopies  (refl {a = id-equiv X})  (refl {a = id X})
isotopies≃homotopies-stable {i} {X} = ap π₁ total-Σ-inv-stable-2


reflrefl≃idid :  {i} {X : Set i} 
   (refl {a = X}  refl {a = X}) 
      
     (id X  id X)
reflrefl≃idid = equiv-compose paths≃eqs isotopies≃homotopies

reflrefl≃idid-stable :  {i} {X : Set i}
   reflrefl≃idid  (refl {a = refl {a = X}})  refl {a = id X}
reflrefl≃idid-stable = isotopies≃homotopies-stable

idfun :  {i}{X : Set i} 
   (id X  id X) 
      
     ((x : X)  x  x)
idfun {i}{X} = (funext-equiv ) ⁻¹


funext-stable :  {i j} {A : Set i} {P : A  Set j} (f : (a : A)  P a)
   (funext {f = f} {g = f}  a  refl))  refl
funext-stable {i}{j}{A}{P} f  = funext-happly refl 

funext-inv-stable :  {i j} {A : Set i} {P : A  Set j} (f : (a : A)  P a)
   π₁ (π₁ (funext-is-equiv {f = f} {g = f} refl))   x  refl)
funext-inv-stable f = 
  ! ( ap π₁ (π₂ (funext-is-equiv {f = f} {g = f} refl)  ((λ x  refl) , funext-stable f)))

idfun-stable :  {i}{X : Set i}
   idfun  (refl {a = id X})  λ x  refl
idfun-stable = funext-inv-stable _

induction₁ :  {i} {X : Set i} 
   (refl {a = X}  refl {a = X}) 
      
     ((x : X)  x  x)
induction₁ {i}{X} = equiv-compose reflrefl≃idid idfun

induction₁-stable :  {i}{X : Set i}  induction₁  (refl {a = refl {a = X}})   x  refl {a = x})
induction₁-stable {i} {X} = 
  (induction₁  (refl {a = refl {a = X}}))               ≡⟨ refl 
  (idfun  (reflrefl≃idid  (refl {a = refl {a = X}}))) ≡⟨ ap (π₁ idfun) reflrefl≃idid-stable 
  (idfun  (refl {a = id X}))                            ≡⟨ idfun-stable 
   x  refl {a = x})    


refl↦refl :  {i}{X : Set i} {a x : X} 
   (p : x  a) 
   Σ ((x  x)  (a  a)) 
        λ e  (e  (refl {a = x}))  refl
refl↦refl (refl) = id-equiv _ , refl


Ω :  {i}  (Σ (Set i) λ A  A)  (Σ (Set i) λ A  A)
Ω (A , a) = (a  a) , refl 

Ωⁿ :  {i}  (n : )   (Σ (Set i) λ A  A)  (Σ (Set i) λ A  A)
Ωⁿ 0 p = p
Ωⁿ (S n) p = Ω (Ωⁿ n p)


r=r :  {i}  (n : )  {X : Set i}  X  Set i
r=r n {X} x = π₁ (Ωⁿ (S n) (X , x))

r+1 :  {i}  (n : )  {X : Set i}  (x : X)  r=r n x
r+1 n {X} x = refl {a = (π₂ (Ωⁿ n (X , x)))}

-- We prove simultanously by induction on n that there
-- is the equivalence that we want, but also that this
-- equivalence is stable, i.e. it maps trivial 
-- inhabitants to trivial inhabitants.

induction :  {i} {X : Set i}  (n : ) 
  -- reflⁿ⁺¹X ≡ reflⁿ⁺¹X    ≃   ∀ x → reflⁿx ≡ reflⁿx
   Σ
      ((r=r (S n) X)  ((x : X)  (r=r n x)))
      λ e  
        e  (r+1 (S n) X)  λ x  r+1 n x
induction O = induction₁ , induction₁-stable
induction {i} {X} (S n) =
  let
    ind-hyp₁ : (r=r (S n) X)  ((x : X)  (r=r n x))
    ind-hyp₁ = π₁ (induction n)
    ind-hyp₂ : ind-hyp₁  (r+1 (S n) X)  λ x  r+1 n x
    ind-hyp₂ = π₂ (induction {i} {X} n)
    rⁿ⁺²X = r+1 (S n) X
    rⁿ⁺²X≡/≃pre∀x,rⁿ⁺¹x≡/ : (rⁿ⁺²X  rⁿ⁺²X)  ((ind-hyp₁  rⁿ⁺²X)  (ind-hyp₁  rⁿ⁺²X))
    rⁿ⁺²X≡/≃pre∀x,rⁿ⁺¹x≡/ = equiv-ap ind-hyp₁ rⁿ⁺²X rⁿ⁺²X
    refl↦refl-applied = Σ ((rⁿ⁺²X  rⁿ⁺²X)  ((λ (x : X)  r+1 n x)   x  r+1 n x)))
                            λ e  (e  (refl {a = rⁿ⁺²X}))  (refl {a = λ x  r+1 n x})
    refl↦refl-applied = refl↦refl ind-hyp₂
    lemma : (rⁿ⁺²X  rⁿ⁺²X)  ((λ x  r+1 n x)   x  r+1 n x))
    lemma = equiv-compose rⁿ⁺²X≡/≃pre∀x,rⁿ⁺¹x≡/ (π₁ refl↦refl-applied)
    first-goal : (rⁿ⁺²X  rⁿ⁺²X)  ((x : X)  (r+1 n x)  (r+1 n x))
    first-goal = equiv-compose lemma (funext-equiv ⁻¹)
    prepare-second-goal : ((rⁿ⁺²X≡/≃pre∀x,rⁿ⁺¹x≡/)  (refl {a = rⁿ⁺²X}))  refl
    prepare-second-goal = refl
    prepare-second-goal' : (lemma  (refl {a = rⁿ⁺²X}))  refl
    prepare-second-goal' = (ap  (π₁ (π₁ refl↦refl-applied))  prepare-second-goal)   (π₂ refl↦refl-applied) 
    second-goal : first-goal  (refl )  λ x  r+1 (S n) x
    second-goal = (ap (π₁ (funext-equiv ⁻¹)) prepare-second-goal')  funext-inv-stable _
  in
    first-goal , second-goal

\end{code}

This allows us to state our first lemma:
  #############################################
  ## LEMMA 1. The types                      ##
  ##            reflⁿ⁺¹X ≡ reflⁿ⁺¹X          ##
  ## and                                     ##
  ##        ∀ x → reflⁿx ≡ reflⁿx            ##
  ## are equivalent.                         ##
  #############################################

\begin{code}
induction-corollary :  {i} {X : Set i}  (n : )
   (r=r (S n) X) 
      
     ((x : X)  r=r n x)
induction-corollary n = π₁ (induction n)
\end{code}

Our next goal is to show that, if we consider higher loops, the 
"simple" parts of tuples do not play a role. 
More precisely, our goal is:
  If Y is a type, dependent on X, and (Y x) is always an h-set, 
  then:
    reflⁿ⁺¹(x,y) ≡ reflⁿ⁺¹(x,y)   ≃   reflⁿ⁺¹x ≡ reflⁿ⁺¹x


\begin{code}
-- a lemma: transporting paths along paths is just path composition
-- taken from our Hedberg file (and simplified, less general)

transport-paths-along-paths :  {i} {X : Set i} {x y : X} (p : x  x) (q : x  y) 
                               (transport _ q p )  (! q)  p  q
transport-paths-along-paths p refl = ! (refl-right-unit p)

trans-p-p≡p :  {i} {X : Set i} {x : X} (p : x  x)  (transport  x  x  x) p p)  p
trans-p-p≡p p = (transport  x  x  x) p p)  ≡⟨ transport-paths-along-paths p p 
                 (! p)  p  p                   ≡⟨ ! (concat-assoc (! p) p p) 
                 ((! p)  p)  p                 ≡⟨ ap  q  q  p) (opposite-left-inverse p) 
                 p                               


equiv-ap-stable :  {i j} {A : Set i} {B : Set j} (f : A  B) (x : A) 
   (equiv-ap f x x)  refl  refl
equiv-ap-stable {i}{j}{A}{B} f x = refl


kill-set-component :  {i j}(n : )(X : Set i)(Y : X  Set j)(x : X)(y : Y x)
   ((x : X)  is-set (Y x))
   Σ  ((r=r (S n) x)  (r=r (S n) {X = Σ X Y} (x , y))) 
      λ e  e  refl  refl
kill-set-component {i} {j} O X Y x y h-bound = 
  let
    rr≃r₂ : (_≡_ {A = Σ (x  x) λ u  transport  x  Y x) u y  y} 
            (refl , refl) 
            (refl , refl))
            
            (r=r (S O) {X = Σ X Y} (x , y)) 
    rr≃r₂ = equiv-ap total-Σ-eq-equiv (refl , refl) (refl , refl)

    rr1 =   (_≡_ {A = x  x} refl refl)
    rr2 =   (_≡_ {A = Σ (x  x) λ u  transport  x  Y x) u y  y} 
            (refl , refl) 
            (refl , refl))
    rr3 =   Σ (_≡_ {A = (x  x)} refl refl) 
                λ rr  (  transport  (u : x  x)  transport  x  Y x) u y  y  ) rr refl)  refl
    
    rr3≃rr2 : rr3  rr2
    rr3≃rr2 = total-Σ-eq-equiv
    rr3≃rr1 : rr3  rr1
    rr3≃rr1 = Σ-drop-prop 
               {Y = x  x}
               {P = λ u  transport  x  Y x) u y  y}
                (p : x  x)  h-bound x _ _) 
               refl refl refl refl
    rr1≃rr2 : rr1  rr2
    rr1≃rr2 = equiv-compose (rr3≃rr1 ⁻¹) rr3≃rr2
    e       : (r=r (S O) x)  (r=r (S O) {X = Σ X Y} (x , y))
    e       = equiv-compose rr1≃rr2 rr≃r₂ 

    rr1≃rr2-stable : rr1≃rr2  (r+1 (S O) x)  refl
    rr1≃rr2-stable =         
        let
          s₁           = r+1 (S O) x
          simple-im-s₁ : Σ (refl {a = x}  refl {a = x}) 
                           λ p   transport  u  transport Y u y  y) p refl  refl
          simple-im-s₁ = s₁ , (π₁ (h-bound x y y (transport  u  transport Y u y  y) s₁ refl) refl))
          s₂          = π₂ simple-im-s₁
          s₂≡refl    : _≡_ {A = refl {a = y}  refl {a = y}} s₂ refl
          s₂≡refl    = let
                          center    = π₁ (h-bound x y y refl refl)
                          connecter = π₂ (h-bound x y y refl refl)
                        in
                          ! (connecter refl)
          goal        : rr1≃rr2  s₁  refl
          goal        = rr1≃rr2  s₁   ≡⟨ refl 
                        Σ-eq s₁   s₂    ≡⟨ refl 
                        Σ-eq refl s₂   ≡⟨ ap  s  Σ-eq refl s) s₂≡refl 
                        Σ-eq refl refl ≡⟨ refl 
                        refl           
        in 
          goal 

    e-stable       : e  (r+1 (S O) x)  (r+1 (S O) {X = Σ X Y} (x , y)) 
    e-stable       = e  (r+1 (S O) x)                         ≡⟨ refl 
                     ((π₁ rr≃r₂)  (π₁ rr1≃rr2)) (r+1 (S O) x)  ≡⟨ ap (π₁ rr≃r₂) rr1≃rr2-stable 
                     (π₁ rr≃r₂) refl                            ≡⟨ refl 
                     (r+1 (S O) {X = Σ X Y} (x , y))   
  in 
    e , e-stable -- induction base case done
kill-set-component {i} {j} (S n) X Y x y h = 
    let
      step1        : _
      step1        = equiv-ap (π₁ (kill-set-component n X Y x y h)) refl refl
      step1-stable : (step1  refl)  refl
      step1-stable = refl -- trivial, can ignore later
      step2        : (_  _)  (refl  refl)
      step2        = π₁ (refl↦refl {a = refl}
                            {x = π₁ (π₁ (kill-set-component n X Y x y h)) refl} 
                            (π₂ (kill-set-component n X Y x y h)))
      step2-stable : (step2  refl)  refl
      step2-stable = π₂ (refl↦refl {a = refl}
                            {x = π₁ (π₁ (kill-set-component n X Y x y h)) refl} 
                            (π₂ (kill-set-component n X Y x y h)))
    in
      equiv-compose step1 step2
      ,
      step2-stable
\end{code}

As a corollary, we get:

  #############################################
  ## LEMMA 2. If (Y x) is always an h-set,   ##
  ## then the types                          ##
  ##       reflⁿ⁺¹(x,y) ≡ reflⁿ⁺¹(x,y)       ##
  ## and                                     ##
  ##       reflⁿ⁺¹x ≡ reflⁿ⁺¹x               ##
  ## are equivalent.                         ##
  #############################################

\begin{code}
kill-set-component-corollary :  {i j}(n : )(X : Set i)(Y : X  Set j)(x : X)(y : Y x)
   ((x : X)  is-set (Y x))
   ((r=r (S n) x)  (r=r (S n) {X = Σ X Y} (x , y))) 
kill-set-component-corollary n X Y x y h = π₁ (kill-set-component n X Y x y h)
\end{code}

Now that we know that a potentially disturbing component of a
pair can be ignored under some condition, we want to show how
that this condition can be achieved in a case that is important
for us.

\begin{code}

-- a simple lemma that corresponds to "1+n = n+1"
in=out :  {i}  (n : )  (p : Σ (Set i) λ A  A) 
   Ω (Ωⁿ n p)  (Ωⁿ n (Ω p))
in=out O p = refl 
in=out (S n) p = ap Ω (in=out n p)


lemma :  {i} {X : Set i} (x : X) (n : ) 
    π₁ (Ωⁿ (S n) (Ω (X , x)))      
       -- same as (π₂ (Ωⁿ n ((x ≡ x) , refl)) ≡ π₂ (Ωⁿ n ((x ≡ x) , refl))) 
     
      π₁ (Ω (Ωⁿ (S n) (X , x)))
      -- same es π₁ (Ω (_ , refl {a = π₂ (Ωⁿ n (X , x))})) 
      -- same as (refl {a = π₂ (Ωⁿ n (X , x))} ≡ refl {a = π₂ (Ωⁿ n (X , x))})
lemma {i} {X} x n = ap π₁ (! (in=out (S n) (X , x)))

-- we prove a stronger statement that needed, as the induction
-- would not go through otherwise.
bound-reduce :  {i}  (n : ) 
   (X : Set i) 
   (is-truncated  S n  X )  
   (x : X)  is-set (r=r n x)
bound-reduce O X h x = h x x
bound-reduce {i} (S n) X h x = 
  let
    have-type = _
    goal-type = refl {a = _}  refl
    have-type≡goal-type : have-type  goal-type
    have-type≡goal-type = lemma x n
    property :  {j}  (T : Set j)  Set j
    property T = (p q : T)  (is-prop (p  q))
    have : property have-type
    have = bound-reduce n (x  x) (h x x) refl
    goal : property goal-type
    goal = transport  T  property T) have-type≡goal-type have
  in
    goal
\end{code}

  #############################################
  ## LEMMA 3. If X is an n-Type,             ##
  ## then (reflⁿX ≡ reflⁿX) is an h-set.     ##
  #############################################

\begin{code}

bound-reduce-cor :  {i}  (n : ) 
   (X : Set i) 
   (is-truncated  n  X )  
   is-set (r=r n X)
bound-reduce-cor O X h = 
  let
    X≃X-is-set : is-set (X  X)
    X≃X-is-set = ≃-is-set h h
    X≡X-is-set : is-set (X  X)
    X≡X-is-set = equiv-types-truncated  O  eq-to-path-equiv X≃X-is-set
  in
    X≡X-is-set
bound-reduce-cor (S n) X h = 
  let
    ∀xrrnx : (x : X)  is-set (r=r n x)
    ∀xrrnx = bound-reduce n X h
    rrn∀x : is-set ((x : X)  r=r n x)
    rrn∀x = Π-is-truncated  O  ∀xrrnx
    rrnX  : is-set (r=r (S n) X)
    rrnX  = equiv-types-truncated  O  (  (induction-corollary n) ⁻¹  ) rrn∀x
  in
    rrnX 
\end{code}

We now define the type A(n), which has several nice properties:
  ∘ It is an n+1 - Type.
  ∘ It is not an n - Type.
  ∘ It lives in Universe n+1.

\begin{code}
ℕ→Level :   Level
ℕ→Level O = zero
ℕ→Level (S n) = suc (ℕ→Level n)


A : (n : )  Set (suc (ℕ→Level n))
A n = Σ (Set (ℕ→Level n)) 
       λ X  (is-truncated  n  X) × (r=r n X)

e1 : (n : )  (r=r (S n) (A n))  ((a : A n)  (r=r n a))
e1 n = induction-corollary n

Π-≃ : ∀{i j₁ j₂}(X : Set i)(Y : X  Set j₁)(Z : X  Set j₂) 
   ((x : X)  (Y x)  (Z x))
   ((x : X)  (Y x))  ((x : X)  (Z x))
Π-≃ {i}{j₁}{j₂} X Y Z h =
  let
    f : ((x : X)  (Y x))  ((x : X)  (Z x)) 
    f = λ k x  (h x)  (k x)
    g : ((x : X)  (Z x))  ((x : X)  (Y x)) 
    g = λ m x  (h x) ⁻¹  (m x)
  in  
    f , iso-is-eq f g  m  funext  x  inverse-right-inverse (h x) (m x)))  k  funext  x  inverse-left-inverse (h x) (k x)))

trunc→trunc×rr-is-set :  {i} (n : )  (X : Set i)  (is-truncated  n  X)  is-set ((is-truncated  n  X) × (r=r n X))
trunc→trunc×rr-is-set n X h = ×-is-truncated  O  (prop-is-set (is-truncated-is-prop  n )) (bound-reduce-cor n X h)

-- other levels allow same proof
inh→set→set :  {i} (X : Set i)  (X  is-set X)  (is-set X)
inh→set→set X h = λ x  (h x) x

trunc×r=r-is-set :  {i} (n : )  (X : Set i)  is-set ((is-truncated  n  X) × (r=r n X))
trunc×r=r-is-set n X = inh→set→set _  x  trunc→trunc×rr-is-set n X (π₁ x))

e2 : (n : )  (((a : A (S n))  (r=r (S n) (π₁ a)))  ((a : A (S n))  (r=r (S n) a))) 
e2 n = Π-≃ (A (S n))  a  r=r (S n) (π₁ a))  a  r=r (S n) a) 
            a  kill-set-component-corollary n _  X  (is-truncated  S n  X) × (r=r (S n) X)) _ _  X  trunc×r=r-is-set (S n) _))

e : (n : )  (r=r (S (S n)) (A (S n)))  ((a : A (S n))  (r=r (S n) (π₁ a)))
e n = equiv-compose (e1 (S n)) ((e2 n) ⁻¹)

An≃Ty≤×rr : (n : )  (A n)  Σ (Type≤  n  (ℕ→Level n)) λ Xh  (r=r n (π₁ Xh))
An≃Ty≤×rr n = 
  let
    f : A n  Σ (Type≤  n  (ℕ→Level n)) λ Xh  (r=r n (π₁ Xh))
    f = λ {(X , br)  (X , π₁ br) , π₂ br}
    g : (Σ (Type≤  n  (ℕ→Level n)) λ Xh  (r=r n (π₁ Xh)))  A n
    g = λ {(Xb , r)  π₁ Xb , (π₂ Xb , r)}
    h :  exp  f(g exp)  exp
    h = λ exp  refl
    h' :  a  g(f a)  a
    h' = λ exp  refl
  in
    f , iso-is-eq f g h h'
\end{code}

For the case of A₀, we need a different equivalence. 
Of course, A₀ allows us to prove that the second universe is not
a groupoid (not a 1-Type). This proof can be done without all the
lemmas above, but at least Lemma 1 makes the proof easier.

\begin{code}
-- A type that is  equivalent to A O. This should not be necessary,
-- but is makes things easier.
A₀' : Set (suc zero)
A₀' = Σ Set λ X  ((X  X) × is-set X)

transport-× :  {i j k}(X : Set i)(Y : X  Set j)(Z : X  Set k)
   {x₁ x₂ : X}  (p : x₁  x₂)
   (y : Y x₁)  (z : Z x₁)
   (transport  x  (Y x) × (Z x)) p (y , z))
     
     (transport  x  Y x) p y) , (transport  x  Z x) p z)
transport-× X Y Z refl y z = refl 

A₀'-triv : (a : A₀')  a  a
A₀'-triv = λ a  refl

A₀'-nontriv : (a : A₀')  a  a
A₀'-nontriv (X , (p , b)) = 
  Σ-eq p (
    let
      -- this is actually not the correct type - there is some trivial transport missing
      -- trans-p-b≡b : transport (λ X → is-set X) p b ≡ b
      trans-p-b≡b = π₁ (is-set-is-prop _ b)
      trans-p-p=p : transport  X  X  X) p p  p
      trans-p-p=p = trans-p-p≡p p
      
      goal : (transport  X  (X  X) × (is-set X)) p (p , b))  (p , b)
      goal = transport  X  (X  X) × (is-set X)) p (p , b)                  ≡⟨ transport-× Set  X  X  X)  X  is-set X) p _ _ 
              (transport  X  X  X) p p) , (transport  X  is-set X) p b) ≡⟨ Σ-eq trans-p-p=p trans-p-b≡b 
              p                              ,  b                                  
    in
      goal
    )


triv-on-bool = ap π₁ (A₀'-triv (bool , (eq-to-path negation-equiv , bool-is-set)))


nontriv-on-bool = ap π₁ (A₀'-nontriv (bool , (eq-to-path negation-equiv , bool-is-set)))

apπ₁-Σeq-lemma :  {i j}{X : Set i}{Y : X  Set j}
   {x₁ x₂ : X}{y₁ : Y x₁}{y₂ : Y x₂}
   (p : x₁  x₂)
   (q : transport  x  Y x) p y₁  y₂)
   ap π₁ (Σ-eq {A = X}{P = Y} p q)  p
apπ₁-Σeq-lemma refl refl = refl

eval-triv-on-bool : triv-on-bool  eq-to-path (id-equiv bool)
eval-triv-on-bool = 
  let
    path-goal : path-to-eq triv-on-bool  path-to-eq (eq-to-path (id-equiv bool))
    path-goal = path-to-eq triv-on-bool ≡⟨ refl 
                path-to-eq refl         ≡⟨ refl 
                id-equiv bool           ≡⟨ ! (eq-to-path-right-inverse _) 
                path-to-eq (eq-to-path (id-equiv bool)) 
    goal      : triv-on-bool  eq-to-path (id-equiv bool)
    goal      = triv-on-bool                                         ≡⟨ ! (path-to-eq-right-inverse _) 
                eq-to-path (path-to-eq (triv-on-bool))               ≡⟨ ap eq-to-path path-goal 
                eq-to-path (path-to-eq (eq-to-path (id-equiv bool))) ≡⟨ path-to-eq-right-inverse _ 
                eq-to-path (id-equiv bool)                                    
  in
    goal

eval-nontriv-on-bool : nontriv-on-bool  eq-to-path (negation-equiv)
eval-nontriv-on-bool = 
    nontriv-on-bool                                                           ≡⟨ refl 
    ap π₁ (A₀'-nontriv (bool , (eq-to-path negation-equiv , bool-is-set)))    ≡⟨ refl 
    ap π₁ (Σ-eq (eq-to-path negation-equiv) _)                                ≡⟨ apπ₁-Σeq-lemma _ _ 
    eq-to-path (negation-equiv)                                                                

triv-nontriv-different-on-bool : triv-on-bool  nontriv-on-bool 
triv-nontriv-different-on-bool triv-on-bool≡nontriv-on-bool = 
  let
    path-id≡path-¬ : eq-to-path (id-equiv bool)  eq-to-path (negation-equiv)
    path-id≡path-¬ = eq-to-path (id-equiv bool) ≡⟨ ! eval-triv-on-bool 
                      triv-on-bool               ≡⟨ triv-on-bool≡nontriv-on-bool 
                      nontriv-on-bool            ≡⟨ eval-nontriv-on-bool 
                      eq-to-path (negation-equiv) 
    id≡¬           : id-equiv (bool {i = zero})  negation-equiv
    id≡¬           = id-equiv bool                            ≡⟨ ! (eq-to-path-right-inverse _) 
                      path-to-eq (eq-to-path (id-equiv bool))  ≡⟨ ap path-to-eq path-id≡path-¬ 
                      path-to-eq (eq-to-path (negation-equiv)) ≡⟨ eq-to-path-right-inverse _ 
                      negation-equiv                           
  in
    id≢negation-equiv id≡¬ 



triv≢nontriv' : A₀'-triv  A₀'-nontriv
triv≢nontriv' triv≡nontriv =                 
                 let
                   use-bool₁ = happly triv≡nontriv (bool , (eq-to-path negation-equiv , bool-is-set))
                   use-bool₂ = ap (ap π₁) use-bool₁
                 in
                   triv-nontriv-different-on-bool use-bool₂ 

\end{code}

Note. The first attempt to prove that the trivial and the nontrivial
auto-equivalence on A₀ are different resulted in the following gap,
which requires us to show that some closed term of type Bool is equal
to false.

Goal: false ≡
      π₁
      (path-to-eq
       (ap π₁
        (ap2 _,_
         (π₁
          (π₁
           (univalence bool bool
            (negation ,
             (λ y →
                (negation y , (λ {true → refl; false → refl}) y) ,
                .Equivalences._._.path negation negation
                (λ {true → refl; false → refl})
                (π₁
                 (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                  (λ {true → refl; false → refl})))
                (π₂
                 (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                  (λ {true → refl; false → refl})))
                y)))))
         (transport-× Set (λ X → X ≡ X)
          (λ A₁ →
             (x y : A₁) (x₁ y₁ : x ≡ y) →
             Σ (x₁ ≡ y₁) (λ x₂ → (y₂ : x₁ ≡ y₁) → y₂ ≡ x₂))
          (π₁
           (π₁
            (univalence bool bool
             (negation ,
              (λ y →
                 (negation y , (λ {true → refl; false → refl}) y) ,
                 .Equivalences._._.path negation negation
                 (λ {true → refl; false → refl})
                 (π₁
                  (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                   (λ {true → refl; false → refl})))
                 (π₂
                  (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                   (λ {true → refl; false → refl})))
                 y)))))
          (π₁
           (π₁
            (univalence bool bool
             (negation ,
              (λ y →
                 (negation y , (λ {true → refl; false → refl}) y) ,
                 .Equivalences._._.path negation negation
                 (λ {true → refl; false → refl})
                 (π₁
                  (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                   (λ {true → refl; false → refl})))
                 (π₂
                  (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                   (λ {true → refl; false → refl})))
                 y)))))
          bool-is-set

          ap2 _,_
          (transport-paths-along-paths
           (π₁
            (π₁
             (univalence bool bool
              (negation ,
               (λ y →
                  (negation y , (λ {true → refl; false → refl}) y) ,
                  .Equivalences._._.path negation negation
                  (λ {true → refl; false → refl})
                  (π₁
                   (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                    (λ {true → refl; false → refl})))
                  (π₂
                   (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                    (λ {true → refl; false → refl})))
                  y)))))
           (π₁
            (π₁
             (univalence bool bool
              (negation ,
               (λ y →
                  (negation y , (λ {true → refl; false → refl}) y) ,
                  .Equivalences._._.path negation negation
                  (λ {true → refl; false → refl})
                  (π₁
                   (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                    (λ {true → refl; false → refl})))
                  (π₂
                   (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                    (λ {true → refl; false → refl})))
                  y)))))

           !
           (concat-assoc
            (!
             (π₁
              (π₁
               (univalence bool bool
                (negation ,
                 (λ y →
                    (negation y , (λ {true → refl; false → refl}) y) ,
                    .Equivalences._._.path negation negation
                    (λ {true → refl; false → refl})
                    (π₁
                     (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                      (λ {true → refl; false → refl})))
                    (π₂
                     (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                      (λ {true → refl; false → refl})))
                    y))))))
            (π₁
             (π₁
              (univalence bool bool
               (negation ,
                (λ y →
                   (negation y , (λ {true → refl; false → refl}) y) ,
                   .Equivalences._._.path negation negation
                   (λ {true → refl; false → refl})
                   (π₁
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   (π₂
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   y)))))
            (π₁
             (π₁
              (univalence bool bool
               (negation ,
                (λ y →
                   (negation y , (λ {true → refl; false → refl}) y) ,
                   .Equivalences._._.path negation negation
                   (λ {true → refl; false → refl})
                   (π₁
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   (π₂
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   y))))))

           ap
           (λ q →
              q ∘
              π₁
              (π₁
               (univalence bool bool
                (negation ,
                 (λ y →
                    (negation y , (λ {true → refl; false → refl}) y) ,
                    .Equivalences._._.path negation negation
                    (λ {true → refl; false → refl})
                    (π₁
                     (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                      (λ {true → refl; false → refl})))
                    (π₂
                     (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                      (λ {true → refl; false → refl})))
                    y)))))
           (opposite-left-inverse
            (π₁
             (π₁
              (univalence bool bool
               (negation ,
                (λ y →
                   (negation y , (λ {true → refl; false → refl}) y) ,
                   .Equivalences._._.path negation negation
                   (λ {true → refl; false → refl})
                   (π₁
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   (π₂
                    (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                     (λ {true → refl; false → refl})))
                   y))))))
           ∘ refl)
          (π₁
           (is-set-is-prop
            (transport
             (λ _ →
                (x y : bool) (x₁ y₁ : x ≡ y) →
                Σ (x₁ ≡ y₁) (λ x₂ → (y₂ : x₁ ≡ y₁) → y₂ ≡ x₂))
             (transport-paths-along-paths
              (π₁
               (π₁
                (univalence bool bool
                 (negation ,
                  (λ y →
                     (negation y , (λ {true → refl; false → refl}) y) ,
                     .Equivalences._._.path negation negation
                     (λ {true → refl; false → refl})
                     (π₁
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     (π₂
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     y)))))
              (π₁
               (π₁
                (univalence bool bool
                 (negation ,
                  (λ y →
                     (negation y , (λ {true → refl; false → refl}) y) ,
                     .Equivalences._._.path negation negation
                     (λ {true → refl; false → refl})
                     (π₁
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     (π₂
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     y)))))

              !
              (concat-assoc
               (!
                (π₁
                 (π₁
                  (univalence bool bool
                   (negation ,
                    (λ y →
                       (negation y , (λ {true → refl; false → refl}) y) ,
                       .Equivalences._._.path negation negation
                       (λ {true → refl; false → refl})
                       (π₁
                        (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                         (λ {true → refl; false → refl})))
                       (π₂
                        (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                         (λ {true → refl; false → refl})))
                       y))))))
               (π₁
                (π₁
                 (univalence bool bool
                  (negation ,
                   (λ y →
                      (negation y , (λ {true → refl; false → refl}) y) ,
                      .Equivalences._._.path negation negation
                      (λ {true → refl; false → refl})
                      (π₁
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      (π₂
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      y)))))
               (π₁
                (π₁
                 (univalence bool bool
                  (negation ,
                   (λ y →
                      (negation y , (λ {true → refl; false → refl}) y) ,
                      .Equivalences._._.path negation negation
                      (λ {true → refl; false → refl})
                      (π₁
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      (π₂
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      y))))))

              ap
              (λ q →
                 q ∘
                 π₁
                 (π₁
                  (univalence bool bool
                   (negation ,
                    (λ y →
                       (negation y , (λ {true → refl; false → refl}) y) ,
                       .Equivalences._._.path negation negation
                       (λ {true → refl; false → refl})
                       (π₁
                        (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                         (λ {true → refl; false → refl})))
                       (π₂
                        (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                         (λ {true → refl; false → refl})))
                       y)))))
              (opposite-left-inverse
               (π₁
                (π₁
                 (univalence bool bool
                  (negation ,
                   (λ y →
                      (negation y , (λ {true → refl; false → refl}) y) ,
                      .Equivalences._._.path negation negation
                      (λ {true → refl; false → refl})
                      (π₁
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      (π₂
                       (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                        (λ {true → refl; false → refl})))
                      y))))))
              ∘ refl)
             (transport
              (λ A₁ →
                 (x y : A₁) (x₁ y₁ : x ≡ y) →
                 Σ (x₁ ≡ y₁) (λ x₂ → (y₂ : x₁ ≡ y₁) → y₂ ≡ x₂))
              (π₁
               (π₁
                (univalence bool bool
                 (negation ,
                  (λ y →
                     (negation y , (λ {true → refl; false → refl}) y) ,
                     .Equivalences._._.path negation negation
                     (λ {true → refl; false → refl})
                     (π₁
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     (π₂
                      (iso-is-adjiso negation negation (λ {true → refl; false → refl})
                       (λ {true → refl; false → refl})))
                     y)))))
              bool-is-set))
            bool-is-set))
          ∘ refl))))
      true

And this is why we really need canonicity!


\begin{code}

A₀≃A₀' : A O  A₀'
A₀≃A₀' = 
  let
    f : A O  A₀'
    f = λ {(X , (p , b))  (X , (b , p))}
    g : A₀'  A O
    g = λ {(X , (b , p))  (X , (p , b))}
  in    
    f , iso-is-eq f g  {(_ , (_ , _))  refl})  {(_ , (_ , _))  refl})

e₀₁ : (r=r (S O) (A O))  ((a : A O)  a  a)
e₀₁ = e1 O

-- Could be that there is a library lemma for this
e₀₂ : ((a : A O)  a  a)  ((a : A₀')  a  a)
e₀₂ = path-to-eq (ap  AA  ((a : AA)  a  a)) (eq-to-path A₀≃A₀'))

A₀-triv : (a : A O)  a  a
A₀-triv  = (e₀₂ ⁻¹  A₀'-triv)

A₀-nontriv : (a : A O)  a  a
A₀-nontriv = (e₀₂ ⁻¹  A₀'-nontriv)


triv≢nontriv : A₀-triv  A₀-nontriv
triv≢nontriv t≡nt = triv≢nontriv' (! (inverse-right-inverse e₀₂ _)  (ap (π₁ e₀₂) t≡nt)  inverse-right-inverse e₀₂ _)


-- If a type is a set, then it is also an n-Type for any n > 0.
-- We only found the 1-step-version in the library.
ugly-lemma :  {i} {X : Set i} (n : )  (is-set X)  (is-truncated  n  X)
ugly-lemma O issetX = issetX
ugly-lemma (S n) issetX = truncated-is-truncated-S  n  (ugly-lemma n issetX)

b : (n : )  is-truncated  S n  (A n)
b n = 
  let
    Ty≤×rr-is-truncated : is-truncated  S n  (Σ (Type≤  n  (ℕ→Level n)) λ Xh  (r=r n (π₁ Xh)))
    Ty≤×rr-is-truncated = Σ-is-truncated 
                             S n  
                            (Type≤-is-truncated  n  _) 
                            λ Xh  let
                                      is-set-rrX : is-set (r=r n (π₁ Xh))
                                      is-set-rrX = bound-reduce-cor n (π₁ Xh) (π₂ Xh)
                                      is-hSn-rrx : is-truncated  S n  (r=r n (π₁ Xh))
                                      is-hSn-rrx = ugly-lemma (S n) is-set-rrX
                                    in
                                      is-hSn-rrx 
    An-is-truncated     : is-truncated  S n  (A n)
    An-is-truncated     = equiv-types-truncated  S n  ((An≃Ty≤×rr n) ⁻¹) Ty≤×rr-is-truncated
  in 
    An-is-truncated

v : (n : )  r=r (S n) (A n)
v O = (e₀₁ ⁻¹)  A₀-nontriv 
v (S n) = ((e n) ⁻¹)   (a : A (S n))  π₂ (π₂ a))

w : (n : )  r=r (S n) (A n)
w O = (e₀₁ ⁻¹)  A₀-triv 
w (S n) = ((e n) ⁻¹)   (a : A (S n))  refl) -- of course, we could just write 'refl', but then, we would have to prove that e is stable

t : (n : )  (v n)  (w n)
t O = λ vO≡wO 
      let
        A₀-nontriv≡A₀-triv :  A₀-nontriv  A₀-triv 
        A₀-nontriv≡A₀-triv = A₀-nontriv                    ≡⟨ ! (inverse-right-inverse (e₀₁) _) 
                              e₀₁  ((e₀₁ ⁻¹)  A₀-nontriv) ≡⟨ refl 
                              e₀₁  (v O)                   ≡⟨ ap (π₁ e₀₁) vO≡wO 
                              e₀₁  (w O)                   ≡⟨ refl 
                              e₀₁  ((e₀₁ ⁻¹)  A₀-triv)    ≡⟨ inverse-right-inverse e₀₁ _ 
                              A₀-triv                        
      in
        triv≢nontriv (! A₀-nontriv≡A₀-triv) 
t (S n) = λ vSn≡wSn  
  let
    π₂π₂≡refl :  (a : A (S n))  π₂ (π₂ a))   (a : A (S n))  refl)
    π₂π₂≡refl  = ! (inverse-right-inverse (e n) _)  (ap (π₁ (e n)) vSn≡wSn)  inverse-right-inverse (e n) _
    vn≡wn     : (v n)  (w n)
    vn≡wn     = let
                   vn≡refl : v n  refl
                   vn≡refl = ap  f  f (A n , (b n , v n))) π₂π₂≡refl
                   wn≡refl : w n  refl
                   wn≡refl = ap  f  f (A n , (b n , w n))) π₂π₂≡refl
                 in
                   vn≡refl  ! wn≡refl
  in
    (t n) vn≡wn



-- a lemma: reflⁿA ≡ reflⁿA is not a set
not-set-rr-n-A : (n : )  ¬ (is-set (r=r n (A n)))
not-set-rr-n-A n set = 
  let
    prop : is-prop (r=r (S n) (A n))
    prop = set refl refl
    v≡w : (v n)  (w n)
    v≡w = π₁ (prop (v n) (w n))
  in
    (t n) v≡w

\end{code}

  #############################################
  ## THEOREM 1. For all n, there exists a    ##
  ##            strict (n+1)-Type.           ##
  #############################################

\begin{code}

strict-n+1-type : (n : ) 
   Σ (Set (suc (ℕ→Level n)))
      λ A     
        (is-truncated  S n  A) × ¬ (is-truncated  n  A)
strict-n+1-type n = 
  (A n) , ((b n) ,  A-is-n-type  not-set-rr-n-A n (bound-reduce-cor n (A n) A-is-n-type)))

\end{code}

  #############################################
  ## THEOREM 2. Universe n is not an n-type. ##
  #############################################

\begin{code}

Un-is-not-an-n-Type : (n : )  ¬ (is-truncated  n  (Set (ℕ→Level n)))
Un-is-not-an-n-Type O = U₀-not-a-set
Un-is-not-an-n-Type (S n) = λ h_SnU_Sn  not-set-rr-n-A n (bound-reduce n _ h_SnU_Sn (A n))

\end{code}