Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to an adjunction.

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory

https://arxiv.org/abs/1611.02108

MIT License

571 stars 76 forks source link

Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to an adjunction. #56

Closed linuborj closed 7 years ago

linuborj commented 7 years ago

Added definitions of algebraic structures in algstruct.ctt, a formalisation of the Grothendieck group in grothendieck.cct, definitions of natural transformations, universal arrows, and adjunctions in univprop as well as a proof that a family of universal arrows gives rise to an adjunction.

mortberg commented 7 years ago

Good! Did you change the error in the other PR that you commented on?

linuborj commented 7 years ago

Yep.