michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

undraft
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2024-06-29 17:39:27 -05:00
parent 06d483b3dd
commit 76ea2d345a
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/content/posts/2024-06-28-boolean-equivalences.lagda.md
View file

@ -3,7 +3,6 @@ title: "Boolean equivalences in HoTT"
slug: 2024-06-28-boolean-equivalences slug: 2024-06-28-boolean-equivalences
date: 2024-06-28T21:37:04.299Z date: 2024-06-28T21:37:04.299Z
tags: ["agda", "type-theory", "hott"] tags: ["agda", "type-theory", "hott"]
draft: true
--- ---
This post is about a problem I recently proved that seemed simple going in, but This post is about a problem I recently proved that seemed simple going in, but
@ -299,7 +298,7 @@ $$
This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]: This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]:
[^equiv-isProp]: I haven't worked that far in the book yet, but this is shown in Theorem 4.2.13 in the [HoTT book][book]. [^equiv-isProp]: This is shown in Theorem 4.2.13 in the [HoTT book][book].
I might write a separate post about that when I get there, it seems like an interesting proof as well! I might write a separate post about that when I get there, it seems like an interesting proof as well!
``` ```