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.