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.
finitely complete category, cartesian functor, cartesian logic, cartesian theory
regular category, regular functor, regular logic, regular theory, regular coverage, regular topos
coherent category, coherent functor, coherent logic, coherent theory, coherent coverage, coherent topos
geometric category, geometric functor, geometric logic, geometric theory
Carsten Butz, Regular Categories and Regular Logic , BRICS LS-98-2 Aarhus 1998. (brics)
Jaap van Oosten, Basic category theory , BRICS LS-95-1 Aarhus 1995. (Section 4.2) (pdf)
Peter Johnstone, Sketches of an Elephant II , Oxford UP 2002. (Section D1.2)