{P : Sort u_1} →
  {carrier : Type u} →
    {booleanRing : BooleanRing carrier} →
      {carrier' : Type u} →
        {booleanRing' : BooleanRing carrier'} →
          { carrier := carrier, booleanRing := booleanRing } = { carrier := carrier', booleanRing := booleanRing' } →
            (carrier = carrier' → booleanRing ≍ booleanRing' → P) → P