michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 02:55:44 +00:00
parent a96dd16303
commit 9b55a90c5e
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/HottBook/Chapter3.lagda.md
View file

@ -14,6 +14,13 @@ isSet : (A : Set) → Set
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
```
### Example 3.1.1
```
𝟙-is-Set : isSet 𝟙
𝟙-is-Set tt tt p q = {! !}
```
## 3.2 Propositions as types?
## 3.4 Classical vs. intuitionistic logic