module Chapter6.Universe where

open import Function

open import Data.Product
open import Data.Empty
open import Data.Unit
open import Data.Bool

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



data DescConst : Set where
  `1 : DescConst
  `X : DescConst
   : DescConst
   : DescConst

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
    -- Closed under your happiness:
     : (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

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

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.

-- ** From Levitated to Concrete

open import Chapter2.IProp

-- 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)