Contents

# Contents

## Idea

A pointed type is a type equipped with a term of that type.

## Properties

There is a way of pointing any type $X$ by forming the sum $X+\mathbf{1}$ and taking $inr(\star_{\mathbf{1}})$ as the base point.

### Propositions as types

In the propositions as types interpretation of type theory, every pointed type represents a true proposition. Contrast this to an inhabited type, which only represents the double negation of a true proposition.

## Type of pointed types

For a given type universe $\mathcal{U}$ the type of pointed types is

$\mathcal{U}_+\equiv \sum_{X:\mathcal{U}}X$

## References

Last revised on February 4, 2023 at 11:39:18. See the history of this page for a list of all contributions to it.