equality

Documentation

Overview

Package equality is the EQUALITY STRATUM: the notion of equality, kept behind a bounded interface so the roadmap can extend it (v2: quotients) and swap it (v3: two-level type theory) without a rewrite.

The interface the stratum implements is core.EqStratum — the eval hooks the glued-NbE machine calls when it reaches an equality former. Phase 3 binds the signatures and ships the one v1 implementation, Observational (Pujet–Tabareau): a proof-irrelevant Prop, an observational Eq that computes on type structure (funext is a reduction), and cast, which computes on the endpoint types and never inspects its proof. The store, hashing, semiring, codegen, and surface/nameless split are all deliberately ORTHOGONAL to this package.

Index

• type Observational
  • func (o Observational) EvalCast(m *core.Machine, a, b, p, x core.Val) core.Val
  • func (Observational) EvalEq(m *core.Machine, ty, l, r core.Val) core.Val
  • func (Observational) EvalSubst(m *core.Machine, a, x, y, prf, pmot, px core.Val) core.Val
  • func (Observational) Formers() []string
  • func (Observational) Name() string
• type Stratum
  • func Default() Stratum

Types

type Observational

type Observational struct{}

Observational is the v1 equality stratum (Pujet–Tabareau, *Observational Equality: Now For Good*): proof-irrelevant Prop, an Eq that computes on the structure of its type, and cast. UIP holds; univalence is refuted by design (NON-GOALS.md). What v1 computes:

• Eq (Pi (x:A) B) f g ~> (x : A) -> Eq B (f x) (g x) [funext]
• cast A B p x ~> x when A ≡ B definitionally
• cast (Pi a1 b1) (Pi a2 b2) p f ~> fn (y : a2) is cast (b1 (cast a2 a1 _ y)) (b2 y) _ (f (cast a2 a1 _ y)) end
• Eq U/Prop endpoints and proof-typed values are irrelevant: conversion skips cast proofs and equates refl proofs (core/conv.go).

Deeper type-equality DECOMPOSITION (Eq U (Pi …) (Pi …) unfolding to a telescope of equalities) needs Sigma types and is parked until a listing needs it; a stuck Eq U is still provable by refl at convertible endpoints.

func (Observational) EvalCast

func (o Observational) EvalCast(m *core.Machine, a, b, p, x core.Val) core.Val

EvalCast computes cast a b p x, never inspecting p (proof irrelevance): the reduction is driven entirely by the endpoint types.

func (Observational) EvalEq

func (Observational) EvalEq(m *core.Machine, ty, l, r core.Val) core.Val

EvalEq computes Eq ty l r. The load-bearing rule is funext-as-reduction: an equality of functions IS the pointwise equality function type.

func (Observational) EvalSubst

func (Observational) EvalSubst(m *core.Machine, a, x, y, prf, pmot, px core.Val) core.Val

EvalSubst computes Leibniz transport: when the equality's endpoints are definitionally equal the transport is the identity on its subject; otherwise it is stuck. The proof is never inspected.

func (Observational) Formers

func (Observational) Formers() []string

func (Observational) Name

func (Observational) Name() string

type Stratum

type Stratum interface {
	core.EqStratum
	// Name identifies the stratum implementation (e.g. "observational").
	Name() string
	// Formers returns the core type-former names this stratum gives meaning to.
	Formers() []string
}

Stratum is the equality stratum: core.EqStratum plus identification.

func Default

func Default() Stratum

Default is the stratum instance v1 wires into every Machine.