natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Regular logic is the internal logic of regular categories. Its logical operations consist only of truth, conjunction, and existential quantification, which makes it a superset of finite-limit logic and a subset of coherent logic and geometric logic.
Carsten Butz, Regular Categories and Regular Logic , BRICS LS-98-2 Aarhus 1998. (brics)
B. Fong, D. Spivak, Graphical Regular Logic , arXiv:1812.05765 (2018). (abstract)
Peter Johnstone, Sketches of an Elephant II , Oxford UP 2002. (Section D1.2)
Jaap van Oosten, Basic category theory , BRICS LS-95-1 Aarhus 1995. (Section 4.2) (pdf)
Last revised on November 16, 2022 at 06:05:21. See the history of this page for a list of all contributions to it.