Dedined in abbott2004-containers
Properties
locally cartesian closed category disjoint Coproduct (Category Theory) and Initial algebras of container functors (the categorical analogue of W Type)
strictly positive types exist in any Martin-Lof category abbott2004-containers