3 ms·
Fun Fact: Agda called types "Set", e.g: data ℕ : Set where zero : ℕ suc : ℕ → ℕ This was recently deemed inappropriate: "Bye bye Set" "Set and
by hackandthink 3y ago
Fun Fact:
Agda called types "Set", e.g:
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
This was recently deemed inappropriate:
"Bye bye Set"
"Set and Prop are removed as keywords"
https://github.com/agda/agda/pull/4629 https://github.com/agda/agda/pull/4629
- sortalongo 3y agoI think that's because, before the HoTT extensions, all definable types could be seen as in the Category of Sets. And they didn't get rid of Set and Prop entirely. They just made them default-imported symbols instead of keywords.