square type

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

In homotopy type theory a **square type** is the product type of the interval type with itself.

Created on May 12, 2022 at 23:14:47. See the history of this page for a list of all contributions to it.