UNIVERSAL QUANTIFICATION

-type represents universal quantification over a domain, encoding properties or functions that hold for all elements of a type. It is the type-theoretic analogue of logical and forms the basis for dependent function spaces (Π-types) when the body is a type family.

In this system, -types are used to define predicates, sets, measures, and logical statements, bridging classical analysis with type theory.

Formation

(-Formation). The universal quantification type is formed over a domain and a body or , representing "for all , holds."

type exp =
  | Forall of string * exp * exp  (* ∀ (x : A), B(x) *)

Introduction

(-Introduction). A term of type is introduced via a lambda abstraction , where for all .

let lam (x : string) (a : exp) (b : exp) : exp =
  Lam (x, a, b)  (* λ x : A. b *)

Elimination

(-Elimination). Given and , the application yields .

let apply (f : exp) (a : exp) : exp =
  App (f, a)  (* f a *)

Computation

(-Computation). The β-rule states that applying a lambda abstraction reduces to substitution.

let reduce env ctx = function
  | App (Lam (x, _, body), arg) -> subst x arg body
  | _ -> ...

Uniqueness

(-Uniqueness). The η-rule states that any function equals its eta-expanded form.

(* Implicit in type equality *)
let equal env ctx f (Lam (x, a, App (f', Var x'))) =
  x = x' && equal env ctx f f'

Theorems

(Predicate Logic). If holds and , then holds (modus ponens in type theory).

(Set Definition). Sets in this system are defined as -types with a propositional body, e.g., .

let set_a = Set (Lam ("x", Real, RealIneq (Gt, Var "x", Zero)))