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.
higher coinductive types in dependent type theory, to fill out a link from the higher observational type theory article
On this page,
- The amazing right adjoint of a specified type T is a higher coinductive type 1/T cogenerated by a 1-dimensional field root in T,
what does “a 1-dimensional field root in T” mean?
I assume “field” is as in “entry of a record type” and just means here “cogenerator”, and “1-dimensional” means that it’s a term of Id-type.
1 to 3 of 3