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

The *wedge sum type* is an axiomatization of the wedge sum in the context of homotopy type theory.

The wedge sum of two pointed types $(A,a)$ and $(B,b)$ can be defined as the higher inductive type with the following constructors:

- Points come from the sum type $in : A + B \to A \vee B$
- And their base point is glued $path : inl(a) = inr(b)$ Clearly this is pointed.

The wedge sum of two types $A$ and $B$, can also be defined as the pushout type of the span

$A \leftarrow \mathbf{1} \rightarrow B$

where the maps pick the base points of $A$ and $B$. This pushout is denoted $A \vee B$ and has basepoint $\star_{A \vee B} \equiv \mathrm{inl}(\star_A)$

Created on June 9, 2022 at 01:34:40. See the history of this page for a list of all contributions to it.