<foo> simply produces <foo>in the text).
<URL: http://somewhere.tld/ >,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto: URI,
e.g. mailto:my.email@somewhere.tld,
if you do not have a genuine Web site).
ncf (2023-12-23T12:34:59Z)
La théorie *cubique* des types, basée sur la théorie homotopique des types, et implémentée dans Cubical Agda, permet d'avoir de vrais types quotients qui réduisent correctement (ce sont un cas particulier des "types inductifs supérieurs" (Higher Inductive Types) limités au niveau des ensembles (types 0-tronqués)).
Par exemple: <URL: https://1lab.dev/Data.Set.Coequaliser.html >
Thomas (2023-12-23T08:32:07Z)
Introduction intelligible, mis à part les addenda. Je n'ai toujours pas vraiment compris comment se matérialise côté typage la distinction entre les deux notions d'existence — le fait que je n'ai aucune notion en théorie des types et ne connaisse pas les langages utilisés ici n'aide certainement pas… (mais bon, ce n'est pas grave, à mon niveau la compréhension de CH dans le cas "Martin-Löf" me suffit).
Autre sujet, mais puisque tu mentionnes les problématiques de preuve constructive, logique intuitionniste, etc. cette question <https://math.stackexchange.com/questions/4831457/non-constructiveness-and-finite-mathematics> que je me posais et la réponse obtenue t'intéresseront peut-être.