QUOTIENT TYPE

The type constructs a type from a base type and an equivalence relation, quotienting the base type by the relation. It is a fundamental construct in type theory for defining types modulo equivalence, supporting applications like setoids and modular arithmetic.

Following Lean’s quotient module, this type is formed via , introduced via , and eliminated via the dependent eliminator , ensuring computational and logical consistency.

This system assumes the quotient type is built into the core, matching Lean’s design, where defines the type, maps elements to equivalence classes, and provides the dependent elimination principle. The non-dependent eliminator is derivable from .

Formation

(-Formation). The quotient type is formed over a base type and a relation , yielding a new type .

type exp =
  | Quotient of exp * exp  (* Quotient α r *)
  | Quot of exp * exp * exp  (* Quot α r a *)
  | QuotLift of exp * exp * exp * exp * exp  (* QuotLift α r β f h *)
  | QuotInd of exp * exp * exp * exp  (* QuotInd α r β h *)

Introduction

(-Introduction). A term of type is introduced by the constructor , which maps an element to its equivalence class under .

let quot_intro (alpha : exp)
  (r : exp) (a : exp) : exp =
    Quot (alpha, r, a)

Elimination

(-Elimination). The dependent eliminator allows proving a property for all , given it holds for all .

let quot_ind (alpha : exp) (r : exp)
  (beta : exp) (h : exp) : exp =
    QuotInd (alpha, r, beta, h)

Computation

(-Computation). The application of to a term reduces to the application of the hypothesis to , ensuring computational soundness.

let reduce env ctx = function
  | App (QuotInd (_, _, _, h), Quot (_, _, a)) -> App (h, a)
  | _ -> ...

Uniqueness

(-Uniqueness). Two quotient types and are equal if and .

For terms, if holds, reflecting the quotient’s identification.

let equal_quotient env ctx (Quotient (a1, r1)) (Quotient (a2, r2)) =
  equal env ctx a1 a2 && equal env ctx r1 r2

Theorems

(Non-Dependent Elimination). The non-dependent eliminator lifts a function to a function , provided respects the relation , and is derivable from .

let quot_lift (alpha : exp) (r : exp)
  (beta : exp) (f : exp) (h : exp) : exp =
    QuotLift (alpha, r, beta, f, h)

(Non-Dependent Elimination Derivability). The non-dependent eliminator lifts a function to a function , provided respects the relation , and is derivable from as follows:

let quot_lift_derivable alpha r beta f h =
   let beta_prop = Lam ("q", Quotient (alpha, r), beta) in
   let h_prime = Lam ("a", alpha, App (f, Var "a")) in
     QuotInd (alpha, r, beta_prop, h_prime)

(Soundness of Lift). The lifted function respects the equivalence relation: if , then