open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.HLevels
open import Cubical.Relation.Nullary
open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.HITs.S1

module TT.Wild.NotSet (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Wild.Syntax X Y

⟦_⟧ₛ : Sort → Type
⟦_⟧ : ∀ {S} → EL S → ⟦ S ⟧ₛ

⟦ con ⟧ₛ = Unit
⟦ sub Δ Γ ⟧ₛ = Unit
⟦ ty A ⟧ₛ = S¹
⟦ tm Γ A ⟧ₛ = Unit

⟦ γ ∘ δ ⟧ = tt
⟦ assoc γ δ θ i ⟧ = tt
⟦ id ⟧ = tt
⟦ idr γ i ⟧ = tt
⟦ idl γ i ⟧ = tt

⟦ A [ γ ]ᵀ ⟧ = ⟦ A ⟧
⟦ []ᵀ-∘ A γ δ i ⟧ = ⟦ A ⟧
⟦ []ᵀ-id A i ⟧ = ⟦ A ⟧
⟦ a [ γ ]ᵗ ⟧ = tt
⟦ []ᵗ-∘ a γ δ i ⟧ = tt
⟦ []ᵗ-id a i ⟧ = tt

⟦ ◇ ⟧ = tt
⟦ ε ⟧ = tt
⟦ ε-∘ γ i ⟧ = tt
⟦ ◇-η i ⟧ = tt

⟦ Γ ▹ A ⟧ = tt
⟦ p ⟧ = tt
⟦ q ⟧ = tt
⟦ γ ⁺ ⟧ = tt
⟦ ⟨ a ⟩ ⟧ = tt
⟦ ⟨⟩-∘ a γ i ⟧ = tt
⟦ ▹-η i ⟧ = tt
⟦ ⁺-∘ γ δ i ⟧ = tt
⟦ ⁺-id i ⟧ = tt

⟦ p-⁺ γ i ⟧ = tt
⟦ []ᵀ-p-⁺ B γ i ⟧ = ⟦ B ⟧
⟦ q-⁺ γ i ⟧ = tt
⟦ p-⟨⟩ a i ⟧ = tt
⟦ []ᵀ-p-⟨⟩ B a i ⟧ = ⟦ B ⟧
⟦ q-⟨⟩ a i ⟧ = tt

⟦ U ⟧ = base
⟦ U-[] γ i ⟧ = loop i
⟦ Â [ γ ]ᵘ ⟧ = tt
⟦ []ᵘ-filler  γ i ⟧ = tt
⟦ El  ⟧ = base
⟦ El-[] Â γ i ⟧ = base

⟦ Π A B ⟧ = base
⟦ Π-[] A B γ i ⟧ = base
⟦ app f ⟧ = tt
⟦ lam b ⟧ = tt
⟦ lam-[] b γ i ⟧ = tt
⟦ Π-β b i ⟧ = tt
⟦ Π-η f i ⟧ = tt

⟦ in-X x ⟧ = tt
⟦ in-Y y ⟧ = tt

möbius : S¹ → Type
möbius base = Bool
möbius (loop i) = notEq i

odd? : base ≡ base → Bool
odd? e = subst möbius e false

refl≢loop : ¬ refl ≡ loop
refl≢loop e = false≢true (cong odd? e)

[]ᵀ-id≢U-[] : ¬ []ᵀ-id {◇} U ≡ U-[] {◇} id
[]ᵀ-id≢U-[] e = refl≢loop (cong (cong ⟦_⟧) e)

¬isSetTy : ¬ ((Γ : Con) → isSet (Ty Γ))
¬isSetTy f = []ᵀ-id≢U-[] (f ◇ (U [ id ]ᵀ) U ([]ᵀ-id U) (U-[] id))