Pushout draft #335
Pushout draft #335
Conversation
|
@martinescardo I finished a first draft of my pushout experiment. It is currently in the form where I postulate induction + computation rules and derive the UP. But I will eventually swithc this as we discussed. |
|
@martinescardo Got it! Also should I change the name of cocone? To specify that it is a cocone of a pushout diagram? Or a cocone of a cospan? Or something along these lines. |
|
@martinescardo I believe this file is now in a state that is ready for review. I think this file can be greatly improved in a few ways that I am going to continue to explore and can outline for any interested party. But I think it is best to focus on the work I currently have in the meantime. Edit: Typos and indentation now fixed. |
Pushouts are pustulated via a record type. We explore deriving universal properties from induction and computation rules.