module LevitationUniverse where
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
data Level : Set where
zero : Level
suc : (l : Level) → Level
open import Data.Product
open import Data.Empty
open import Data.Unit
open import Data.Bool
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
mutual
data Û (U : Set)(El : U → Set) : Set where
`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))
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
U : Level → Set
U n = U⁺ (suc n)
El : {n : Level} → U n → Set
El {n} t = El⁺ {suc n} t
[_] : {n : Level} → U n → Set
[ t ] = El t
SDescChoices : ∀{n} → DescConst → U (suc n)
SDescChoices `1 = `1
SDescChoices `X = `1
SDescChoices `Σ = `Σ `U (λ S → `Π (`El S) λ _ → `1)
SDescChoices `Π = `Σ `U (λ S → `Π (`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) λ _ → `1
PDesc (`Π , S , _) = `Σ (`El S) λ _ → `1
DescW : ∀ n → U (suc n)
DescW n = `W SDesc PDesc
`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}
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)
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
DescL : ∀ n → U (suc n)
DescL n = μ (DescD n)
`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 }
infixr 1 ⊢_
data ⊢_ (X : Set) : Set where
pf : .X → ⊢ X
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
postulate
extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} →
((x : A) → ⊢ (f x ≡ g x)) → ⊢ (f ≡ g)
to : ∀{n} → [ DescL n ] → [ DescW n ]
to (In (`1 , tt) p) = In (`1 , tt) λ ()
to (In (`X , tt) p) = In (`X , tt) λ ()
to (In (`Σ , S , x) T) = In (`Σ , S , x) λ s → to (T s)
to (In (`Π , S , x) T) = In (`Π , S , x) λ s → to (T s)
from : ∀{n} → [ DescW n ] → [ DescL n ]
from (In (`1 , tt) _) = In (`1 , tt) λ ()
from (In (`X , tt) _) = In (`X , tt) λ ()
from (In (`Σ , S , x) T) = In (`Σ , S , x) λ s → from (T s)
from (In (`Π , S , x) T) = In (`Π , S , x) λ s → from (T s)
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)
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)