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

Update Quest4Solutions.agda

Browse Source
This commit is contained in:
jlh 2022-03-30 15:55:34 +01:00 committed by GitHub
parent a55e3bfc57
commit d10e5805a2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
0Trinitarianism/Quest4Solutions.agda
View File

@ -44,7 +44,7 @@ rfl* p = rfl
*Sym : (p : Id x y) → Id (p * Sym p) rfl
*Sym rfl = rfl
Sym* : (p : Id x y) → Id rfl (p * Sym p)
Sym* : {A : Type} {x y : A} (p : Id x y) → Id (Sym p * p) rfl
Sym* rfl = rfl
Assoc : (p : Id w x) (q : Id x y) (r : Id y z)