search

thehottgame / TheHoTTGame

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
125 stars 15 forks source link

Correct the definitions of `Sym*` and `*Sym` #14

Closed ghost closed 2 years ago

ghost commented 2 years ago

See this PR in the repository for the guide:

Sym* and *Sym should give proofs of Id (Sym p * p) rfl and Id (p * Sym p) = rfl, respectively, i.e. "Concatenating p with Sym p on the left and right gives rfl", from the guide. Currently, they are defined with Id rfl (p * Sym p) and Id (p * Sym p) rfl respectively, which aren't the right statements -- they both just say that concatenating p by Sym p on the right does nothing, but in different ways.

I also swapped their order so that they would be analogous to rfl* and *rfl.