Ali Caglayan

I have rewritten to and from using refines now. I could probably improve the speed by hinting to coq a bit more but it is reasonable for now. It is...

How do we get the 3x3 diagram back from the "dependently typed form"? I don't see how the maps are encoded.

Ok so I can see how we get 9 objects and 12 maps from this. How do we turn 9 objects and 12 maps into this dependently encoded type however?

OK so I have played around with this in coq, I am a bit stuck trying to make Axx however. See my [Dep3x3 branch](https://github.com/Alizter/HoTT/blob/dep3x3/contrib/Dep3x3.v). --- Edit: actually nevermind, I managed...

@mikeshulman I am having a look at this again. Can you elaborate on your "symmetric double pushout" and what you expect it to look like?

Sorry, Mike there was nothing unclear. Andreas and I are currently working on it. We have sort-of managed to define the HIT.

What happens to square constructors in the dependent eliminator? I had to make some sort of dependent path between Dependent squares. Is this some sort of dependent cube, because I...

I stopped working on this about a month ago, since the path-algebra (even with the cubical library) got a bit heavy. I am sure if I drank enough coffee I...

Another argument has come to mind. Colimits satisfy the property of "having a right adjoint". From this we can show that the colimit functor preserves colimits. Hence colimits commute. From...

OK, I have made some progress. Egbert's suggestion does work. I have managed to formalize a (terribly written) proof that (R -> X) (C -> X) for all X, where...