eval

Documentation

Overview

Package eval implements Normalization by Evaluation (NbE) for the HoTT kernel. This file provides alpha-equality checking for AST terms.

Package eval implements Normalization by Evaluation (NbE) for the HoTT kernel.

NbE is a technique for normalizing lambda calculus terms by evaluating syntax into a semantic domain and then reifying values back to normal form. This approach is more efficient than repeated syntactic reduction and naturally handles evaluation under binders.

Overview

The normalization process has three phases:

1. Eval: syntax → semantic values (Values)
2. Apply: handle applications (performs beta reduction)
3. Reify: semantic values → syntax in normal form

Semantic Domain

The Value interface represents semantic values:

• VLam - lambda closures capturing environment
• VPi - Pi type with domain value and codomain closure
• VSigma - Sigma type with domain value and codomain closure
• VPair - pairs in weak head normal form
• VSort - universe sorts
• VGlobal - global constant references
• VNeutral - stuck computations (see below)
• VId - identity type values
• VRefl - reflexivity proof values

Closures

Closure captures an environment and a term for lazy evaluation under binders. When a lambda is evaluated, it becomes a VLam containing a closure. When applied, the closure's term is evaluated in an extended environment.

Neutral Terms

Neutral represents stuck computations - terms that cannot reduce further because they're blocked on a variable. A neutral term has:

• Head - either a de Bruijn variable index or global name
• Spine - list of arguments already applied

For example, (x 1 2) where x is a variable becomes a neutral with head x and spine [1, 2].

Environment

Env maps de Bruijn indices to Values:

• Lookup(ix) - retrieves value at index, returns neutral if unbound
• Extend(v) - adds binding at index 0, shifting others up

Key Functions

• Eval - evaluates a term to weak head normal form
• Apply - applies a function value to an argument
• Reify - converts a value back to syntax in normal form
• EvalNBE - convenience: Eval + Reify in one call
• Fst, Snd - projections in the semantic domain

Debug Mode

The DebugMode variable (set via HOTTGO_DEBUG=1) controls error handling:

• When true: internal errors cause panics for easier debugging
• When false: errors return diagnostic fallback values

Well-typed inputs should never trigger these error paths.

Recursor Reduction

The evaluator handles computation rules for eliminators:

• natElim P pz ps zero → pz
• natElim P pz ps (succ n) → ps n (natElim P pz ps n)
• boolElim P pt pf true → pt
• boolElim P pt pf false → pf
• J A C d x x (refl A x) → d

User-defined recursors are handled via the recursor registry.

Cubical Extensions

When cubical features are enabled, additional Value types and evaluation rules are defined in nbe_cubical.go for paths, transport, composition, etc.

References

• Abel, A. "Normalization by Evaluation: Dependent Types and Impredicativity"
• Coquand, T. "An Algorithm for Type-Checking Dependent Types"

Package eval implements Normalization by Evaluation (NbE) for the HoTT kernel.

NbE is a technique for normalizing lambda calculus terms by:

1. Evaluating syntax into a semantic domain (Values)
2. Reifying Values back to syntax in normal form

The semantic domain uses closures for lazy evaluation under binders, and neutral terms to represent stuck computations (e.g., variable applications).

Key concepts:

• Value: semantic representation (VLam, VPi, VSigma, VPair, VSort, VNeutral)
• Closure: captures environment + term for delayed evaluation
• Neutral: stuck computation with head variable and argument spine
• Env: de Bruijn environment mapping indices to Values

References:

• Abel, A. "Normalization by Evaluation: Dependent Types and Impredicativity"
• Coquand, T. "An Algorithm for Type-Checking Dependent Types"

Package eval provides NbE for the HoTT kernel. This file contains cubical type theory extensions.

Index

• Variables
• func AlphaEq(a, b ast.Term) bool
• func ClearRecursorRegistry()
• func DebugValue(v Value) string
• func EvalNBE(t ast.Term) ast.Term
• func IsFaceFalse(f FaceValue) bool
• func IsFaceTrue(f FaceValue) bool
• func NeutralEqual(n1, n2 Neutral) bool
• func Normalize(t ast.Term) ast.Term
• func NormalizeNBE(t ast.Term) string
• func PrettyNeutral(n Neutral) string
• func PrettyValue(v Value) string
• func RegisterRecursor(info *RecursorInfo)
• func Reify(v Value) ast.Term
• func ReifyCubicalAt(level int, ilevel int, v Value) ast.Term
• func SprintNeutral(n Neutral) string
• func SprintValue(v Value) string
• func ValueEqual(v1, v2 Value) bool
• type BoundarySpec
• type BoundaryVal
• type Closure
• type ConstructorInfo
• type Env
  • func (e *Env) Extend(v Value) *Env
  • func (e *Env) Lookup(ix int) Value
• type FaceValue
• type Head
• type IClosure
• type IEnv
  • func EmptyIEnv() *IEnv
  • func (ie *IEnv) Extend(v Value) *IEnv
  • func (ie *IEnv) ILen() int
  • func (ie *IEnv) Lookup(ix int) Value
• type Neutral
• type PathConstructorInfo
• type RecursorInfo
  • func LookupRecursor(elimName string) *RecursorInfo
• type VComp
• type VFaceAnd
• type VFaceBot
• type VFaceEq
• type VFaceOr
• type VFaceTop
• type VFill
• type VGlobal
• type VGlue
• type VGlueBranch
• type VGlueElem
• type VGlueElemBranch
• type VHComp
• type VHITPathCtor
• type VI0
• type VI1
• type VIVar
• type VId
• type VLam
• type VNeutral
• type VPair
• type VPartial
• type VPath
• type VPathLam
• type VPathP
• type VPi
• type VRefl
• type VSigma
• type VSort
• type VSystem
• type VSystemBranch
• type VTransport
• type VUA
• type VUABeta
• type VUnglue
• type Value
  • func Apply(fun Value, arg Value) Value
  • func Eval(env *Env, t ast.Term) Value
  • func EvalComp(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value
  • func EvalCubical(env *Env, ienv *IEnv, t ast.Term) Value
  • func EvalFill(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value
  • func EvalGlue(a Value, branches []VGlueBranch) Value
  • func EvalGlueElem(branches []VGlueElemBranch, base Value) Value
  • func EvalHComp(a Value, phi FaceValue, tubeClosure *IClosure, base Value) Value
  • func EvalTransport(aClosure *IClosure, e Value) Value
  • func EvalUA(a, b, equiv Value) Value
  • func EvalUABeta(equiv, arg Value) Value
  • func EvalUnglue(ty Value, g Value) Value
  • func Fst(v Value) Value
  • func MakeNeutralGlobal(name string) Value
  • func PathApply(p Value, r Value) Value
  • func Snd(v Value) Value
  • func UAPathApply(ua VUA, r Value) Value

Variables

var DebugMode = os.Getenv("HOTTGO_DEBUG") == "1"

DebugMode enables strict error handling for NbE. When true, internal errors panic instead of returning fallback values. Set via HOTTGO_DEBUG=1 environment variable or programmatically.

Functions

func AlphaEq

func AlphaEq(a, b ast.Term) bool

AlphaEq checks if two terms are alpha-equal. Terms are alpha-equal if they have the same structure and all binders correspond correctly. Since we use de Bruijn indices, binder names are irrelevant and structurally identical terms are alpha-equal.

func ClearRecursorRegistry

func ClearRecursorRegistry()

ClearRecursorRegistry clears all registered recursors (useful for testing).

func DebugValue

func DebugValue(v Value) string

DebugValue provides detailed debug information about a Value.

func EvalNBE

func EvalNBE(t ast.Term) ast.Term

EvalNBE is a convenience function that evaluates and reifies a term using NbE.

func IsFaceFalse

func IsFaceFalse(f FaceValue) bool

IsFaceFalse checks if a face value is definitely false.

func IsFaceTrue

func IsFaceTrue(f FaceValue) bool

IsFaceTrue checks if a face value is definitely true.

func NeutralEqual

func NeutralEqual(n1, n2 Neutral) bool

NeutralEqual compares two Neutrals for structural equality.

func Normalize

func Normalize(t ast.Term) ast.Term

Normalize reduces a term to weak head normal form using beta-reduction and projections.

func NormalizeNBE

func NormalizeNBE(t ast.Term) string

NormalizeNBE normalizes a term using NbE and returns its string representation. This function provides compatibility with existing test expectations.

func PrettyNeutral

func PrettyNeutral(n Neutral) string

PrettyNeutral converts a Neutral to a stable string representation for testing.

func PrettyValue

func PrettyValue(v Value) string

PrettyValue converts a Value to a stable string representation for testing. This ensures deterministic output for golden tests.

func RegisterRecursor

func RegisterRecursor(info *RecursorInfo)

RegisterRecursor registers an eliminator for generic reduction. This should be called when declaring an inductive type.

func Reify

func Reify(v Value) ast.Term

Reify converts a Value back to an ast.Term in normal form.

This is the "read back" phase of NbE that extracts syntax from semantics:

• VLam: applies to a fresh variable, reifies the result under a binder
• VPi/VSigma: reifies domain, applies closure to fresh var for codomain
• VPair: reifies both components
• VNeutral: reconstructs term from head and spine
• VSort/VGlobal: direct conversion

The result is in beta-normal form (no reducible beta redexes). Uses level-indexed fresh variables for correct de Bruijn handling under binders.

func ReifyCubicalAt

func ReifyCubicalAt(level int, ilevel int, v Value) ast.Term

ReifyCubicalAt reifies a value at given term and interval levels.

func SprintNeutral

func SprintNeutral(n Neutral) string

SprintNeutral returns a string representation of a Neutral for debugging and testing.

func SprintValue

func SprintValue(v Value) string

SprintValue returns a string representation of a Value for debugging and testing.

func ValueEqual

func ValueEqual(v1, v2 Value) bool

ValueEqual compares two Values for structural equality (useful for testing).

Types

type BoundarySpec

type BoundarySpec struct {
	AtZeroVal Value // Evaluated value when interval = i0
	AtOneVal  Value // Evaluated value when interval = i1
}

BoundarySpec specifies boundary values for one interval dimension.

type BoundaryVal

type BoundaryVal struct {
	AtZero Value // Value when interval = i0
	AtOne  Value // Value when interval = i1
}

BoundaryVal stores evaluated boundary values for a path constructor.

type Closure

type Closure struct {
	Env  *Env
	Term ast.Term
}

Closure captures an environment and a term for lazy evaluation.

type ConstructorInfo

type ConstructorInfo struct {
	Name         string // Constructor name (e.g., "zero", "succ")
	NumArgs      int    // Total number of arguments
	RecursiveIdx []int  // Indices of recursive arguments (need IH)
	// IndexArgPositions maps each recursive arg to the positions of its index args.
	// For Vec's vcons with data args [n, x, xs] where xs : Vec A n:
	//   IndexArgPositions[2] = []int{0}  (xs at position 2 uses n at position 0)
	// For non-indexed inductives or non-recursive args, entries are nil.
	IndexArgPositions map[int][]int
	// RecursiveArgElims maps each recursive arg position to the eliminator name
	// for that arg's type. Currently unused because we use SEPARATE eliminators
	// for mutual types (each type gets its own eliminator, no cross-type IHs).
	// This field is reserved for future JOINT eliminator support where cross-type
	// IHs would require looking up different eliminators.
	// For the current separate eliminator design, all entries equal RecursorInfo.ElimName.
	RecursiveArgElims map[int]string
}

ConstructorInfo contains information about a single constructor.

type Env

type Env struct {
	Bindings []Value
}

Env represents an evaluation environment mapping de Bruijn indices to Values.

func (*Env) Extend

func (e *Env) Extend(v Value) *Env

Extend adds a new binding to the front of the environment.

func (*Env) Lookup

func (e *Env) Lookup(ix int) Value

Lookup retrieves a value by de Bruijn index.

type FaceValue

type FaceValue interface {
	Value
	// contains filtered or unexported methods
}

FaceValue is the interface for face formula values.

type Head

type Head struct {
	Var  int    // de Bruijn index
	Glob string // global name
}

Head represents the head of a neutral term.

type IClosure

type IClosure struct {
	Env  *Env     // Term environment
	IEnv *IEnv    // Interval environment
	Term ast.Term // Body term
}

IClosure captures both term and interval environments with a term. Used for constructs that bind an interval variable.

type IEnv

type IEnv struct {
	Bindings []Value // Must be VI0, VI1, or VIVar
}

IEnv represents an interval evaluation environment. Maps interval de Bruijn indices to interval values (VI0, VI1, VIVar).

func EmptyIEnv

func EmptyIEnv() *IEnv

EmptyIEnv returns an empty interval environment.

func (*IEnv) Extend

func (ie *IEnv) Extend(v Value) *IEnv

Extend adds a new binding to the front of the interval environment.

func (*IEnv) ILen

func (ie *IEnv) ILen() int

ILen returns the number of bindings in the interval environment.

func (*IEnv) Lookup

func (ie *IEnv) Lookup(ix int) Value

Lookup retrieves an interval value by de Bruijn index.

type Neutral

type Neutral struct {
	Head Head
	Sp   []Value
}

Neutral represents stuck terms with a head and spine of arguments.

type PathConstructorInfo

type PathConstructorInfo struct {
	Name       string         // Constructor name (e.g., "loop")
	Level      int            // Dimension: 1=path, 2=path-of-path, etc.
	NumArgs    int            // Number of arguments before interval args
	Boundaries []BoundarySpec // Boundary specs for each interval dimension
}

PathConstructorInfo contains information about a path constructor in a HIT.

type RecursorInfo

type RecursorInfo struct {
	ElimName   string            // Name of the eliminator (e.g., "natElim")
	IndName    string            // Name of the inductive type (e.g., "Nat")
	NumParams  int               // Number of type parameters (e.g., 1 for List A)
	NumIndices int               // Number of indices (e.g., 1 for Vec A n)
	NumCases   int               // Number of constructor cases
	Ctors      []ConstructorInfo // Info about each constructor

	// HIT-specific fields
	PathCtors []PathConstructorInfo // Info about path constructors (for HITs)
	IsHIT     bool                  // True if this is a Higher Inductive Type
}

RecursorInfo contains the information needed to reduce a recursor application.

func LookupRecursor

func LookupRecursor(elimName string) *RecursorInfo

LookupRecursor returns the RecursorInfo for an eliminator, or nil if not found.

type VComp

type VComp struct {
	A    *IClosure // Type line: I → Type
	Phi  FaceValue // Face constraint
	Tube *IClosure // Partial tube
	Base Value     // Base element
}

VComp represents a stuck heterogeneous composition. Used when the face is not satisfied and reduction cannot proceed.

type VFaceAnd

type VFaceAnd struct {
	Left  FaceValue
	Right FaceValue
}

VFaceAnd represents conjunction of faces: φ ∧ ψ.

type VFaceBot

type VFaceBot struct{}

VFaceBot represents the always-false face formula (⊥).

type VFaceEq

type VFaceEq struct {
	ILevel int  // Interval variable level (for reification)
	IsOne  bool // true for (i = 1), false for (i = 0)
}

VFaceEq represents an endpoint constraint: (i = 0) or (i = 1).

type VFaceOr

type VFaceOr struct {
	Left  FaceValue
	Right FaceValue
}

VFaceOr represents disjunction of faces: φ ∨ ψ.

type VFaceTop

type VFaceTop struct{}

VFaceTop represents the always-true face formula (⊤).

type VFill

type VFill struct {
	A    *IClosure // Type line: I → Type
	Phi  FaceValue // Face constraint
	Tube *IClosure // Partial tube
	Base Value     // Base element
}

VFill represents a stuck fill operation.

type VGlobal

type VGlobal struct{ Name string }

VGlobal represents global constants.

type VGlue

type VGlue struct {
	A      Value         // Base type
	System []VGlueBranch // System of equivalences
}

VGlue represents a Glue type value: Glue A [φ ↦ (T, e)].

type VGlueBranch

type VGlueBranch struct {
	Phi   FaceValue // Face constraint
	T     Value     // Fiber type
	Equiv Value     // Equivalence: Equiv T A
}

VGlueBranch represents a branch in a VGlue value.

type VGlueElem

type VGlueElem struct {
	System []VGlueElemBranch // Partial element in fiber
	Base   Value             // Base element
}

VGlueElem represents a Glue element value: glue [φ ↦ t] a.

type VGlueElemBranch

type VGlueElemBranch struct {
	Phi  FaceValue
	Term Value
}

VGlueElemBranch represents a branch in a VGlueElem value.

type VHComp

type VHComp struct {
	A    Value     // Type (constant)
	Phi  FaceValue // Face constraint
	Tube *IClosure // Partial tube
	Base Value     // Base element
}

VHComp represents a stuck homogeneous composition.

type VHITPathCtor

type VHITPathCtor struct {
	HITName    string        // HIT type name (e.g., "S1")
	CtorName   string        // Path constructor name (e.g., "loop")
	Args       []Value       // Type/term parameters applied to constructor
	IArgs      []Value       // Interval arguments (VI0, VI1, or VIVar)
	Boundaries []BoundaryVal // Boundary values at endpoints
}

VHITPathCtor represents a path constructor applied to interval argument(s). This value reduces to boundary values when applied at endpoints:

loop @ i0 --> base
loop @ i1 --> base

When applied to an interval variable, it remains stuck until eliminated.

type VI0

type VI0 struct{}

VI0 represents the left endpoint of the interval (i0).

type VI1

type VI1 struct{}

VI1 represents the right endpoint of the interval (i1).

type VIVar

type VIVar struct{ Level int }

VIVar represents a neutral interval variable. Level is used for level-indexed reification (similar to term variables).

type VId

type VId struct {
	A Value
	X Value
	Y Value
}

VId represents identity type values.

type VLam

type VLam struct{ Body *Closure }

VLam represents lambda closures.

type VNeutral

type VNeutral struct{ N Neutral }

VNeutral represents neutral terms (stuck computations).

type VPair

type VPair struct{ Fst, Snd Value }

VPair represents pairs in WHNF.

type VPartial

type VPartial struct {
	Phi FaceValue // The face constraint
	A   Value     // The type
}

VPartial represents a partial type value: Partial φ A.

type VPath

type VPath struct {
	A Value // Type
	X Value // Left endpoint
	Y Value // Right endpoint
}

VPath represents non-dependent path type values: Path A x y.

type VPathLam

type VPathLam struct {
	Body *IClosure // Body with interval variable bound
}

VPathLam represents path abstraction values: <i> t.

type VPathP

type VPathP struct {
	A *IClosure // Type family: I → Type
	X Value     // Left endpoint
	Y Value     // Right endpoint
}

VPathP represents dependent path type values: PathP A x y.

type VPi

type VPi struct {
	A Value
	B *Closure
}

VPi represents Pi type closures (optional for now).

type VRefl

type VRefl struct {
	A Value
	X Value
}

VRefl represents reflexivity proof values.

type VSigma

type VSigma struct {
	A Value
	B *Closure
}

VSigma represents Sigma type closures (optional for now).

type VSort

type VSort struct{ Level int }

VSort represents universe sorts.

type VSystem

type VSystem struct {
	Branches []VSystemBranch
}

VSystem represents a system of partial elements.

type VSystemBranch

type VSystemBranch struct {
	Phi  FaceValue
	Term Value
}

VSystemBranch represents a single branch in a system value.

type VTransport

type VTransport struct {
	A *IClosure // Type family: I → Type
	E Value     // Element at i0
}

VTransport represents stuck transport values. Used when A is not constant and reduction cannot proceed.

type VUA

type VUA struct {
	A     Value // Source type
	B     Value // Target type
	Equiv Value // Equivalence: Equiv A B
}

VUA represents ua e : Path Type A B. ua is defined as: ua e = <i> Glue B [(i=0) ↦ (A, e)]

type VUABeta

type VUABeta struct {
	Equiv Value // The equivalence e
	Arg   Value // The argument a : A
}

VUABeta represents the computation result: transport (ua e) a = e.fst a.

type VUnglue

type VUnglue struct {
	Ty Value // The Glue type
	G  Value // The Glue element
}

VUnglue represents a stuck unglue operation.

type Value

type Value interface {
	// contains filtered or unexported methods
}

Value is the semantic domain for NbE.

func Apply

func Apply(fun Value, arg Value) Value

Apply performs function application in the semantic domain.

This is the key operation for beta reduction in NbE:

• VLam: performs beta reduction by extending the closure's environment with the argument and evaluating the body
• VNeutral: extends the spine with the new argument (stuck application), and checks for recursor computation rules
• Other: creates a "bad_app" neutral term (type error in well-typed terms)

func Eval

func Eval(env *Env, t ast.Term) Value

Eval evaluates a term in an environment to weak head normal form (WHNF).

Evaluation proceeds recursively, handling each term constructor:

• Var: lookup in environment, return neutral if unbound
• Lam: create closure capturing current environment
• App: evaluate function and argument, then apply
• Pi/Sigma: evaluate domain, create closure for codomain
• Pair: evaluate both components
• Fst/Snd: evaluate pair and project
• Let: evaluate definition, extend environment, evaluate body
• Sort/Global: convert directly to corresponding Value

If env is nil, an empty environment is used. If t is nil, returns an error value (or panics in debug mode).

func EvalComp

func EvalComp(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value

EvalComp evaluates heterogeneous composition: comp^i A [φ ↦ u] a₀. Computation rules:

comp^i A [1 ↦ u] a₀  ⟶  u[i1/i]         (face satisfied)
comp^i A [0 ↦ _] a₀  ⟶  transport A a₀  (face empty)

func EvalCubical

func EvalCubical(env *Env, ienv *IEnv, t ast.Term) Value

EvalCubical evaluates a term with both term and interval environments. This is the main entry point for cubical evaluation.

func EvalFill

func EvalFill(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value

EvalFill evaluates the filler: fill^i A [φ ↦ u] a₀. Fill produces a path-like value that can be applied to an interval. The computation rules are handled in PathApply:

fill^i A [φ ↦ u] a₀ @ i0 = a₀
fill^i A [φ ↦ u] a₀ @ i1 = comp^i A [φ ↦ u] a₀

If the face is satisfied (φ = ⊤), we can reduce immediately:

fill^i A [1 ↦ u] a₀ = <j> u[j/i]

func EvalGlue

func EvalGlue(a Value, branches []VGlueBranch) Value

EvalGlue evaluates a Glue type: Glue A [φ ↦ (T, e)]. Computation rules:

Glue A [⊤ ↦ (T, e)] = T    (face satisfied)
Glue A []           = A    (no branches)

func EvalGlueElem

func EvalGlueElem(branches []VGlueElemBranch, base Value) Value

EvalGlueElem evaluates a Glue element: glue [φ ↦ t] a. Computation rules:

glue [⊤ ↦ t] a = t    (face satisfied)

func EvalHComp

func EvalHComp(a Value, phi FaceValue, tubeClosure *IClosure, base Value) Value

EvalHComp evaluates homogeneous composition: hcomp A [φ ↦ u] a₀. Computation rules:

hcomp A [1 ↦ u] a₀  ⟶  u[i1/i]   (face satisfied)
hcomp A [0 ↦ _] a₀  ⟶  a₀        (face empty, identity)

func EvalTransport

func EvalTransport(aClosure *IClosure, e Value) Value

EvalTransport evaluates transport (λi. A) e. The computation rule is: transport (λi. A) e --> e when A is constant in i.

func EvalUA

func EvalUA(a, b, equiv Value) Value

EvalUA evaluates ua e : Path Type A B. Definition via Glue:

ua e = <i> Glue B [(i=0) ↦ (A, e)]

At i=0: Glue B [⊤ ↦ (A, e)] = A At i=1: Glue B [⊥ ↦ (A, e)] = B

func EvalUABeta

func EvalUABeta(equiv, arg Value) Value

EvalUABeta evaluates the transport computation: transport (ua e) a = e.fst a. The equivalence e : Equiv A B has the form (fwd, proof) where fwd : A -> B. This computation rule extracts the forward function and applies it to the argument. When the equivalence is neutral (stuck), we return VUABeta to preserve the structure.

func EvalUnglue

func EvalUnglue(ty Value, g Value) Value

EvalUnglue evaluates unglue: unglue g. Computation rules:

unglue (glue [φ ↦ t] a) = a    (definitional)

func Fst

func Fst(v Value) Value

Fst performs first projection in the semantic domain.

func MakeNeutralGlobal

func MakeNeutralGlobal(name string) Value

MakeNeutralGlobal creates a neutral value from a global name. Exported for testing purposes.

func PathApply

func PathApply(p Value, r Value) Value

PathApply applies a path to an interval argument. Implements the computation rules:

(<i> t) @ i0  -->  t[i0/i]
(<i> t) @ i1  -->  t[i1/i]
(<i> t) @ j   -->  t[j/i]

For PathP types (dependent path types), endpoint values are returned:

(PathP A x y) @ i0  -->  x
(PathP A x y) @ i1  -->  y

func Snd

func Snd(v Value) Value

Snd performs second projection in the semantic domain.

func UAPathApply

func UAPathApply(ua VUA, r Value) Value

UAPathApply applies ua to an interval argument. This is called when we have (ua e) @ r.

(ua e) @ i0 = A
(ua e) @ i1 = B
(ua e) @ i  = Glue B [(i=0) ↦ (A, e)]