Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
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 complete loop graph is a loop graph? $G$ where between any two vertices $a:G$ and $b:G$ there is exactly one edge $p:a \to_G b$.
In the context of homotopy type theory, a complete loop graph is a type $G$ with a type family $\to_G$ such that the dependent type $a \to_G b$ is a contractible type for all elements $a:G$ and $b:G$.
A complete loop graph is univalent, a subsingleton, or a proposition if the canonical function
is an equivalence of types.
Last revised on September 22, 2022 at 15:26:31. See the history of this page for a list of all contributions to it.