Show that the forgetful functor from rings to sets creates limits

JetBrains / arend-lib

Apache License 2.0

79 stars 23 forks source link

Show that the forgetful functor from rings to sets creates limits #42

Open valis opened 2 years ago

valis commented 2 years ago

This is Algebra.Ring.Category/CRingBicat.createsLimits. It is probably better to show that the forgetful functor from any algebraic category to sets creates limits and then transfer this result to rings.