[[!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: \prod_{a:A} \prod_{b:A} a = b$$ The above term could be replaced with the following instead: $$p: \prod_{a:A} a = e$$ and that every identity type in $A$ is a proposition follows from concatenation and inverses of identity types. There is also a fourth definition of contractible types as a type $A$ with a term $$c: A \times \prod_{a:A} \prod_{b:A} a = b$$ ## 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]]