```module LevitationUniverse where

-- * Public library

open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

data Level : Set where
zero : Level
suc : (l : Level) → Level

-- * Required set formers

-- ** Σ
open import Data.Product
-- ** 0
open import Data.Empty
-- ** 1
open import Data.Unit
-- ** 2
open import Data.Bool

-- ** 4
data DescConst : Set where
`1 : DescConst
`X : DescConst
`Π : DescConst
`Σ : DescConst

-- (Conveniently named to suit my needs)

-- ** W-types

data W (S : Set)(P : S → Set) : Set where
In : (s : S)(p : P s → W S P) → W S P

-- * Universe construction

-- ** Next universe operator

mutual
data Û (U : Set)(El : U → Set) : Set where
-- Closed under next universe:
`U : Û U El
`El : (t : U) → Û U El
`Π : (S : Û U El)(T : Êl S → Û U El) → Û U El
`Σ : (S : Û U El)(T : Êl S → Û U El) → Û U El
`0 : Û U El
`1 : Û U El
`2 : Û U El
`4 : Û U El
`W : (S : Û U El)(P : Êl S → Û U El) → Û U El

Êl : ∀{U El} → Û U El → Set
Êl {U} `U = U
Êl {U}{El} (`El t) = El t
Êl (`Π S T) = (s : Êl S) → Êl (T s)
Êl (`Σ S T) = Σ[ s ∶ Êl S ] Êl (T s)
Êl `0 = ⊥
Êl `1 = ⊤
Êl `2 = Bool
Êl `4 = DescConst
Êl (`W S P) = W (Êl S) (λ s → Êl (P s))

-- ** Hierarchy of universes

mutual
U⁺ : Level → Set
U⁺ zero = ⊥
U⁺ (suc n) = Û (U⁺ n) El⁺

El⁺ : {n : Level} → U⁺ n → Set
El⁺ {zero} ()
El⁺ {(suc n)} t = Êl t

-- Achtung! The level 0 in (U⁺ , El⁺) is the boring 1 universe. Our usual
-- type-theories starts at (U⁺ 1 , El⁺ 1):

U : Level → Set
U n = U⁺ (suc n)

El : {n : Level} → U n → Set
El {n} t = El⁺ {suc n} t

-- We will need El quite a lot, so a nice syntax is cool:

[_] : {n : Level} → U n → Set
[ t ] = El t

-- * Descriptions: hard-coded with W-type

-- ** Definition

-- Modelling:
--
-- data Desc (n : Level) : Set (suc n) where
--   `1 : Desc n
--   `X : Desc n
--   `Σ : (S : Set n)(T : S → Desc n) → Desc n
--   `Π : (S : Set n)(T : S → Desc n) → Desc n

-- The definition might seem awkard with its useless units:
-- the point is that the inhabitants of DescW are *exactly* (well,
-- extensionally anyway) the same than the future inhabitants of
-- DescL.

SDescChoices : ∀{n} → DescConst → U (suc n)
SDescChoices `1 = `1
SDescChoices `X = `1
SDescChoices `Σ = `Σ `U (λ S → {- coding noise: -} `Π (`El S) λ _ → `1)
SDescChoices `Π = `Σ `U (λ S → {- coding noise: -} `Π (`El S) λ _ → `1)

SDesc : ∀{n} → U (suc n)
SDesc = `Σ `4 SDescChoices

PDesc : ∀{n} → [ SDesc {n} ] → U (suc n)
PDesc (`1 , tt) = `0
PDesc (`X , tt) = `0
PDesc (`Σ , S , _) = `Σ (`El S) {- coding noise: -} λ _ → `1
PDesc (`Π , S , _) = `Σ (`El S) {- coding noise: -} λ _ → `1

DescW : ∀ n → U (suc n)
DescW n = `W SDesc PDesc

-- ** Constructors

`1` : ∀{n} → [ DescW n ]
`1` = In (`1 , tt) λ ()

`X` : ∀{n} → [ DescW n ]
`X` = In (`X , tt) λ ()

`Σ` : ∀{n} → (S : U n)(T : [ S ] → [ DescW n ]) → [ DescW n ]
`Σ` S T = In (`Σ , S , λ _ → tt) λ {(s , tt) → T s}

`Π` : ∀{n} → (S : U n)(T : [ S ] → [ DescW n ]) → [ DescW n ]
`Π` S T = In (`Π , S , λ _ → tt) λ {(s , tt) → T s}

-- ** Fix-point of descriptions

-- Modelling:
--
-- data μ {n}(D : Desc n) : Set n where
--   In : (xs : ⟦ D ⟧ (μ D)) → μ D

Sh : ∀{n} → [ DescW n ] → U n
Sh (In (`1 , tt) p) = `1
Sh (In (`X , tt) p) = `1
Sh (In (`Σ , S , _) T) = `Σ S λ s → Sh (T (s , tt))
Sh (In (`Π , S , _) T) = `Π S λ s → Sh (T (s , tt))

Pos : ∀{n} → (D : [ DescW n ]) → [ Sh D ] → U n
Pos (In (`1 , tt) _) tt = `0
Pos (In (`X , tt) _) tt = `1
Pos (In (`Σ , S , _) T) (s , sh) = Pos (T (s , tt)) sh
Pos (In (`Π , S , _) T) f = `Σ S λ s → Pos (T (s , tt)) (f s)

μ : ∀{n} → [ DescW n ] → U n
μ D = `W (Sh D) (Pos D)

-- * Levitation

-- ** DescD n : Describe Desc n with Desc (suc n)

-- Modelling:
--
-- DescD : ∀ n → Desc (suc n)
-- DescD n = `Σ` DescConst λ { `1 → `1`
--                           ; `X → `X`
--                           ; `Σ → `Σ` (Set n) (λ S → `Π` S (λ _ → `X`))
--                           ; `Π` → `Σ` (Set n) (λ S → `Π` S (λ _ → `X)) }

DescDChoices : ∀ {n} → DescConst → [ DescW (suc n) ]
DescDChoices `1 = `1`
DescDChoices `X = `1`
DescDChoices `Σ = `Σ` `U (λ S → `Π` (`El S) λ _ → `X`)
DescDChoices `Π = `Σ` `U (λ S → `Π` (`El S) λ _ → `X`)

DescD : ∀ n → [ DescW (suc n) ]
DescD n = `Σ` `4 DescDChoices

-- ** Obtain Desc n

-- Modelling:
--
-- DescL : ∀ n → Set (suc n)
-- DescL n = μ (DescD n)

DescL : ∀ n → U (suc n)
DescL n = μ (DescD n)

-- ** Constructors

`1L` : ∀{n} → [ DescL n ]
`1L` = In (`1 , tt) (λ ())

`XL` : ∀{n} → [ DescL n ]
`XL` = In (`X , tt) (λ ())

`ΣL` : ∀ {n} → (S : U n)(T : [ S ] → [ DescL n ]) → [ DescL n ]
`ΣL` S T = In (`Σ , S , λ s → tt ) λ { (s , _) → T s }

⌊Π⌋ : ∀ {n} → (S : U n)(T : [ S ] → [ DescL n ]) → [ DescL n ]
⌊Π⌋ S T = In (`Π , S , λ s → tt) λ { (s , _) → T s }

-- * Equivalence proof

-- We want to prove that, at every level, the code of descriptions
-- DescW (hard-coded version) and the self-described set of
-- descriptions are isomorphic.
--
-- To this end, we build the two functions, to and from DescL and
-- DescW and show that they are (extensionally) equal.

-- ** Kit: extensional equality

-- *** Universe of proofs

infixr 1 ⊢_
data ⊢_ (X : Set) : Set where
pf : .X → ⊢ X

-- *** Applicative combinators

open import Category.Applicative
open import Category.Applicative.Indexed

Applicative⊢ : RawApplicative ⊢_
Applicative⊢ = record { pure = pf
; _⊛_ = λ {(pf f) (pf a) → pf (f a)} }

open RawIApplicative Applicative⊢ public

-- *** Extensional equality

postulate
extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} →
((x : A) → ⊢ (f x ≡ g x)) → ⊢ (f ≡ g)

-- ** From Levitated to Concrete

-- Morally (and extensionally): an identity!

to : ∀{n} → [ DescL n ] → [ DescW n ]
to (In (`1 , tt) p) = In (`1 , tt) λ ()
-- = `1`
to (In (`X , tt) p) = In (`X , tt) λ ()
-- = `X`
to (In (`Σ , S , x) T) = In (`Σ , S , x) λ s → to (T s)
-- = `Σ` S (λ s → to (T s))
to (In (`Π , S , x) T) = In (`Π , S , x) λ s → to (T s)
-- = ‵Π` S (λ s → to (T s))

-- ** From Concrete to Levitated

-- Morally (and extensionally): an identity!

from : ∀{n} → [ DescW n ] → [ DescL n ]
from (In (`1 , tt) _) = In (`1 , tt) λ ()
-- = ⌊1⌋
from (In (`X , tt) _) = In (`X , tt) λ ()
-- = ⌊X⌋
from (In (`Σ , S , x) T) = In (`Σ , S , x) λ s → from (T s)
-- = ⌊Σ⌋ S (λ s → from (T (true , s)))
from (In (`Π , S , x) T) = In (`Π , S , x) λ s → from (T s)
-- = ⌊Π⌋ S (λ s → from (T (true , s)))

-- ** to ∘ from = id

pf-to-from : ∀{n} → (x : [ DescW n ]) → ⊢ to (from x) ≡ x
pf-to-from (In (`1 , tt) p) = cong (λ p → In (`1 , tt) p)
<\$> extensionality (λ ())
pf-to-from (In (`X , tt) p) = cong (λ p → In (`X , tt) p)
<\$> extensionality (λ ())
pf-to-from (In (`Σ , S) p) = cong (λ p → In (`Σ , S) p)
<\$> extensionality λ x → pf-to-from (p x)
pf-to-from (In (`Π , S) p) = cong (λ p → In (`Π , S) p)
<\$> extensionality λ x → pf-to-from (p x)

-- ** from ∘ to = id

pf-from-to : ∀{n} → (x : [ DescL n ]) → ⊢ from (to x) ≡ x
pf-from-to (In (`1 , tt) p) = cong (λ p → In (`1 , tt) p)
<\$> extensionality (λ ())
pf-from-to (In (`X , tt) p) = cong (λ p → In (`X , tt) p)
<\$> extensionality (λ ())
pf-from-to (In (`Σ , S , f) p) = cong (λ p → In (`Σ , S , f) p)
<\$> extensionality λ s → pf-from-to (p s)
pf-from-to (In (`Π , S , f) p) = cong (λ p → In (`Π , S , f) p)
<\$> extensionality λ s → pf-from-to (p s)

-- * Outro

-- Local Variables:
-- mode: outline-minor
-- outline-regexp: "-- [*\f]+"
-- outline-level: outline-level
-- End:
```