https://agda.readthedocs.io/en/latest/language/polarity.html
I really don't know why strictly positive is used here as well, when it is only one of the conditions, that of the closure to type variables.
I know how to use it now, but using the same name for two different things is confusing.
I literally searched for 30+ minutes to find a good definition.
@apostolis It's two different mechanisms to check for the same property, and the syntax-based mechanism is more conservative (more false non-strictly-positives) than the modality-based one.
I think the best semantic definition of a strictly positive operation on types [type families] is a polynomial functor (a.k.a. [indexed] container functor) on the category of [indexed] types.
@apostolis See here for the associated abstract, talk & PR:
https://anuyts.github.io/#agda-polarities
For a specific indexed coinductive type, what would be the easiest way to define its functor and terminal object with regards to its coalgebra?
For a non-indexed, it is pretty easy, but not for the indexed case.
For example, how would you define the functor for this :
"
record Stream (n : ℕ) : 𝓤₀ ̇ where
coinductive
field
k : ℕ
cond : succ n ≤ k
next : Stream k
"
@apostolis
So you get a functor F : Type^Nat -> Type^Nat with
F X n = Σ (k : Nat) . (succ n ≤ k) x (X k).
I suspect we're talking past each other?
@anuytstt Perfect, that is what I was expecting but I couldn't find it somewhere.
In the paper , it is defined differently.
@apostolis IFunc is the type of functors from Set^I to Set, which are not endofunctors, and therefore do not qualify to have any fixpoints.
Could you link to this paper?
I think that the main point here is that although programming categorically is easy, there is not enough documentation how to do it, it is an antipattern, and the papers that use categories are not suitable for the working programmer / mathematician.
@apostolis Oh no, I should stop recommending this paper to people…
Perhaps this presentation was sensible when the paper was written, but at least in today's perspective, this seems very undidactical.