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

Merge pull request #18 from iblech/patch-1

Browse Source 
compatibility with recent cubical
This commit is contained in:
jlh 2024-01-19 21:08:11 -05:00 committed by GitHub
commit d880d951ae
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
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/Preambles/P0.agda
View File

@ -2,7 +2,7 @@ module 1FundamentalGroup.Preambles.P0 where
open import Cubical.Data.Empty using (⊥) public
open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public
open import Cubical.Data.Bool public
open import Cubical.Data.Bool hiding (elim) public
open import Cubical.Foundations.Prelude
renaming ( subst to endPt
; transport to pathToFun