{-# OPTIONS --safe #-}

open import Prelude

module Truth.MonoLevel (ℓ : Level) where

import Truth as Poly

open Poly using (proves; disproves)

Ω : Type (ℓsuc ℓ)
Ω = Poly.Ω ℓ

True : Ω
True = Poly.True

False : Ω
False = Poly.False

|T| : Bool → Ω
|T| = Poly.|T|

distinct :
  ¬ (Σ[ p ⦂ Ω ] × p ≢ True × p ≢ False)
distinct (p , p≢True , p≢False) = p≢False (disproves (p≢True ∘ proves))