aerskine

Keybase proof

I hereby claim:

• I am aerskine on github.
• I am thedatabase (https://keybase.io/thedatabase) on keybase.
• I have a public key ASCzOpYOoXd_6Vm7hCg6BTg0xZs7WuKqHBtSHeEaou_wMAo

To claim this, I am signing this object:

aerskine

{-# OPTIONS --without-K #-}

{-
 Load this file as-is, and Agda will highlight the S m == S n term, and complain:

Sort _4  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,27-37 ]
_A_6 : Set _4  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,31-33 ]
_8 : _A_6  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,27-30 ]
_10 : _A_6  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,34-37 ]
_11 : _8 == _10  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:44,10-13 ]