Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Now that we have an entry dependent function, I feel it’s time to showcase also the corresponding notation
$f \;\,\colon\;\, (d \,\colon\, D) \to C_d$for
$f \,\colon\, \underset{d \,\colon\, D}{\prod} \, C_d$and dually for dependent pairs; and to cross-link all these notions at a glance.
So I am hereby making a little table, meant to be !include
-d into the “Related concepts”-sections of the relevant entries.
(Currently the table says “dependent co-product” for what everyone calls the “dependent sum”. I can change that if there is much insistence that I should, and I know it’s an uphill battle, but it bugs me that saying “dependent sum” for the dependent coproduct was a step in the wrong direction.)
1 to 1 of 1