import Level
open import Data.Universe
module README.DependentlyTyped.Term-without-type
(Uni₀ : Universe Level.zero Level.zero)
where
import Axiom.Extensionality.Propositional as E
open import Data.Product
open import Function renaming (const to k)
import README.DependentlyTyped.NBE as NBE; open NBE Uni₀
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Relation.Nullary using (¬_)
abstract
no-closed-neutral : ∀ {σ} → ¬ (ε ⊢ σ ⟨ ne ⟩)
no-closed-neutral (var ())
no-closed-neutral (t₁ · t₂) = no-closed-neutral t₁
no-closed-atomic-normal :
∀ {σ} → ε ⊢ σ atomic-type → ¬ (ε ⊢ σ ⟨ no ⟩)
no-closed-atomic-normal ⋆ (ne ⋆ t) = no-closed-neutral t
no-closed-atomic-normal el (ne el t) = no-closed-neutral t
no-closed-atomic :
E.Extensionality Level.zero Level.zero →
∀ {σ} → ε ⊢ σ atomic-type → ¬ (ε ⊢ σ)
no-closed-atomic ext atomic t =
no-closed-atomic-normal atomic (normalise ext t)
term-without-type :
E.Extensionality Level.zero Level.zero → U₀ →
∃₂ λ Γ σ → ∃ λ (t : Γ ⊢ σ) → ¬ (Γ ⊢ σ type)
term-without-type ext u = (ε , (-, σ) , ƛ (var zero) , proof)
where
σ : IType ε (π el el)
σ = k (U-π (U-el u) (k (U-el u)))
proof : ∀ {σ} → ¬ (ε ⊢ π el el , σ type)
proof (π (el t) (el t′)) = no-closed-atomic ext ⋆ t