Agda.TypeChecking.Telescope.Path

In an ambient context Γ, telePiPath f lams Δ t bs builds a type that can be telViewPathBoundaryed into (TelV Δ t, bs'). Γ.Δ ⊢ t bs = [(i,u_i)] Δ = Δ0,(i : I),Δ1 ∀ b ∈ {0,1}. Γ.Δ0 | lams Δ1 (u_i .b) : (telePiPath f Δ1 t bs)(i = b) -- kinda: see lams Γ ⊢ telePiPath f Δ t bs

telePiPath_ Δ t [(i,u)] Δ ⊢ t i ∈ Δ Δ ⊢ u_b : t for b ∈ {0,1}

arity of the type, including both Pi and Path. Does not reduce the type.

Collect the interval copattern variables as list of de Bruijn indices.

Check whether a type is the built-in interval type.