<p>One semantic criterion is preservation of <span class="math-container">$\omega$</span>-colimits, or <span class="math-container">$\omega$</span>-cocontinuity. AFAIK, initial algebras of such functors correspond to finitary inductive types in type theory. The construction of initial algebras, given by <a href="https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#AdameksTheorem" rel="nofollow noreferrer">Adámek's theorem</a>, can be formalized inside type theory as well. It's described in <a href="https://link.springer.com/content/pdf/10.1007%2Fs10817-018-9474-4.pdf" rel="nofollow noreferrer">this paper</a> and there's a Coq formalization for it. Probably there is a generalization of this to transfinite colimits, which would give us infinitary inductive types, but for this I don't know any formalization.</p>

CC BY-SA 4.0
2020-02-07T09:51:15.703Z
That's $\aleph_0$-accessibility, is it not? I was thinking that accessibility should have a type-theoretic formulation in which the cardinals are replaced by universes (so a $U$-accessible functor), but then we still need another condition that captures preservation of "filtered $U$-colimits", whatever that is.
Andrej Bauer
CC BY-SA 4.0
2020-02-04T12:08:45.600Z
2020-02-07T07:54:00.550Z
2020-02-07T07:54:00.550Z
András Kovács
<p>If we consider a definition of recursive type as:</p>

<pre><code>F : Type -&gt; Type;
T = fix F;
</code></pre>

<p>It is customary to talk about the functor <code>F</code> needing to be positive or strictly positive in order to avoid non-termination in the recursor.</p>

<p>I'm familiar with the usual syntactic definition of strict positivity, but I'm looking for corresponding semantic definitions, especially ones that can be expressed in the system (rather than being defined at the meta level).</p>

<p>The closest I have found is the work on containers <a href="http://www.cs.nott.ac.uk/~psztxa/publ/cont-tcs.pdf" rel="noreferrer">(Abbott et.al., 2005)</a>, but it appears to require some "creativity" to come up with a container corresponding to a given functor and then prove equivalence between the two.  I'm looking for something that talks more directly about the properties of <code>F</code>.</p>

CC BY-SA 4.0
2020-02-03T19:42:08.960Z
I'm confused: a functor is "positive" if it is co-variant, that is it has a `map_f : (A -> B) -> F A -> F B`. What more do you need?
cody
CC BY-SA 4.0
2020-02-03T21:32:29.673Z
@cody: Duh, yes, I see I messed my copy&paste and left plain positivity in there.  I'm looking for the "strict positivity".  I updated my question accordingly.
Stefan
CC BY-SA 4.0
2020-02-04T07:41:18.073Z
Some sort of accessibility?
Andrej Bauer
<type-theory>
Semantic definition of strict positivity for a functor
Stefan
# Semantic definition of strict positivity for a functor

(Asked by: username_0 on 2020-02-03)

If we consider a definition of recursive type as:
F : Type -> Type;
T = fix F;

It is customary to talk about the functor F needing to be positive or strictly positive in order to avoid non-termination in the recursor.
I'm familiar with the usual syntactic definition of strict positivity, but I'm looking for corresponding semantic definitions, especially ones that can be expressed in the system (rather than being defined at the meta level).
The closest I have found is the work on containers (Abbott et.al., 2005), but it appears to require some "creativity" to come up with a container corresponding to a given functor and then prove equivalence between the two.  I'm looking for something that talks more directly about the properties of F.

**Tags:** type-theory

> **Comments:**
> **username_1**: I'm confused: a functor is "positive" if it is co-variant, that is it has a `map_f : (A -> B) -> F A -> F B`. What more do you need?  
> **username_0**: @username_1: Duh, yes, I see I messed my copy&paste and left plain positivity in there.  I'm looking for the "strict positivity".  I updated my question accordingly.  
> **username_2**: Some sort of accessibility?  

---

## 1 answers

### Answer by username_3 on 2020-02-04. Score: 9

One semantic criterion is preservation of $\omega$-colimits, or $\omega$-cocontinuity. AFAIK, initial algebras of such functors correspond to finitary inductive types in type theory. The construction of initial algebras, given by [Adámek's theorem](https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#AdameksTheorem), can be formalized inside type theory as well. It's described in [this paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-018-9474-4.pdf) and there's a Coq formalization for it. Probably there is a generalization of this to transfinite colimits, which would give us infinitary inductive types, but for this I don't know any formalization.

> **Comments:**
> **username_2**: That's $\aleph_0$-accessibility, is it not? I was thinking that accessibility should have a type-theoretic formulation in which the cardinals are replaced by universes (so a $U$-accessible functor), but then we still need another condition that captures preservation of "filtered $U$-colimits", whatever that is.  

---

