Abstract
Per is a theorem prover that constitutes a MLTT-80 core for a dependently-typed lambda calculus. It is specifically constrained to exclude pattern matching, let-bindings, and implicit arguments to focus on the pure structural properties of the type-theoretic core. It incorporates twin hierarchies of universes, U and V, following the HTS distinction: U for Kan-fibrant types supporting composition, and V for pretypes, including the geometric interval I. The system supports dependent products Pi, dependent pairs Sigma, identity types Id, and inductive types 0, 1, 2, W for well-founded definitions.
Unlike full CCHM systems with complex Higher Inductive Types (HITs),
Per remains a minimal cubical core with Glue, Partial, and Subtype primitives
supporting hcomp and transp operations. It prioritizes the structural integrity of
canonicity and normalization — essential invariants for an internalized type theory.
Constructive Natural Numbers
Comparison of constructive natural numbers: structural vs. homotopical representations.
Strict Canonicity
canonical.per — Natural numbers as a direct W-type. Every closed term of type Nat normalizes to a constructor form, perfectly satisfying the canonicity property.
def A : U := 𝟐 def B (b : 𝟐) : U₀ := ind₂ (λ (_ : 𝟐), U₀) 𝟎 𝟏 b def Nat : U₀ := W (b : A), B b def zero : Nat := sup A B 0₂ (λ (e : 𝟎), ind₀ Nat e) def succ (n : Nat) : Nat := sup A B 1₂ (λ (u : 𝟏), n)
Standard constructive semantics with strict reduction paths.
Homotopy Canonicity
homotopical.per — Homotopy-inductive representation. Extends canonicity to path-induction, ensuring that terms involving transp and PathP maintain computational behavior through normalization to values.
def ℕ := W (x : 𝟐), ℕ-ctor x
def zero : ℕ := sup 𝟐 ℕ-ctor 0₂ (ind₀ ℕ)
def 𝟎⟶ℕ (C : ℕ → U) (f : 𝟎 → ℕ) : C zero → C (sup 𝟐 ℕ-ctor 0₂ f)
:= transp (<i> C (sup 𝟐 ℕ-ctor 0₂ (λ (x : 𝟎), ind₀ (PathP (<_> ℕ)
(ind₀ ℕ x) (f x)) x @ i))) 0
Demonstrates the computational integrity of cubical foundations where paths are first-class residents.
Self Awareness
Internalization
Per is designed to be self-hosting in its logic. The core constructs are represented within the language itself, allowing for proofs about the typechecker's own behaviors and properties.
def Internalizing : MLTT-73
:= ( Pi, Π-lambda, Π-apply, Π-β, Π-η,
Sigma, pair, pr₁, pr₂, Σ-β₁, Σ-β₂, Σ-η,
Path-1, idp-1, J-1, J-β, ★ )
Groupoid Interpretation
This Hofmann–Streicher groupoid model remains the classical starting point for understanding how type theory can carry intrinsic homotopical or higher-categorical content, even without explicit homotopy axioms.
def CatGroupoid (X : U) (G : isGroupoid X)
: isCatGroupoid (PathCat X)
:= ( idp X,
comp-Path X,
G,
sym X,
comp-inv-Path⁻¹ X,
comp-inv-Path X,
comp-Path-left X,
comp-Path-right X,
comp-Path-assoc X,
star
)
MLTT and CCHM Foundations
Fibrational Systems
Pi-type is a space that contains dependent functions, which codomain type depends on value from domain type. As fiber domain present in every defined function, Pi-type is also a dependent product. Spaces of dependent functions are using in type theory to model various mathematical constructions, objects, types, or spaces and their maps: dependent functions, continuous maps, étale maps, fibre bundles, universal quantifier П-type, implications, etc.
def Pi (A : U) (B : A → U) : U := Π (x : A), B x def Π-lambda (A : U) (B : A → U) (b : Pi A B) : Pi A B := λ (x : A), b x def Π-apply (A: U) (B: A → U) (f: Pi A B) (a: A) : B a := f a def Π-β (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (B a) (Π-apply A B (Π-lambda A B f) a) (f a) := idp (B a) (f a) def Π-η (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (Pi A B) f (λ (x : A), f x) := idp (Pi A B) f
Sigma-type is a space that contains dependent pairs where type of the second element depends on the value of the first element. As only one point of fiber domain present in every defined pair, Sigma-type is also a dependent sum, where fiber base is a disjoint union.
def Sigma (A : U) (B : A → U) : U := summa (x: A), B x def pair (A: U) (B: A → U) (a: A) (b: B a) : Sigma A B := (a, b) def pr₁ (A: U) (B: A → U) (x: Sigma A B) : A := x.1 def pr₂ (A: U) (B: A → U) (x: Sigma A B) : B (pr₁ A B x) := x.2 def Σ-β₁ (A : U) (B : A → U) (a : A) (b : B a) : Path A a (pr₁ A B (a ,b)) := idp A a def Σ-β₂ (A : U) (B : A → U) (a : A) (b : B a) : Path (B a) b (pr₂ A B (a, b)) := idp (B a) b def Σ-η (A : U) (B : A → U) (p : Sigma A B) : Path (Sigma A B) p (pr₁ A B p, pr₂ A B p) := idp (Sigma A B) p
Identity Systems
Identity is realized via PathP, derived from the geometric interval I.
Per's foundations ensure the structural derivation of the J-induction principle
from Kan-composition operations, forming a robust basis for univalent formalization.
def singl (A: U) (a: A): U := Σ (x: A), Path A a x def eta (A: U) (a: A): singl A a := (a, idp A a) def sym (A: U) (a b : A) (p : Path A a b) : Path A b a := <i> p @ -i def contr (A : U) (a b : A) (p : Path A a b) : Path (singl A a) (eta A a) (b, p) := <i> (p @ i, <j> p @ i /\ j) def transport (A B: U) (p : PathP (<_> U) A B) (a: A): B := transp p 0 a def singl (A: U) (a: A): U := Σ (x: A), Path A a x def eta (A: U) (a: A): singl A a := (a, idp A a) def contr (A : U) (a b : A) (p : Path A a b) : Path (singl A a) (eta A a) (b, p) := <i> (p @ i, <j> p @ i /\ j) def trans_comp (A : U) (a : A) : Path A a (transport A A (<i> A) a) := <j> transp (<_> A) -j a def subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b := transp (<i> P (p @ i)) 0 e def subst-comp (A: U) (P: A → U) (a: A) (e: P a): Path (P a) e (subst A P a a (idp A a) e) := trans_comp (P a) e def D (A : U) : U₁ := Π (x y : A), Path A x y → U def J (A: U) (x: A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path A x y): C x y p := subst (singl A x) (\ (z: singl A x), C x (z.1) (z.2)) (eta A x) (y, p) (contr A x y p) d def J-1 (A : U) (x : A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path A x y): C x y p := subst (singl A x) (\ (z: singl A x), C x (z.1) (z.2)) (eta A x) (y, p) (contr A x y p) d def J-β (A : U) (a : A) (C : D A) (d: C a a (idp A a)) : Path (C a a (idp A a)) d (J A a C d a (idp A a)) := subst-comp (singl A a) (\ (z: singl A a), C a (z.1) (z.2)) (eta A a) d
def ∂ (i : I) := i ∨ -i def ∂-eq-neg-∂ (i : I) : Id I (∂ i) (∂ -i) := ref (∂ i) def min (i j : I) := i ∧ j def max (i j : I) := i ∨ j def ⊕ (i j : I) : I := (i ∧ -j) ∨ (-i ∧ j) def ⊕-comm (i j : I) : Id I (⊕ i j) (⊕ j i) := ref (⊕ i j) def ∧-comm (i j : I) : Id I (i ∧ j) (j ∧ i) := ref (i ∧ j) def ∨-comm (i j : I) : Id I (i ∨ j) (j ∨ i) := ref (i ∨ j) def ¬-of-∧ (i j : I) : Id I -(i ∧ j) (-i ∨ -j) := ref -(i ∧ j) def ¬-of-∨ (i j : I) : Id I -(i ∨ j) (-i ∧ -j) := ref -(i ∨ j) def ∧-distrib-∨ (i j k : I) : Id I ((i ∨ j) ∧ k) ((i ∧ k) ∨ (j ∧ k)) := ref ((i ∨ j) ∧ k) def ∨-distrib-∧ (i j k : I) : Id I ((i ∧ j) ∨ k) ((i ∨ k) ∧ (j ∨ k)) := ref ((i ∧ j) ∨ k) def ∧-assoc (i j k : I) : Id I (i ∧ (j ∧ k)) ((i ∧ j) ∧ k) := ref (i ∧ (j ∧ k))
Homotopy Type Theory
univalent.per — Implementation of the core of Homotopy Type Theory, providing path spaces, identity systems, and the J-induction principle within the semi-cubical framework.
def idp (A : U) (x : A) : Path A x x := <_> x def isContr (A: U) : U := Σ (x: A), Π (y: A), Path A x y def isContrSingl (A : U) (a : A) : isContr (singl A a) := ((a,idp A a),(\ (z:singl A a), contr A a z.1 z.2)) def cong (A B : U) (f : A → B) (a b : A) (p : Path A a b) : Path B (f a) (f b) := <i> f (p @ i) def ap (A: U) (a x: A) (B: A → U) (f: A → B a) (b: B a) (p: Path A a x) : Path (B a) (f a) (f x) := <i> f (p @ i) def inv (A: U) (a b: A) (p: Path A a b): Path A b a := <i> p @ -i def Path-η (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (<i> p @ i) := <_> p def idp-left (A : U) (x y : A) (p : Path A x y) : Path (Path A x x) (<_> x) (<_> p @ 0) := <_ _> x def idp-right (A : U) (x y : A) (p : Path A x y) : Path (Path A y y) (<_> y) (<_> p @ 1) := <_ _> y def sym-sym-eq-idp (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (sym A y x (sym A x y p)) := <_> p def isProp (A : U) : U := Π (a b : A), Path A a b def isSet (A : U) : U := Π (a b : A) (a0 b0 : Path A a b), Path (Path A a b) a0 b0 def isGroupoid (A : U) : U := Π (a b : A) (x y : Path A a b) (i j : Path (Path A a b) x y), Path (Path (Path A a b) x y) i j def SET : U₁ := Σ (X : U), isSet X def Ω' : U₁ := Σ (A : U), isProp A def section (A B : U) (f : A -> B) (g : B -> A) : U := Π (b : B), Path B (f (g b)) b def retract (A B : U) (f : A -> B) (g : B -> A) : U := Π (a : A), Path A (g (f a)) a def hmtpy (A : U) (x y : A) (p : Path A x y) : Path (Path A x x) (<_> x) (<i> p @ i /\ -i) := <j i> p @ j /\ i /\ -i def plam (A : U) (f : I → A) : Path A (f 0) (f 1) := <i> f i def elim (A : U) (a b : A) (p : Path A a b) : I → A := λ (i : I), p @ i def plam-elim (A : U) (f : I → A) : Id (I → A) (elim A (f 0) (f 1) (plam A f)) f := ref f def elim-plam (A : U) (a b : A) (p : Path A a b) : Path (Path A a b) (plam A (elim A a b p)) p := <_> p
Decidability of Interval Boundaries
The structural consistency of the CCHM model over the face lattice requires a robust decidability mechanism for boundary conditions. Per implements a DNF (Disjunctive Normal Form) solver to ensure the coherence of Kan-composition across multi-dimensional faces, guaranteeing that judgmental equality remains stable in the presence of complex boundary constraints.
Accessing Higher Dimensions
constcubes.per — An extensive test suite defining higher-dimensional structures. From Squares and Cubes to 4D Tesseracts, these definitions verify the structural stability of normalization and face composition, ensuring the core remains sound as geometric complexity scales.
def Line (A : I → U) : V := Π (i : I), A i
def Square (A : U) (a₀ a₁ b₀ b₁ : A) (u : Path A a₀ a₁) (v : Path A b₀ b₁) (r₀ : Path A a₀ b₀) (r₁ : Path A a₁ b₁)
: U := PathP (<i> (Path A (r₀ @ i) (r₁ @ i))) u v
def Cube (A : U) (a₀ b₀ c₀ d₀ a₁ b₁ c₁ d₁ : A)
(ab₀ : Path A a₀ b₀) (cd₀ : Path A c₀ d₀) (ac₀ : Path A a₀ c₀) (bd₀ : Path A b₀ d₀)
(ab₁ : Path A a₁ b₁) (cd₁ : Path A c₁ d₁) (ac₁ : Path A a₁ c₁) (bd₁ : Path A b₁ d₁)
(s₀ : Square A a₀ b₀ c₀ d₀ ab₀ cd₀ ac₀ bd₀) (s₁ : Square A a₁ b₁ c₁ d₁ ab₁ cd₁ ac₁ bd₁)
(pa : Path A a₀ a₁) (pb : Path A b₀ b₁) (pc : Path A c₀ c₁) (pd : Path A d₀ d₁)
(sab : Square A a₀ b₀ a₁ b₁ ab₀ ab₁ pa pb) (scd : Square A c₀ d₀ c₁ d₁ cd₀ cd₁ pc pd)
(sac : Square A a₀ c₀ a₁ c₁ ac₀ ac₁ pa pc) (sbd : Square A b₀ d₀ b₁ d₁ bd₀ bd₁ pb pd) : U
:= PathP (<i> (Square A (pa @ i) (pb @ i) (pc @ i) (pd @ i) (sab @ i) (scd @ i) (sac @ i) (sbd @ i))) s₀ s₁
def Tesseract (A : U) (a₀ b₀ c₀ d₀ a₁ b₁ c₁ d₁ a₂ b₂ c₂ d₂ a₃ b₃ c₃ d₃ : A)
(ab₀ : Path A a₀ b₀) (cd₀ : Path A c₀ d₀) (ac₀ : Path A a₀ c₀) (bd₀ : Path A b₀ d₀)
(ab₁ : Path A a₁ b₁) (cd₁ : Path A c₁ d₁) (ac₁ : Path A a₁ c₁) (bd₁ : Path A b₁ d₁)
(s₀ : Square A a₀ b₀ c₀ d₀ ab₀ cd₀ ac₀ bd₀) (s₁ : Square A a₁ b₁ c₁ d₁ ab₁ cd₁ ac₁ bd₁)
(a₀₁ : Path A a₀ a₁) (b₀₁ : Path A b₀ b₁) (c₀₁ : Path A c₀ c₁) (d₀₁ : Path A d₀ d₁)
(sab₀₁ : Square A a₀ b₀ a₁ b₁ ab₀ ab₁ a₀₁ b₀₁) (scd₀₁ : Square A c₀ d₀ c₁ d₁ cd₀ cd₁ c₀₁ d₀₁)
(sac₀₁ : Square A a₀ c₀ a₁ c₁ ac₀ ac₁ a₀₁ c₀₁) (sbd₀₁ : Square A b₀ d₀ b₁ d₁ bd₀ bd₁ b₀₁ d₀₁)
(cu₀₁ : Cube A a₀ b₀ c₀ d₀ a₁ b₁ c₁ d₁ ab₀ cd₀ ac₀ bd₀ ab₁ cd₁ ac₁ bd₁ s₀ s₁ a₀₁ b₀₁ c₀₁ d₀₁ sab₀₁ scd₀₁ sac₀₁ sbd₀₁)
(ab₂ : Path A a₂ b₂) (cd₂ : Path A c₂ d₂) (ac₂ : Path A a₂ c₂) (bd₂ : Path A b₂ d₂)
(ab₃ : Path A a₃ b₃) (cd₃ : Path A c₃ d₃) (ac₃ : Path A a₃ c₃) (bd₃ : Path A b₃ d₃)
(s₂ : Square A a₂ b₂ c₂ d₂ ab₂ cd₂ ac₂ bd₂) (s₃ : Square A a₃ b₃ c₃ d₃ ab₃ cd₃ ac₃ bd₃)
(a₂₃ : Path A a₂ a₃) (b₂₃ : Path A b₂ b₃) (c₂₃ : Path A c₂ c₃) (d₂₃ : Path A d₂ d₃)
(sab₂₃ : Square A a₂ b₂ a₃ b₃ ab₂ ab₃ a₂₃ b₂₃) (scd₂₃ : Square A c₂ d₂ c₃ d₃ cd₂ cd₃ c₂₃ d₂₃)
(sac₂₃ : Square A a₂ c₂ a₃ c₃ ac₂ ac₃ a₂₃ c₂₃) (sbd₂₃ : Square A b₂ d₂ b₃ d₃ bd₂ bd₃ b₂₃ d₂₃)
(cu₂₃ : Cube A a₂ b₂ c₂ d₂ a₃ b₃ c₃ d₃ ab₂ cd₂ ac₂ bd₂ ab₃ cd₃ ac₃ bd₃ s₂ s₃ a₂₃ b₂₃ c₂₃ d₂₃ sab₂₃ scd₂₃ sac₂₃ sbd₂₃)
(a₀₂ : Path A a₀ a₂) (b₀₂ : Path A b₀ b₂) (c₀₂ : Path A c₀ c₂) (d₀₂ : Path A d₀ d₂)
(a₁₃ : Path A a₁ a₃) (b₁₃ : Path A b₁ b₃) (c₁₃ : Path A c₁ c₃) (d₁₃ : Path A d₁ d₃)
(sab₀₂ : Square A a₀ b₀ a₂ b₂ ab₀ ab₂ a₀₂ b₀₂) (scd₀₂ : Square A c₀ d₀ c₂ d₂ cd₀ cd₂ c₀₂ d₀₂)
(sac₀₂ : Square A a₀ c₀ a₂ c₂ ac₀ ac₂ a₀₂ c₀₂) (sbd₀₂ : Square A b₀ d₀ b₂ d₂ bd₀ bd₂ b₀₂ d₀₂)
(sab₁₃ : Square A a₁ b₁ a₃ b₃ ab₁ ab₃ a₁₃ b₁₃) (scd₁₃ : Square A c₁ d₁ c₃ d₃ cd₁ cd₃ c₁₃ d₁₃)
(sac₁₃ : Square A a₁ c₁ a₃ c₃ ac₁ ac₃ a₁₃ c₁₃) (sbd₁₃ : Square A b₁ d₁ b₃ d₃ bd₁ bd₃ b₁₃ d₁₃)
(sa : Square A a₀ a₁ a₂ a₃ a₀₁ a₂₃ a₀₂ a₁₃) (sb : Square A b₀ b₁ b₂ b₃ b₀₁ b₂₃ b₀₂ b₁₃)
(sc : Square A c₀ c₁ c₂ c₃ c₀₁ c₂₃ c₀₂ c₁₃) (sd : Square A d₀ d₁ d₂ d₃ d₀₁ d₂₃ d₀₂ d₁₃)
(cu₀₂ : Cube A a₀ b₀ c₀ d₀ a₂ b₂ c₂ d₂ ab₀ cd₀ ac₀ bd₀ ab₂ cd₂ ac₂ bd₂ s₀ s₂ a₀₂ b₀₂ c₀₂ d₀₂ sab₀₂ scd₀₂ sac₀₂ sbd₀₂)
(cu₁₃ : Cube A a₁ b₁ c₁ d₁ a₃ b₃ c₃ d₃ ab₁ cd₁ ac₁ bd₁ ab₃ cd₃ ac₃ bd₃ s₁ s₃ a₁₃ b₁₃ c₁₃ d₁₃ sab₁₃ scd₁₃ sac₁₃ sbd₁₃)
(cuab : Cube A a₀ b₀ a₁ b₁ a₂ b₂ a₃ b₃ ab₀ ab₁ a₀₁ b₀₁ ab₂ ab₃ a₂₃ b₂₃ sab₀₁ sab₂₃ a₀₂ b₀₂ a₁₃ b₁₃ sab₀₂ sab₁₃ sa sb)
(cucd : Cube A c₀ d₀ c₁ d₁ c₂ d₂ c₃ d₃ cd₀ cd₁ c₀₁ d₀₁ cd₂ cd₃ c₂₃ d₂₃ scd₀₁ scd₂₃ c₀₂ d₀₂ c₁₃ d₁₃ scd₀₂ scd₁₃ sc sd)
(cuac : Cube A a₀ c₀ a₁ c₁ a₂ c₂ a₃ c₃ ac₀ ac₁ a₀₁ c₀₁ ac₂ ac₃ a₂₃ c₂₃ sac₀₁ sac₂₃ a₀₂ c₀₂ a₁₃ c₁₃ sac₀₂ sac₁₃ sa sc)
(cubd : Cube A b₀ d₀ b₁ d₁ b₂ d₂ b₃ d₃ bd₀ bd₁ b₀₁ d₀₁ bd₂ bd₃ b₂₃ d₂₃ sbd₀₁ sbd₂₃ b₀₂ d₀₂ b₁₃ d₁₃ sbd₀₂ sbd₁₃ sb sd)
: U := PathP (<i> (Cube A (a₀₂ @ i) (b₀₂ @ i) (c₀₂ @ i) (d₀₂ @ i) (a₁₃ @ i) (b₁₃ @ i) (c₁₃ @ i) (d₁₃ @ i)
(sab₀₂ @ i) (scd₀₂ @ i) (sac₀₂ @ i) (sbd₀₂ @ i) (sab₁₃ @ i) (scd₁₃ @ i) (sac₁₃ @ i) (sbd₁₃ @ i)
(cu₀₂ @ i) (cu₁₃ @ i) (sa @ i) (sb @ i) (sc @ i) (sd @ i)
(cuab @ i) (cucd @ i) (cuac @ i) (cubd @ i))) cu₀₁ cu₂₃
Agda and Lean Syntaxes
Always support more than one syntax.
$ mix per.base --syntax=agda Generated per app Compiling Per base library [agda]... Compiling priv/agda/foundations/mltt.agda... OK Compiling priv/agda/foundations/inductive.agda... OK Compiling priv/agda/foundations/univalent.agda... OK Per base library compilation finished successfully.
$ mix per.repl --syntax=lean 🧊 Per Programming Language version 0.4.00 Copyright (c) 2016-2026 Groupoid Infinity https://groupoid.github.io/per/ Loaded: mltt Loaded: inductive Loaded: univalent per [Lean]> :eval zero TYPE: W(x : 𝟐) (ind₂ \f -> U₀) 𝟎 𝟏 x TERM: (sup 𝟐 (ind₂ \f -> U₀) 𝟎 𝟏) 0₂ ind₀ W(x : 𝟐) (ind₂ \f -> U₀) 𝟎 𝟏 x per [Lean]>
Performance Tracing
Make your stack profileable and tuneable.
$ mix per.test --syntax=lean --trace Running Per tests [lean]... Testing test/per/canonical.per... desugar [ ] 0.000002s (x1) imports [= ] 0.000057s (x1) lexer [= ] 0.000072s (x1) parser [ ] 0.000008s (x1) typecheck [========================================] 0.002943s (x1) OK (canonical) Testing test/per/constcubes.per... desugar [ ] 0.000131s (x1) imports [ ] 0.001360s (x1) lexer [ ] 0.003333s (x1) parser [ ] 0.000444s (x1) typecheck [========================================] 0.718808s (x1) OK (constcubes) Testing test/per/homotopical.per... desugar [ ] 0.000007s (x1) imports [=================================== ] 0.000671s (x1) lexer [========================================] 0.000764s (x1) parser [= ] 0.000020s (x1) typecheck [=========== ] 0.000213s (x1) OK (homotopical) All Per tests passed.
Model Checker in OCaml
Order peer review or replicated proof checker in another (possibly faster) language for double (triple) checking. Order as much implementations as possible, make them follow your syntax sctrictly, issue a spec. Per should be robust and sound in all its syntaxeses and across all its implementations.
% dune exec per check test/per/constcubes.per repl File “constcubes.per” checked. Per theorem prover [MLTT-80] version 5.3.20 >
Open Source
