LAURENT

ANALYTICAL TYPE SYSTEM

MLTT

  1. PROP
  2. U0 : U1
  3. FORALL
  4. EXISTS
  5. AND
  6. OR
  7. REAL

SET

  1. SET
  2. EQZ3
  3. \
  4. INTERSECT
  5. CLOSURE
  6. POWER
  7. QUOTIENT

CALC

  1. SEQ
  2. INF
  3. SUP
  4. LIMIT
  5. SUM
  6. UNION
  7. MEASURE
  8. LEBESGUE
  9. BOCHNER

We omit identity types Id, idp, J (HoTT, MLTT-80, MLTT-75) to keep the system lean with Pi and Set truncated Sigma relying instead on Prop predicates. Also we have explicitly built in set theory with open sets and topology to have more classical core. Built-in inequalities propositional resolution by reduction is handled by external Z3 SMT solver.



LAURENT.PDF


.

The doesn't have proper syntax yet, that's said you use it as OCaml framework working in pure AST as you would do in Lisp.

$ git clone \ [email protected]:groupoid/laurent $ opam install z3 $ ocamlfind ocamlc -o laurent \ -package z3 -linkpkg src/laurent.ml

SYNTAX

SEMANTICS


MLTT

(-Formation, Dependent Product). -types represents the way we create the spaces of dependent functions with domain in and codomain in type family over .

(-Formation, Dependent Sum). The dependent sum type is indexed over type in the sense of coproduct or disjoint union, where only one fiber codomain is present in pair.

Bibliography


ANALYSIS

[1]. L.Schwartz. Analyse Mathematique (1967)
[2]. E.Bishop. Foundations of Constructive Analysis (1967)
[3]. D.Bridges. Constructive math: a foundation for computable analysis (1999)
[4]. W.Ziemer, M.Torres. Modern Real Analysis (2017)
[5]. A.Booij. Analysis in Univalent Type Theory (2020)
[6]. Z.Murray. Constructive Real Numbers in the Agda (2023)




Присвячується Володимиру Олександровичу Клименку. Механізована верифікація теорем функціонального аналізу і теорії розподілів Лорана Шварца у власній теорії типів на основі MLTT-72.