germax26/TheHoTTGame
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

plan change

Browse Source
This commit is contained in:
Jlh18 2021-08-16 19:05:17 +01:00
parent c93ca368b2
commit c22a5777d3
1 changed files with 15 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Plan.org
View File

@ -79,9 +79,9 @@
** SuperUltraMegaHyperLydianBosses ** SuperUltraMegaHyperLydianBosses
- natural number object unique and _+_ unique on any nat num obj + natural number object unique and `_+_` unique on any nat num obj
+ nat num obj unique + nat num obj unique
+ _+_ unique on a model of nat num obj + `_+_` unique on a model of nat num obj
- axiomatize addition on naturals - axiomatize addition on naturals
- naturals is a set - naturals is a set
- fun extensionality - fun extensionality
@ -89,3 +89,16 @@
- propositions - propositions
- propositions closed under sigma types - propositions closed under sigma types
+ univalence + univalence
** Top 100 (set theoretic) misconceptions about type theory
+ Propositions
+ Proof relevance
+ Propositions are _inside the theory_
+ Membership not the same as :
+ typing is unique (doesn't make sense to intersect two types)
+
+ Though set theory had fewer axioms type theory's assumptions are more intuitive (hence intionistic type theory)
There is no fiddling about with membership to construct things e.g. cartesian product
+ 'we cannot use LEM' ~ not assuming law of excluded middle _globally_ means type theory theorems are stronger!
+