Boolean hyperdoctrine

**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**

A *Boolean hyperdoctrine* $P$ is a hyperdoctrine for lattices which are Boolean algebras

$P \;\colon\; T^{op} \to BooleanAlgebra
\,.$

A discussion of the free Boolean hyperdoctrine generated from a signature is in

Last revised on August 19, 2021 at 05:30:56. See the history of this page for a list of all contributions to it.