[[!redirects contractible]] ## Idea A type which represents the notion of logical truth in homotopy type theory. ## Definitions A __contractible type__ is a type $A$ with a term $$c: \sum_{a:A} \prod_{b:A} a = b$$ Since contractible types are inhabited [[proposition]]s, there is an alternate definition of contractible type as a type $A$ with a point $e:A$ and a term $$p: isProposition(A)$$ The above term could be replaced with the following instead: $$p: \prod_{a:A} a = e$$ and that $A$ is a proposition follows from concatenation and inverses of identity types. The above definition could be reworded in natural language as a type that is inhabited and a proposition; i.e. as a type $A$ with a term $$c: A \times isProposition(A)$$ ## Examples * The [[unit type]] is a contractible type. * The [[interval type]] is a contractible type. * By the third definition, every [[cone type]] is a contractible type, of which the unit type (cone type of the empty type) and the interval type (cone type of the unit type) are examples of cone types. ## See also * [[proposition]] * [[set]]