nLab dependent functions and dependent pairs -- table
Redirected from "initial algebra of a presentable ∞-monad".
| type former: | meaning of terms: |
|---|---|
| dependent product | dependent function / section of bundle |
| dependent coproduct (aka: dependent sum) | dependent pair / element of bundle |
Created on January 20, 2023 at 17:55:23. See the history of this page for a list of all contributions to it.