Skip to content

TOTBWF/cubical-categories

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 

Repository files navigation

Cubical Categories

This library formalizes Category Theory inside of Cubical Agda. This lets us avoid issues of morphism equality, and hopefully lets us implement things like strict categories is a much easier way.

Origins

This library was born out of https://github.com/agda/agda-categories, and takes quite a bit of inspiration from it.

About

Category theory formalized in cubical agda

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages