search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Change the Constructor Name of Sequential Colimits #1046

Closed kangrongji closed 11 months ago

kangrongji commented 11 months ago

When using sequential colimits from the library, the constructor inl can be hard to align with push during pattern patching, etc. So it doesn't look good. Renaming it to incl and maybe changing the field name space to obj would improve alignment and give a more category-theory-inspired feel. If you all agree, I could make a PR very soon.

felixwellen commented 11 months ago

Not a user of sequential colimits (yet), but this looks like an improvement to me. What do you think about the name Lim→? I consistently forger the traditional math notation it resembles over the years, but maybe that's just me. It is also a lot shorter than SeqColim.

kangrongji commented 11 months ago

Yeah... I think Lim→ looks a bit weird. There is no hurt to use SeqColim instead. I could do all these changes.