statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
259 stars 23 forks source link

Pushout and limits #54

Closed marcosh closed 5 years ago

marcosh commented 5 years ago

Hi @FabrizioRomanoGenovese, could you please quickly check if the math of the dual definitions of limits are correct?

FabrizioRomanoGenovese commented 5 years ago

Everything seems correct to me!

marcosh commented 5 years ago

@FabrizioRomanoGenovese thanks!