Agda.Syntax.Internal

x es neutral

Terms are beta normal. Relevance is ignored

f es, possibly a delta/iota-redex

c es or record { fs = es } es allows only Apply and IApply eliminations, and IApply only for data constructors.

dependent or non-dependent function space

Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom .irrAx : .A -> A.

A (part of a) term or type which is only used for internal purposes. Replaces the Sort Prop hack. The String typically describes the location where we create this dummy, but can contain other information as well. The second field accumulates eliminations in case we apply a dummy term to more of them. Dummy terms should never be used in places where they can affect type checking, so syntactic checks are free to ignore the eliminators, which are only there to ease debugging when a dummy term incorrectly leaks into a relevant position.

Prop ℓ, Set ℓ, SSet ℓ.

Propωᵢ, (S)Setωᵢ.

SizeUniv, a sort inhabited by type Size.

LockUniv, a sort for locks.

LevelUniv, a sort inhabited by type Level. When --level-universe isn't on, this universe reduces to Set 0

IntervalUniv, a sort inhabited by the cubical interval.

Sort of the pi type.

Sort of a (non-dependent) function type.

Sort of another sort.

A postulated sort.

A (part of a) term or type which is only used for internal purposes. Replaces the abuse of Prop for a dummy sort. The String typically describes the location where we create this dummy, but can contain other information as well.

Identity substitution. Γ ⊢ IdS : Γ

Empty substitution, lifts from the empty context. First argument is IMPOSSIBLE. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthening substitution. First argument is IMPOSSIBLE. In 'Strengthen err n ρ the number n must be non-negative. This substitution should only be applied to values t for which none of the variables 0 up to n - 1 are free in t[ρ], and in that case n is subtracted from all free de Bruijn indices in t[ρ]. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @

Weakening substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

The body has (at least) one free variable. Danger: unAbs doesn't shift variables properly

c ps The subpatterns do not contain any projection copatterns.

E.g. 5, "hello".

Projection copattern. Can only appear by itself.

Path elimination pattern, like VarP but keeps track of endpoints.

Used for HITs, the QName should be the one from primHComp.

Abs is never NoAbs.