[Agda] Fin n -> Fin n extensional?

Jacques Carette carette at mcmaster.ca
Wed Feb 18 15:25:15 CET 2015


Does anyone have a proof in Agda that functions at type (Fin n -> Fin n) 
are extensional?
Jacques


More information about the Agda mailing list