1-Cat instance for MatrixCat

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.25k stars 193 forks source link

1-Cat instance for MatrixCat #1991

Closed ThomatoTomato closed 3 months ago

ThomatoTomato commented 3 months ago

Defines a type MatrixCat R that consists of the natural numbers. We turn MatrixCat into a 1-category by considering the homsets (m,n) = M_{m╳n}(R) of m╳n-dimensional matrices.

jdchristensen commented 3 months ago

Merging. Thanks @ThomatoTomato for your contribution! I'll next create a PR about WildCat.Paths that allows us to simplify things here a bit too.