Thomas Wilskow Thorbjørnsen

icon company University of Western Ontario icon location You may say Tomato-Tomatoe, but I say Thomato-Tomato.

Results 2 comments of Thomas Wilskow Thorbjørnsen

switch to Int in cring_Z

I added a small lemma that I think can be useful in the future. This lemma also has an accompanying lemma that I do not think belong to this file,...

biproducts

(2) has now been completed. In the first commit we add a result that let us transfer (co)product structures along equivalences in a category. Typeclass search tricks itself into looking...