A 2-field structure where we care about equality and other operations should be defined as a sigma-type instead of a structure, this makes definitions like fiber_eq and fiber.sigma_char much easier to prove.
Other examples: ppi, shomotopy, maybe pType. I'm not sure about algebraic structures like Group.
A 2-field structure where we care about equality and other operations should be defined as a sigma-type instead of a structure, this makes definitions like
fiber_eqandfiber.sigma_charmuch easier to prove.Other examples:
ppi,shomotopy, maybepType. I'm not sure about algebraic structures likeGroup.