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

fix

Browse Source
This commit is contained in:
Jlh18 2021-12-03 14:01:21 +00:00
parent 289b5c474f
commit e72c0cb434
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
1FundamentalGroup/Quest0Solutions.agda
View File

@ -43,7 +43,7 @@ pathEmpty : (A : Type) → Type₁
pathEmpty A = A ≡ ⊥ pathEmpty A = A ≡ ⊥
isoEmpty : (A : Type) → Type isoEmpty : (A : Type) → Type
isoEmpty A = A ≅ ⊥ isoEmpty A = {!!}
outOf⊥ : (A : Type) → ⊥ → A outOf⊥ : (A : Type) → ⊥ → A
outOf⊥ A () outOf⊥ A ()