Version: 1.0 Date: December 2025 Authors: Jonathan D.A. Jewell Status: Research Preview
This document presents the type-theoretic and categorical foundations of Eclexia. We develop: (1) a dependent type theory with resource indices; (2) categorical semantics via enriched category theory and graded monads; (3) domain-theoretic denotational semantics; (4) game semantics for interactive resource consumption; (5) realizability semantics connecting computation and proof; and (6) connections to homotopy type theory for higher-dimensional resource structure. This foundational work situates Eclexia within the broader landscape of programming language theory and provides a framework for future extensions.
- Introduction
- Type-Theoretic Foundations
- Dependent Resource Types
- Categorical Semantics
- Enriched Categories and Graded Monads
- Domain-Theoretic Semantics
- Game Semantics
- Realizability Semantics
- Effect Systems and Algebraic Effects
- Session Types for Resources
- Homotopy Type Theory Connections
- Coherence and Canonicity
- Normalization
- Decidability Results
- Extensions and Future Directions
Eclexia's Economics-as-Code paradigm requires a sophisticated type-theoretic foundation that:
- Tracks resources precisely through types
- Ensures dimensional correctness at compile time
- Supports optimization objectives declaratively
- Enables adaptive computation with formal guarantees
- Connects to established mathematical structures
Dependent Types
│
┌────────────┼────────────┐
│ │ │
Martin-Löf Calculus of Cubical
Type Theory Constructions Type Theory
│ │ │
└────────────┼────────────┘
│
┌────┴────┐
│ │
Linear Types Graded Types
│ │
└────┬────┘
│
Quantitative
Type Theory
│
Eclexia's
Resource Types
We assume familiarity with:
- Basic category theory (categories, functors, natural transformations)
- Type theory (λ-calculus, polymorphism, dependent types)
- Domain theory (CPOs, Scott continuity)
- Order theory (lattices, Galois connections)
Eclexia's type theory is based on a predicative, intensional Martin-Löf Type Theory extended with:
- Polymorphism (System F-style)
- Resource types with dimensional indices
- Effect types via graded monads
- Constraint types for optimization
Γ ⊢ Context Γ is well-formed
Γ ⊢ A type A is a type in context Γ
Γ ⊢ A ≡ B type A and B are definitionally equal types
Γ ⊢ a : A a has type A in context Γ
Γ ⊢ a ≡ b : A a and b are definitionally equal at type A
───────────── (Ctx-Empty)
· ⊢
Γ ⊢ Γ ⊢ A type x ∉ dom(Γ)
─────────────────────────────── (Ctx-Ext)
Γ, x:A ⊢
Γ ⊢
───────────── (Ty-Unit)
Γ ⊢ 𝟙 type
Γ ⊢
───────────── (Ty-Bool)
Γ ⊢ 𝔹 type
Γ ⊢
───────────── (Ty-Int)
Γ ⊢ ℤ type
Γ ⊢ A type Γ ⊢ B type
──────────────────────── (Ty-Arr)
Γ ⊢ A → B type
Γ ⊢ A type Γ ⊢ B type
──────────────────────── (Ty-Prod)
Γ ⊢ A × B type
Γ ⊢ A type Γ ⊢ B type
──────────────────────── (Ty-Sum)
Γ ⊢ A + B type
Γ, x:A ⊢ B type
───────────────── (Ty-Pi)
Γ ⊢ Πx:A. B type
Γ, x:A ⊢ B type
───────────────── (Ty-Sigma)
Γ ⊢ Σx:A. B type
Γ ⊢ d : Dim
────────────────────── (Ty-Resource)
Γ ⊢ Resource(rk, d) type
Γ ⊢
────────────────── (Ty-Universe)
Γ ⊢ 𝒰ᵢ type
Γ ⊢ A : 𝒰ᵢ
──────────── (Ty-El)
Γ ⊢ El(A) type
i < j
──────────────── (Cumulative)
Γ ⊢ 𝒰ᵢ : 𝒰ⱼ
Dimensions form a first-class type with group structure:
Γ ⊢
─────────────── (Dim-Type)
Γ ⊢ Dim type
Γ ⊢
────────────── (Dim-Unit)
Γ ⊢ 1 : Dim
b ∈ {M, L, T, I, Θ, N, J}
───────────────────────── (Dim-Base)
Γ ⊢ b : Dim
Γ ⊢ d₁ : Dim Γ ⊢ d₂ : Dim
────────────────────────────── (Dim-Mul)
Γ ⊢ d₁ · d₂ : Dim
Γ ⊢ d : Dim
───────────────── (Dim-Inv)
Γ ⊢ d⁻¹ : Dim
Γ ⊢ d : Dim Γ ⊢ n : ℤ
─────────────────────────── (Dim-Pow)
Γ ⊢ d^n : Dim
Γ ⊢ d : Dim
────────────────────── (Dim-Id-L)
Γ ⊢ 1 · d ≡ d : Dim
Γ ⊢ d : Dim
────────────────────── (Dim-Id-R)
Γ ⊢ d · 1 ≡ d : Dim
Γ ⊢ d₁ : Dim Γ ⊢ d₂ : Dim Γ ⊢ d₃ : Dim
───────────────────────────────────────────── (Dim-Assoc)
Γ ⊢ (d₁ · d₂) · d₃ ≡ d₁ · (d₂ · d₃) : Dim
Γ ⊢ d₁ : Dim Γ ⊢ d₂ : Dim
────────────────────────────── (Dim-Comm)
Γ ⊢ d₁ · d₂ ≡ d₂ · d₁ : Dim
Γ ⊢ d : Dim
───────────────────────── (Dim-Inv-L)
Γ ⊢ d⁻¹ · d ≡ 1 : Dim
Γ ⊢ d : Dim
───────────────────────── (Dim-Inv-R)
Γ ⊢ d · d⁻¹ ≡ 1 : Dim
Resource types are indexed by dimensions:
Resource : ResourceKind → Dim → Type
This allows:
Resource(Energy, M·L²·T⁻²)— Energy in SIResource(Time, T)— TimeResource(Power, M·L²·T⁻³)— Power = Energy/Time
Γ, x:A ⊢ B type Γ ⊢ r : ResourceProfile
──────────────────────────────────────────── (Ty-Pi-Res)
Γ ⊢ Πʳx:A. B type
Γ, x:A ⊢ e : B Γ ⊢ r : ResourceProfile
──────────────────────────────────────────── (Tm-Lam-Res)
Γ ⊢ λʳx:A. e : Πʳx:A. B
Γ ⊢ f : Πʳx:A. B Γ ⊢ a : A resources_available(r)
──────────────────────────────────────────────────────── (Tm-App-Res)
Γ ⊢ f a : B[a/x]
Γ ⊢ A type Γ ⊢ C : Constraint
──────────────────────────────── (Ty-Constrained)
Γ ⊢ A @requires C type
Γ ⊢ a : A Γ ⊢ satisfies(a, C)
──────────────────────────────── (Tm-Constrain)
Γ ⊢ a : A @requires C
C₁ ⊇ C₂
──────────────────────────────────────── (Sub-Constraint)
Γ ⊢ A @requires C₁ <: A @requires C₂
Γ ⊢ a : A @requires C₁ Γ ⊢ A @requires C₁ <: A @requires C₂
────────────────────────────────────────────────────────────── (Sub-App)
Γ ⊢ a : A @requires C₂
Γ ⊢ A : Resource(rk, d) → Type
──────────────────────────────── (Fam-Resource)
Γ ⊢ A(r) type for r : Resource(rk, d)
Example: Bounded computation family:
BoundedComp : (b : Resource(Energy, J)) → Type
BoundedComp(b) = Σ(A : Type). Σ(compute : A). (cost(compute) ≤ b)
Eclexia's type theory is modeled in:
- Locally cartesian closed categories (LCCCs) for dependent types
- Symmetric monoidal categories for resources
- Enriched categories for graded effects
Let Set be the category of sets and functions.
Definition 4.1 (Eclexia Model Category). The semantic category Ecl is:
- Objects: Pairs
(X, ρ)whereX ∈ Setandρ : X → ResourceProfile - Morphisms: Functions
f : X → Ysuch thatρ_Y(f(x)) ≤ ρ_X(x)(resource non-increasing) - Composition: Standard function composition
- Identity: Identity function
Proposition 4.1. Ecl is cartesian closed.
Proof:
- Terminal object:
(1, λ_.∅)where1is singleton set - Products:
(X, ρ_X) × (Y, ρ_Y) = (X × Y, λ(x,y). ρ_X(x) ⊕ ρ_Y(y)) - Exponentials:
(Y, ρ_Y)^(X, ρ_X) = (X → Y, λf. sup_{x ∈ X} ρ_Y(f(x)) ⊖ ρ_X(x))□
⟦𝟙⟧ = (1, λ_.∅)
⟦𝔹⟧ = ({tt, ff}, λ_.∅)
⟦ℤ⟧ = (ℤ, λ_.∅)
⟦A → B⟧ = ⟦B⟧^⟦A⟧
⟦A × B⟧ = ⟦A⟧ × ⟦B⟧
⟦A + B⟧ = ⟦A⟧ + ⟦B⟧
⟦Resource(rk, d)⟧ = (ℝ × {d}, λr. ⟨rk ↦ r⟩)
⟦Πx:A. B⟧ = Π_{a ∈ ⟦A⟧} ⟦B⟧[a/x]
⟦Σx:A. B⟧ = Σ_{a ∈ ⟦A⟧} ⟦B⟧[a/x]
⟦x⟧_γ = γ(x)
⟦λx.e⟧_γ = λa. ⟦e⟧_{γ[x↦a]}
⟦e₁ e₂⟧_γ = ⟦e₁⟧_γ (⟦e₂⟧_γ)
⟦(e₁, e₂)⟧_γ = (⟦e₁⟧_γ, ⟦e₂⟧_γ)
⟦π₁ e⟧_γ = π₁(⟦e⟧_γ)
⟦π₂ e⟧_γ = π₂(⟦e⟧_γ)
⟦n unit⟧_γ = (n, dim(unit))
⟦e₁ +_ρ e₂⟧_γ = ⟦e₁⟧_γ +_ℝ ⟦e₂⟧_γ (with dimension check)
Theorem 4.1 (Soundness). If Γ ⊢ e : A then ⟦Γ⟧ ⊢ ⟦e⟧ : ⟦A⟧.
Proof: By induction on the typing derivation. Each typing rule corresponds to a categorical construction. □
Theorem 4.2 (Completeness). If ⟦Γ⟧ ⊨ ⟦e₁⟧ = ⟦e₂⟧ : ⟦A⟧ then Γ ⊢ e₁ ≡ e₂ : A.
Proof: The model is the term model modulo βη-equivalence, which is complete for the equational theory. □
Definition 5.1 (Grading Monoid). Let (R, ⊕, 0, ≤) be a preordered monoid of resource annotations:
R = ResourceProfile⊕: Resource combination (pointwise addition)0: Empty resource profile≤: Subsumption ordering
Definition 5.2 (R-Graded Category). An R-graded category C has:
- Objects: |C|
- Hom-sets: C(A, B) = ∪_{r ∈ R} C_r(A, B)
- Composition: If
f ∈ **C**_r(A, B)andg ∈ **C**_s(B, C), theng ∘ f ∈ **C**_{r ⊕ s}(A, C) - Identity:
id_A ∈ **C**_0(A, A)
Definition 5.3 (Graded Monad). An R-graded monad on category C consists of:
- Functor
T_r : **C** → **C**for eachr ∈ R - Natural transformation
η : Id → T_0(unit) - Natural transformation
μ_{r,s} : T_r ∘ T_s → T_{r ⊕ s}(multiplication)
Satisfying associativity and unit laws.
Definition 5.4 (Resource Monad). The resource monad Res_r for profile r is:
Res_r(A) = { (a, cost) | a ∈ A, cost ≤ r }
With operations:
η : A → Res_0(A)
η(a) = (a, 0)
μ : Res_r(Res_s(A)) → Res_{r⊕s}(A)
μ((a, c₁), c₂) = (a, c₁ ⊕ c₂)
Definition 5.5 (Graded Kleisli Category). The Kleisli category Kl(T) has:
- Objects: Same as C
- Morphisms: Kl(T)_r(A, B) = C(A, T_r(B))
- Composition: Kleisli composition using
μ
Dual to graded monads, graded comonads model coeffects (context requirements):
Definition 5.6 (Graded Comonad). An R-graded comonad on C consists of:
- Functor
D_r : **C** → **C**for eachr ∈ R - Natural transformation
ε : D_0 → Id(counit) - Natural transformation
δ_{r,s} : D_{r ⊕ s} → D_r ∘ D_s(comultiplication)
Example: The @requires constraint acts as a graded comonad:
D_C(A) = A @requires C
Proposition 5.1. There is an adjunction:
F_r ⊣ U_r : **Kl**(Res_r) → **C**
where F_r(A) = A and U_r(A) = Res_r(A).
Definition 6.1 (Domain). A domain D is a directed-complete partial order (dcpo) with a least element ⊥.
Definition 6.2 (Scott Continuity). A function f : D → E is Scott continuous if it preserves directed suprema:
f(⊔ S) = ⊔ { f(d) | d ∈ S }
Recursive types are solved via domain equations:
⟦μα.τ⟧ = fix(λD. ⟦τ⟧[D/α])
Theorem 6.1 (Domain Equation Solvability). For strictly positive τ, the equation D = ⟦τ⟧[D/α] has a solution.
Proof: By Smyth-Plotkin theorem on bilimits. □
Definition 6.3 (Resource Domain). A resource domain (D, cost) pairs:
- Domain
Dof values - Cost function
cost : D → ResourceProfile_⊥
D_⊥ = D ∪ {⊥}
For resource types:
⟦A⟧_⊥ = { (v, r) | v ∈ ⟦A⟧, r : ResourceProfile } ∪ {⊥}
Definition 6.4 (Fixed Point Operator).
fix : ((A → B) → (A → B)) → (A → B)
fix(F) = ⊔_{n ∈ ℕ} F^n(⊥)
Theorem 6.2 (Kleene's Theorem). fix(F) = F(fix(F)) for continuous F.
⟦e⟧ : Env → ⟦τ⟧
⟦x⟧ρ = ρ(x)
⟦λx.e⟧ρ = λv. ⟦e⟧ρ[x↦v]
⟦e₁ e₂⟧ρ = ⟦e₁⟧ρ (⟦e₂⟧ρ)
⟦fix f. e⟧ρ = fix(λv. ⟦e⟧ρ[f↦v])
⟦if e₁ then e₂ else e₃⟧ρ = cond(⟦e₁⟧ρ, ⟦e₂⟧ρ, ⟦e₃⟧ρ)
where cond(tt, d₁, d₂) = d₁
cond(ff, d₁, d₂) = d₂
cond(⊥, d₁, d₂) = ⊥
Theorem 6.3 (Computational Adequacy). For closed e : Bool:
⟦e⟧∅ = tt ⟺ e ⟶* true
⟦e⟧∅ = ff ⟺ e ⟶* false
⟦e⟧∅ = ⊥ ⟺ e diverges
Proof: Via logical relations between syntax and denotations. □
Definition 7.1 (Arena). An arena A = (M_A, λ_A, ⊢_A) consists of:
M_A: Set of movesλ_A : M_A → {O, P}: Polarity (Opponent/Proponent)⊢_A ⊆ M_A^* × M_A: Enabling relation
Definition 7.2 (Resource Arena). A resource arena (A, cost) extends arenas with:
cost : M_A → ResourceProfile: Resource cost per move
Definition 7.3 (Strategy). A strategy σ : A is a set of plays (alternating sequences of moves) satisfying:
- Prefix-closure
- Determinism on P-moves
- Resource compliance: Total cost ≤ budget
Strategies compose via parallel composition with hiding:
σ ; τ = { s ↾ A,C | s ∈ σ ∥ τ, s complete }
⟦𝟙⟧ = I (empty arena)
⟦A → B⟧ = ⟦A⟧ ⊸ ⟦B⟧ (linear implication arena)
⟦A × B⟧ = ⟦A⟧ & ⟦B⟧ (product arena)
⟦A + B⟧ = ⟦A⟧ ⊕ ⟦B⟧ (sum arena)
Conjecture 7.1 (Full Abstraction). For ground types:
⟦e₁⟧ = ⟦e₂⟧ ⟺ e₁ ≃_{ctx} e₂
TODO: Prove or find counterexample.
Definition 8.1 (Realizer). A realizer is a closed term e such that e ⊩ P (e realizes P).
Definition 8.2 (Resource Realizability). e ⊩_r P means:
erealizesPcost(e) ≤ r
e ⊩_r 𝟙 ⟺ e = ()
e ⊩_r 𝔹 ⟺ e = true ∨ e = false
e ⊩_r A → B ⟺ ∀a, s. a ⊩_s A ⟹ e a ⊩_{r⊕s} B
e ⊩_r A × B ⟺ π₁ e ⊩_r A ∧ π₂ e ⊩_r B
e ⊩_r ∀α. A ⟺ ∀T. e[T] ⊩_r A[T/α]
e ⊩_r Resource(rk, d) ⟺ e = n unit ∧ cost(e, rk) = n
Theorem 8.1 (Realizability Soundness). If Γ ⊢ e : A and γ ⊩_r Γ, then γ(e) ⊩_r A.
Proof: By induction on typing derivation. □
Definition 9.1 (Signature). An effect signature Σ is a set of operation symbols with arities:
Σ = { op : A → B, ... }
handle e with {
return x ↦ e_r,
op(x, k) ↦ e_op,
...
}
Define resource consumption as algebraic effect:
signature ResourceEffect {
consume : Resource(rk, d) → Unit
query_budget : Unit → Resource(rk, d)
defer_until : Condition → Unit
}
Γ ⊢ e : A ! ε
where ε is an effect row:
ε ::= ∅ | Op(A, B) | ε₁ ∪ ε₂
Γ ⊢ e : A ! (ε ∪ ρ)
────────────────────────
Γ ⊢ e : ∀ρ. A ! (ε ∪ ρ)
Γ ⊢ e : A ! (Op(S, T) ∪ ε)
Γ, x:A ⊢ e_r : B ! ε
Γ, x:S, k:(T → B ! ε) ⊢ e_op : B ! ε
─────────────────────────────────────────
Γ ⊢ handle e with {return x ↦ e_r, op(x, k) ↦ e_op} : B ! ε
Theorem 9.1. Algebraic effects with handlers are equivalent to parameterized monads.
T_{Op} A = Free_{Op}(A) = A + Σ_{op ∈ Op} (A_op × (B_op → T_{Op} A))
Session types describe communication protocols:
S ::= !A.S -- Send A, continue with S
| ?A.S -- Receive A, continue with S
| S ⊕ S' -- Internal choice
| S & S' -- External choice
| end -- Session end
| μα.S -- Recursive session
| α -- Session variable
Definition 10.1 (Resource Session). A resource session S @budget B pairs:
- Session type
S - Resource budget
Bfor entire session
Γ; Δ, c:S ⊢ P ▷ c:S'
───────────────────────────── (Send)
Γ; Δ, c:!A.S ⊢ c![e].P ▷ c:S
Γ, x:A; Δ, c:S ⊢ P ▷ c:S'
───────────────────────────── (Recv)
Γ; Δ, c:?A.S ⊢ c?(x).P ▷ c:S'
Γ; Δ, c:S @budget B ⊢ P
cost(P) ≤ B
───────────────────────────── (Session-Budget)
Γ; Δ, c:S ⊢ P
dual(!A.S) = ?A.dual(S)
dual(?A.S) = !A.dual(S)
dual(S ⊕ S') = dual(S) & dual(S')
dual(S & S') = dual(S) ⊕ dual(S')
dual(end) = end
Theorem 10.1 (Session Safety). Well-typed session programs are deadlock-free and respect resource budgets.
In HoTT, paths represent equality. For dimensions:
d₁ = d₂ : Dim ↔ Path_Dim(d₁, d₂)
Conjecture 11.1 (Resource Univalence).
(Resource(rk, d₁) ≃ Resource(rk, d₂)) ≃ (d₁ = d₂)
data Feasible (C : Constraint) : Type where
solution : (s : Solution) → satisfies(s, C) → Feasible(C)
path : (s₁ s₂ : Solution) → equivalent(s₁, s₂) → solution(s₁) = solution(s₂)
TODO: Develop cubical semantics for resource dimensions.
Definition 12.1 (Coherence). All diagrams of canonical morphisms commute.
Theorem 12.1 (Type-Theoretic Coherence). Eclexia's type theory satisfies coherence:
- All proofs of type equality are equal
- Type-checking is invariant under proof choice
Definition 12.2 (Canonicity). Every closed term of base type reduces to a canonical form.
Theorem 12.2 (Canonicity). If ⊢ e : 𝔹 then e ⟶* true or e ⟶* false.
Proof: By logical relations. Define:
V_𝔹 = {true, false}
E_𝔹 = {e | e ⟶* v, v ∈ V_𝔹}
Show by induction that ⊢ e : 𝔹 implies e ∈ E_𝔹. □
Theorem 12.3 (Resource Canonicity). If ⊢ e : Resource(rk, d) then e ⟶* n unit for some n : ℝ.
Proof: Similar to Boolean canonicity. □
Definition 13.1 (Semantic Values).
⟦𝟙⟧ = 1
⟦𝔹⟧ = Bool
⟦A → B⟧ = ⟦A⟧ → ⟦B⟧
⟦A × B⟧ = ⟦A⟧ × ⟦B⟧
Definition 13.2 (Reification and Reflection).
reify : ⟦A⟧ → Nf(A)
reflect : Ne(A) → ⟦A⟧
nf(e) = reify(eval(e, id))
eval : Tm → Env → ⟦A⟧
eval(x, ρ) = ρ(x)
eval(λx.e, ρ) = λv. eval(e, ρ[x↦v])
eval(e₁ e₂, ρ) = eval(e₁, ρ)(eval(e₂, ρ))
Theorem 13.1 (Strong Normalization). Every well-typed term has a normal form.
Proof Sketch:
- Define reducibility candidates for each type
- Show all terms are reducible
- Conclude by reducibility implying SN □
TODO: Full proof via Girard's method of reducibility candidates.
Theorem 13.2. Under finite resource budget B, well-typed terms normalize within bounded steps.
Proof: See PROOFS.md §9 (Termination). □
Theorem 14.1 (Decidability of Type Checking). Given Γ, e, A, deciding Γ ⊢ e : A is decidable.
Proof: Type checking rules are syntax-directed. Dimension equality is decidable (linear algebra over ℤ). □
Theorem 14.2 (Decidability of Type Inference). Given Γ, e, computing A such that Γ ⊢ e : A is decidable.
Proof: Extended Algorithm W with dimension constraint solving. □
Theorem 14.3 (Decidability of Subtyping). Given A, B, deciding A <: B is decidable.
Proof: Subtyping rules are inductive. Constraint subsumption is decidable (implication in linear arithmetic). □
Theorem 14.4 (Decidability of Dimension Equality). Given d₁, d₂, deciding d₁ ≡ d₂ is decidable in O(n) time.
Proof: Compare dimension vectors componentwise. □
Theorem 14.5 (Decidability of Constraint Satisfiability). Given constraint C and profile p, deciding satisfies(p, C) is decidable.
Proof: Constraints are linear inequalities; LP feasibility is polynomial-time decidable. □
Theorem 14.6 (Undecidability of General Termination). Termination of Eclexia programs without resource bounds is undecidable.
Proof: Reduction from the halting problem. □
- Dependent Resource Types: Full dependent types with resource indices
- Higher-Order Resources: Resources parameterized by types
- Probabilistic Resources: Stochastic resource consumption
- Concurrent Resources: Shared resource management
- Quantum Resources: Quantum computational resources
- Full Abstraction: Prove or disprove for game semantics
- Parametricity for Resources: Characterize free theorems
- Effectful Normalization: Strong normalization with effects
- Cubical Resources: Develop cubical semantics
- Certified Compiler: Verified compilation to LLVM
-
Machine Learning Integration:
- Learned resource prediction
- Neural-guided optimization
-
Blockchain/Smart Contracts:
- Gas as first-class resource
- Verified resource bounds
-
Distributed Systems:
- Network resources
- Distributed constraint solving
-
Quantum Computing:
- Qubit resources
- Quantum circuit optimization
| Term | Definition |
|---|---|
| Category | Objects + morphisms + composition + identity |
| Functor | Structure-preserving map between categories |
| Natural transformation | Morphism between functors |
| Adjunction | Pair of functors with unit/counit |
| Monad | Endofunctor with unit and multiplication |
| Comonad | Dual of monad |
| Enriched category | Hom-sets replaced by objects in V |
| Graded monad | Monad indexed by monoid |
| Term | Definition |
|---|---|
| Judgment | Statement derivable in type theory |
| Context | List of typed variable bindings |
| Type formation | Rules for constructing types |
| Introduction rule | How to construct terms of a type |
| Elimination rule | How to use terms of a type |
| β-reduction | Computational reduction |
| η-expansion | Extensionality principle |
| Definitional equality | Built-in equality |
| Propositional equality | Type of equalities |
Document Version: 1.0 Last Updated: December 2025 License: PMPL-1.0-or-later
@techreport{eclexia2025theory,
title={Type Theory and Categorical Semantics of Eclexia},
author={Jewell, Jonathan D.A.},
year={2025},
month={December},
institution={Eclexia Project},
url={https://eclexia.org/theory},
note={Version 1.0}
}