Strictly Positive Endofunctor

Idea

This idea is the functor analage to strictly positive types.

Definition

A strictly positive endofunctor is an endofunctor $F:\mathcal{C}\to \mathcal{C}$ formed built up from functors where the variable $X$ appears only in strictly positive positions. In the context of dependent type theory and Agda, this restriction is syntactic and ensures the consistency of Inductive Type.

For a type constructor $F(X)$, $X$ occurs strictly positively if it never appears to the left of an arrow in the domain of a constructor argument. Formally, the class of strictly positive functors is the smallest class $SPF$ such that:

1. If $A$ is a type not containing $X$, then the constant functor $X\mapsto A$ is in $SPF$.
2. The identity functor $X\mapsto X$ is in $SPF$.
3. If $F,G\in SPF$, then their coproduct $X\mapsto F(X)+G(X)$ and product $X\mapsto F(X)\times G(X)$ are in $SPF$.
4. If $F\in SPF$ and $A$ is a type not containing $X$, then the exponentiation $X\mapsto A\to F(X)$ is in $SPF$.

Properties

Strict positivity excludes occurrences of $X$ in the domain of a function argument. This constraint prevents the construction of paradoxes such as the Russell paradox or violations of Cantor’s theorem within the type system.

In extensional type theory and HoTT, strictly positive endofunctors correspond to containers. Every strictly positive functor $F$ is natural isomorphism to a functor of the form:

$F(X)\cong {\sum }_{s:S}(P(s)\to X)$

where $S$ is a type of shapes and $P(s)$ is a type of positions for each shape $s$.

References

• abbott2004-containers
• hott2013-book