search

fpvandoorn / lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)
Apache License 2.0
0 stars 0 forks source link

define binary pointed maps #4

Closed fpvandoorn closed 6 years ago

fpvandoorn commented 6 years ago

The type ppmap A (ppmap B C) requires function extensionality to define inhabitants, since a_0 has to be sent to the constant pointed map. Define a new type bpmap A B C which is equivalent but doesn't require function extensionality.

fpvandoorn commented 6 years ago

See https://github.com/cmu-phil/Spectral/blob/master/pointed_binary.hlean. It works, but it does require a whole range of new definitions (like composing a map with a binary map and homotopies between binary maps).