ast

package
v1.7.1 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jan 8, 2026 License: MIT Imports: 4 Imported by: 0

Documentation

Overview

Package ast defines the abstract syntax tree for the HoTT kernel.

This package provides the core term representation used throughout the type checker and evaluator. All terms use de Bruijn indices for variable binding, which eliminates name capture issues during substitution.

Term Interface

All syntax nodes implement the Term interface via a private isCoreTerm() method. This includes both standard type-theoretic constructs and cubical type theory extensions.

Base Types

  • Sort - universes Type^n where n is a Level
  • Var - de Bruijn indexed variables (0 = innermost binder)
  • Global - references to named global definitions

Function Types (Π)

  • Pi - dependent function types (x:A) → B
  • Lam - lambda abstractions λx.t
  • App - function application (t u)

Dependent Pairs (Σ)

  • Sigma - dependent pair types (x:A) × B
  • Pair - pair constructors (a, b)
  • Fst, Snd - projections

Let Bindings

  • Let - let x = v : A in body

Identity Types (Martin-Löf)

  • Id - propositional equality Id A x y
  • Refl - reflexivity proof refl A x : Id A x x
  • J - path induction eliminator

Cubical Extensions

Cubical type theory extensions are defined in term_cubical.go:

De Bruijn Indices

Variables use de Bruijn indices where 0 refers to the innermost binder. For example, in λx.λy.x, the variable x has index 1 (skipping y at 0). Binder names are preserved only for pretty-printing; the kernel operates solely on indices.

Helper Functions

  • Sprint - pretty-prints a term to a string
  • MkApps - builds left-associative application chains
  • Sort.IsZeroLevel - checks if a sort is Type₀

Raw Terms

The raw.go file defines surface syntax terms (RVar, RPi, etc.) that use named variables. These are elaborated to core terms during parsing.

Package ast provides the abstract syntax tree for the HoTT kernel. This file contains cubical type theory extensions.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func Sprint 

func Sprint(t Term) string

Sprint returns a compact S-expression-like string for debugging.

Types

type App 

type App struct {
	T Term
	U Term
}

App t u (application).

type Boundary added in v1.7.0 

type Boundary struct {
	AtZero Term // Value when interval variable = i0
	AtOne  Term // Value when interval variable = i1
}

Boundary specifies what a path constructor reduces to at interval endpoints. For a path constructor like `loop : Path S1 base base`: 

AtZero = base (value at i=0)
AtOne  = base (value at i=1)

type Comp added in v1.6.0 

type Comp struct {
	IBinder string // Interval binder name (for printing)
	A       Term   // Type line: I → Type (binds interval variable)
	Phi     Face   // Face constraint
	Tube    Term   // Partial tube: defined when φ holds (binds interval variable)
	Base    Term   // Base element: a₀ : A[i0/i]
}

Comp represents heterogeneous composition: comp^i A [φ ↦ u] a₀. This is the fundamental operation for transport in cubical type theory.

Typing rule: 

Γ, i:I ⊢ A : Type    Γ, i:I, φ ⊢ u : A    Γ ⊢ a₀ : A[i0/i]    Γ, φ[i0/i] ⊢ u[i0/i] = a₀ : A[i0/i]
──────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ comp^i A [φ ↦ u] a₀ : A[i1/i]

Computation rules: 

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

type Constructor added in v1.7.0 

type Constructor struct {
	Name string
	Type Term
}

Constructor represents a point constructor in an inductive type. This mirrors the existing Constructor in env.go but is included here for completeness in HIT specifications.

type Face added in v1.6.0 

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

Face represents a face formula (cofibration). Face formulas are boolean expressions over interval endpoints. They are used to specify where partial elements are defined.

type FaceAnd added in v1.6.0 

type FaceAnd struct {
	Left  Face
	Right Face
}

FaceAnd represents conjunction of faces: φ ∧ ψ. Satisfied when both φ and ψ are satisfied.

type FaceBot added in v1.6.0 

type FaceBot struct{}

FaceBot represents the always-false face formula (⊥ or 0). An element defined on FaceBot is defined nowhere (empty partial element).

type FaceEq added in v1.6.0 

type FaceEq struct {
	IVar  int  // Interval variable index (de Bruijn)
	IsOne bool // true for (i = 1), false for (i = 0)
}

FaceEq represents an endpoint constraint: (i = 0) or (i = 1). This is satisfied when the interval variable equals the specified endpoint.

type FaceOr added in v1.6.0 

type FaceOr struct {
	Left  Face
	Right Face
}

FaceOr represents disjunction of faces: φ ∨ ψ. Satisfied when either φ or ψ (or both) are satisfied.

type FaceTop added in v1.6.0 

type FaceTop struct{}

FaceTop represents the always-true face formula (⊤ or 1). An element defined on FaceTop is defined everywhere.

type Fill added in v1.6.0 

type Fill struct {
	IBinder string // Interval binder name (for printing)
	A       Term   // Type line: I → Type (binds interval variable)
	Phi     Face   // Face constraint
	Tube    Term   // Partial tube (binds interval variable)
	Base    Term   // Base element
}

Fill represents the filler for composition: fill^i A [φ ↦ u] a₀. This produces a path from a₀ to comp^i A [φ ↦ u] a₀.

Typing rule: 

Γ, i:I ⊢ A : Type    Γ, i:I, φ ⊢ u : A    Γ ⊢ a₀ : A[i0/i]
──────────────────────────────────────────────────────────
Γ, j:I ⊢ fill^i A [φ ↦ u] a₀ @ j : A[j/i]

The fill operation is defined as: 

fill^i A [φ ↦ u] a₀ = λj. comp^i A[j∧i/i] [φ ∨ (j=0) ↦ ...] a₀

Endpoints: 

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

type Fst 

type Fst struct{ P Term }

Fst and Snd projections.

type Global 

type Global struct{ Name string }

Global refers to a globally named constant (post-elaboration).

type Globals 

type Globals interface {
	// Has reports whether a global name exists.
	Has(name string) bool
}

type Glue added in v1.6.0 

type Glue struct {
	A      Term         // Base type
	System []GlueBranch // System of equivalences
}

Glue represents the Glue type: Glue A [φ ↦ (T, e)]. This is used to construct paths between types via equivalences.

Formation rule: 

Γ ⊢ A : Type    Γ, φ ⊢ T : Type    Γ, φ ⊢ e : Equiv T A
────────────────────────────────────────────────────────
Γ ⊢ Glue A [φ ↦ (T, e)] : Type

Computation rules: 

Glue A [1 ↦ (T, e)] = T              (face satisfied)
Glue A [0 ↦ (T, e)] = A              (face empty)

type GlueBranch added in v1.6.0 

type GlueBranch struct {
	Phi   Face // Face constraint
	T     Term // Fiber type (when φ holds)
	Equiv Term // Equivalence: Equiv T A (when φ holds)
}

GlueBranch represents a branch in a Glue type: φ ↦ (T, e).

type GlueElem added in v1.6.0 

type GlueElem struct {
	System []GlueElemBranch // Partial element in fiber
	Base   Term             // Base element: a : A
}

GlueElem represents a Glue element constructor: glue [φ ↦ t] a. Creates an element of a Glue type.

Typing rule: 

Γ ⊢ a : A    Γ, φ ⊢ t : T    Γ, φ ⊢ e.fst t = a : A
────────────────────────────────────────────────────
Γ ⊢ glue [φ ↦ t] a : Glue A [φ ↦ (T, e)]

Computation rules: 

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

type GlueElemBranch added in v1.6.0 

type GlueElemBranch struct {
	Phi  Face // Face constraint
	Term Term // Element in T (when φ holds)
}

GlueElemBranch represents a branch in a GlueElem: φ ↦ t.

type HComp added in v1.6.0 

type HComp struct {
	A    Term // Type (constant, no interval dependency)
	Phi  Face // Face constraint
	Tube Term // Partial tube (binds interval variable)
	Base Term // Base element
}

HComp represents homogeneous composition: hcomp A [φ ↦ u] a₀. This is composition where the type A is constant (doesn't depend on i).

Typing rule: 

Γ ⊢ A : Type    Γ, i:I, φ ⊢ u : A    Γ ⊢ a₀ : A    Γ, φ[i0/i] ⊢ u[i0/i] = a₀ : A
─────────────────────────────────────────────────────────────────────────────────
Γ ⊢ hcomp A [φ ↦ u] a₀ : A

Computation rules: 

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

type HITApp added in v1.7.0 

type HITApp struct {
	HITName string // HIT type name (e.g., "S1")
	Ctor    string // Path constructor name (e.g., "loop")
	Args    []Term // Type/term parameters applied to constructor
	IArgs   []Term // Interval arguments (I0, I1, or IVar)
}

HITApp represents application of a HIT path constructor to interval arguments. When applied to interval endpoints (i0 or i1), it computes to boundary values: 

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

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

type HITSpec added in v1.7.0 

type HITSpec struct {
	Name       string            // Type name (e.g., "S1", "Trunc")
	Type       Term              // Full type signature including parameters
	NumParams  int               // Number of type parameters
	ParamTypes []Term            // Types of parameters
	PointCtors []Constructor     // Point constructors (level 0)
	PathCtors  []PathConstructor // Path constructors (level >= 1)
	Eliminator string            // Eliminator name (e.g., "S1-elim")
}

HITSpec represents a Higher Inductive Type specification. Used for declaring and validating HITs.

func (*HITSpec) IsHIT added in v1.7.0 

func (s *HITSpec) IsHIT() bool

IsHIT returns true if the specification has path constructors.

func (*HITSpec) MaxLevel added in v1.7.0 

func (s *HITSpec) MaxLevel() int

MaxLevel returns the maximum constructor level in the HIT. Returns 0 for ordinary inductive types, 1 for 1-HITs, 2 for 2-HITs, etc.

type I0 added in v1.6.0 

type I0 struct{}

I0 represents the left endpoint of the interval (0 : I).

type I1 added in v1.6.0 

type I1 struct{}

I1 represents the right endpoint of the interval (1 : I).

type IVar added in v1.6.0 

type IVar struct {
	Ix int // de Bruijn index in the interval variable namespace
}

IVar is an interval variable with its own de Bruijn index space. Interval variables are bound by PathLam and PathP type families.

type Id added in v1.5.8 

type Id struct {
	A Term // Type
	X Term // Left endpoint
	Y Term // Right endpoint
}

Id represents the identity type: Id A x y "x and y are propositionally equal in type A"

type Interval added in v1.6.0 

type Interval struct{}

Interval represents the abstract interval type I. The interval is NOT a proper type in the universe hierarchy; it is used only for path abstraction and application.

type J added in v1.5.8 

type J struct {
	A Term // Type
	C Term // Motive: (y : A) -> Id A x y -> Type
	D Term // Base case: C x (refl A x)
	X Term // Left endpoint
	Y Term // Right endpoint
	P Term // Proof: Id A x y
}

J is the identity eliminator (path induction). J A C d x y p : C y p where: 

A : Type
C : (y : A) -> Id A x y -> Type   (motive)
D : C x (refl A x)                (base case)
X : A                             (left endpoint)
Y : A                             (right endpoint)
P : Id A x y                      (proof of equality)

type Lam 

type Lam struct {
	Binder string
	Ann    Term // may be nil
	Body   Term
}

Lam (λ) abstraction with optional type annotation on the binder for printing.

type Let 

type Let struct {
	Binder string
	Ann    Term // may be nil
	Val    Term
	Body   Term
}

Let x = v : A in body. (Convenience; kernel may desugar away later.)

type Level 

type Level uint

Level represents a universe level (Type^u).

type Pair 

type Pair struct {
	Fst Term
	Snd Term
}

Pair (a , b)

type Partial added in v1.6.0 

type Partial struct {
	Phi Face // The face constraint
	A   Term // The type (may reference interval variables)
}

Partial represents the type of partial elements: Partial φ A. A partial element of type A is defined only when face φ is satisfied.

Formation rule: 

Γ ⊢ φ : Face    Γ, φ ⊢ A : Type
───────────────────────────────
Γ ⊢ Partial φ A : Type

type Path added in v1.6.0 

type Path struct {
	A Term // Type (constant over interval)
	X Term // Left endpoint: x : A
	Y Term // Right endpoint: y : A
}

Path represents the non-dependent path type: Path A x y. This is definitionally equal to PathP (λi. A) x y where A is constant.

Formation rule: 

Γ ⊢ A : Type_i    Γ ⊢ x : A    Γ ⊢ y : A
─────────────────────────────────────────
Γ ⊢ Path A x y : Type_i

type PathApp added in v1.6.0 

type PathApp struct {
	P Term // Path: PathP A x y or Path A x y
	R Term // Interval argument: I0, I1, or IVar
}

PathApp represents path application: p @ r. Applies a path to an interval term (i0, i1, or interval variable).

Elimination rule: 

Γ ⊢ p : PathP A x y    Γ ⊢ r : I
────────────────────────────────
Γ ⊢ p @ r : A[r/i]

Computation rules: 

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

type PathConstructor added in v1.7.0 

type PathConstructor struct {
	Name       string     // Constructor name (e.g., "loop")
	Level      int        // Dimension: 1=path, 2=path-of-path, etc.
	Type       Term       // Full type (e.g., Path S1 base base)
	Boundaries []Boundary // One Boundary per interval dimension
}

PathConstructor represents a path-level constructor in a HIT.

Level indicates the dimension of the path:

  • Level 1: path between points (binds 1 interval variable)
  • Level 2: path between paths (binds 2 interval variables)
  • etc.

Example for Circle: 

PathConstructor{
    Name: "loop",
    Level: 1,
    Type: Path S1 base base,
    Boundaries: []Boundary{{AtZero: base, AtOne: base}},
}

type PathLam added in v1.6.0 

type PathLam struct {
	Binder string // Interval variable name (for printing only)
	Body   Term   // Body with interval variable bound at index 0
}

PathLam represents path abstraction: <i> t. Creates a path by abstracting over an interval variable.

Introduction rule: 

Γ, i:I ⊢ t : A
───────────────────────────────────────────
Γ ⊢ <i> t : PathP (λi. A) t[i0/i] t[i1/i]

type PathP added in v1.6.0 

type PathP struct {
	A Term // Type family: I → Type (binds an interval variable)
	X Term // Left endpoint: x : A[i0/i]
	Y Term // Right endpoint: y : A[i1/i]
}

PathP represents the dependent path type: PathP A x y. Here A is a type family over the interval: A : I → Type.

Formation rule: 

Γ, i:I ⊢ A : Type_j    Γ ⊢ x : A[i0/i]    Γ ⊢ y : A[i1/i]
──────────────────────────────────────────────────────────
Γ ⊢ PathP (λi. A) x y : Type_j

type Pi 

type Pi struct {
	Binder string
	A      Term
	B      Term
}

Pi (Π) type with domain A and codomain B in a binder (x:A).B. We keep the binder name only for pretty-printing; kernel uses de Bruijn.

type RApp 

type RApp struct{ T, U RTerm }

type RFst 

type RFst struct{ P RTerm }

type RGlobal 

type RGlobal struct{ Name string } // global symbol

type RId added in v1.7.0 

type RId struct {
	A RTerm // Type
	X RTerm // Left endpoint
	Y RTerm // Right endpoint
}

RId is the raw identity type: Id A x y

type RJ added in v1.7.0 

type RJ struct {
	A RTerm // Type
	C RTerm // Motive
	D RTerm // Base case
	X RTerm // Left endpoint
	Y RTerm // Right endpoint
	P RTerm // Proof
}

RJ is the raw identity eliminator (path induction): J A C d x y p

type RLam 

type RLam struct {
	Binder string
	Ann    RTerm
	Body   RTerm

} // Ann may be nil

type RLet 

type RLet struct {
	Binder         string
	Ann, Val, Body RTerm

} // Ann may be nil

type RPair 

type RPair struct{ Fst, Snd RTerm }

type RPi 

type RPi struct {
	Binder string
	A, B   RTerm
}

type RRefl added in v1.7.0 

type RRefl struct {
	A RTerm // Type
	X RTerm // The term being proven equal to itself
}

RRefl is the raw reflexivity constructor: refl A x

type RSigma 

type RSigma struct {
	Binder string
	A, B   RTerm
}

type RSnd 

type RSnd struct{ P RTerm }

type RSort 

type RSort struct{ U Level } // Type^U

type RTerm 

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

Raw terms carry user-chosen names before resolution.

type RVar 

type RVar struct{ Name string } // free or bound

type Refl added in v1.5.8 

type Refl struct {
	A Term // Type
	X Term // The term being proven equal to itself
}

Refl is the reflexivity constructor: refl A x : Id A x x

type Sigma 

type Sigma struct {
	Binder string
	A      Term
	B      Term
}

Sigma (Σ) type.

type Snd 

type Snd struct{ P Term }

type Sort 

type Sort struct{ U Level }

Sort is a universe: Type^U.

func (Sort) IsZeroLevel 

func (s Sort) IsZeroLevel() bool

IsZeroLevel returns true if this is Sort 0 (Type0).

type System added in v1.6.0 

type System struct {
	Branches []SystemBranch
}

System represents a system of partial elements: [ φ₁ ↦ t₁, φ₂ ↦ t₂, ... ]. Each branch provides an element when its face is satisfied. Branches must agree on overlaps.

Typing rule: 

Γ, φᵢ ⊢ tᵢ : A    (∀i,j: φᵢ ∧ φⱼ ⊢ tᵢ = tⱼ)
────────────────────────────────────────────
Γ ⊢ [φ₁ ↦ t₁, ...] : Partial (φ₁ ∨ ...) A

type SystemBranch added in v1.6.0 

type SystemBranch struct {
	Phi  Face // When this face is satisfied...
	Term Term // ...this term is the value
}

SystemBranch represents a single branch in a system: φ ↦ t.

type Term 

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

Term is the interface for all core terms.

func MkApps 

func MkApps(t Term, us ...Term) Term

MkApps applies t to us left-associatively.

func Resolve 

func Resolve(globals Globals, sc scope, r RTerm) (Term, error)

Resolve converts an RTerm to a core Term with respect to a scope and globals.

type Transport added in v1.6.0 

type Transport struct {
	A Term // Type family: I → Type (binds an interval variable)
	E Term // Element at i0: e : A[i0/i]
}

Transport represents cubical transport: transport A e. Transports an element along a type family over the interval.

Typing rule: 

Γ, i:I ⊢ A : Type_j    Γ ⊢ e : A[i0/i]
──────────────────────────────────────
Γ ⊢ transport (λi. A) e : A[i1/i]

Computation rule: 

transport (λi. A) e  ⟶  e    (when A is constant in i)

type UA added in v1.6.0 

type UA struct {
	A     Term // Source type
	B     Term // Target type
	Equiv Term // Equivalence: Equiv A B
}

UA represents the univalence axiom: ua e : Path Type A B. Given an equivalence e : Equiv A B, ua produces a path between types.

Typing rule: 

Γ ⊢ A : Type_i    Γ ⊢ B : Type_i    Γ ⊢ e : Equiv A B
─────────────────────────────────────────────────────
Γ ⊢ ua e : Path Type_i 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

Key computation (transport computes!): 

transport (ua e) a = e.fst a

type UABeta added in v1.6.0 

type UABeta struct {
	Equiv Term // The equivalence e : Equiv A B
	Arg   Term // The argument a : A
}

UABeta represents the computation rule for transport along ua. This is used when we need to explicitly mark that transport (ua e) a = e.fst a. 

transport (ua e) a  ⟶  e.fst a

type Unglue added in v1.6.0 

type Unglue struct {
	Ty Term // The Glue type (needed for computation)
	G  Term // The Glue element
}

Unglue extracts the base from a Glue element: unglue g.

Typing rule: 

Γ ⊢ g : Glue A [φ ↦ (T, e)]
───────────────────────────
Γ ⊢ unglue g : A

Computation rules: 

unglue (glue [φ ↦ t] a) = a          (definitional)
unglue g = e.fst g                   (when φ holds)

type Var 

type Var struct{ Ix int }

Var is a de Bruijn variable: index (0 = innermost binder).

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.