Zulip Chat Archive
Stream: Infinity-Cosmos
Topic: Constructing morphism from inner 2-horn
Julian Komaromy (Apr 09 2025 at 15:02):
I am trying to define the the function
def horn_from_path (X : SSet) (f : SSet.Path X 2) : Λ[2, 1].toSSet ⟶ X
which sends the vertices and edges of Λ[2, 1] to the vertices and edges of the path f. Is there an obvious strategy to define such a function?
Joël Riou (Apr 09 2025 at 15:20):
In my repository, I have code doing essentially that at https://github.com/joelriou/topcat-model-category/blob/7981f135abfe3a18175ea638b2aa1d3a357786fb/TopCatModelCategory/SSet/Horn.lean#L170-L205 (this expresses this horn as a pushout, and then you can use the two edges of the path), but this code depends on ongoing pull requests to mathlib than I have mentioned at
Julian Komaromy (Apr 09 2025 at 15:21):
Thanks, I'll take a look. I figured that the PR you mentioned is probably relevant :thumbs_up:
Last updated: May 02 2025 at 03:31 UTC