remove unused variable a in transportd

martinescardo / HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

GNU General Public License v3.0

218 stars 18 forks source link

Closed TashiWalde closed 4 years ago

TashiWalde commented 4 years ago

Hi Martin,

I have been working through your notes and having great fun with it.

I noticed that in the definition of transportd there is an unused premise (a : A x).

Best regards, Tashi

martinescardo commented 4 years ago

Ooops. You are right. Thanks.