Commit 2023-05-20 10:55 b58077e6
View on Github →feat: port Algebra.Category.ModuleCat.Projective (#3964)
This is stuck at a universe issue. Lean is having trouble merging Type (max (max v u) u v) with Type (max u u v)
See comment below.
feat: port Algebra.Category.ModuleCat.Projective (#3964)
This is stuck at a universe issue. Lean is having trouble merging Type (max (max v u) u v) with Type (max u u v)
See comment below.