Simplicial homotopies - Jack McKoen

Stream: Lean Together 2024

[Johan Commelin]

@Jack McKoen Thanks for your recorded talk https://www.youtube.com/watch?v=lZ6zHma7Rj0
It's great that more theory of simplicial sets is being formalized! Are you planning to contribute Prod and IHom to mathlib in the near future?

[Jack McKoen]

Thanks Johan! I would like to add Prod and IHom to mathlib very soon, I just need to wrap each of them in a nice PR with some associated simp lemmas and things like that. I intend to do something like this in the next week or so