One may decompose a ring equation a = b :> R * R' into fst a = fst b :> R and snd a = snd b :> R'. Thanks to the support for morphisms, it would be possible to push these fst and snd down. But then, I have no idea how to simplify expressions like fst (_, _) properly.
One may decompose a ring equation
a = b :> R * R'intofst a = fst b :> Randsnd a = snd b :> R'. Thanks to the support for morphisms, it would be possible to push thesefstandsnddown. But then, I have no idea how to simplify expressions likefst (_, _)properly.