Suggested improvements for IsPullback

[JacquesCarette]

(from @sergey-goncharov ):
I would suggest:

1. move the "unique" field to the bottom. It is the most sophisticated property, and must logically be
   the last one (this should more generally be taken as a rule for all limits and colimits).

2. I suggest to replace 'unique' with what is currently derived as 'unique-diagram'. This would make
   everything symmetric, and I would expect, in most cases, it would be easier to prove that something is a
   pullback.

As a bonus, uniqueness will no longer depend on 'eq : f ∘ h₁ ≈ g ∘ h₂', which is really not needed for
it, but which gets in way.

[TOTBWF]

These all seem like great changes!

When we do this, we should probably update Pushout as well.

[jacquescomeaux]

This seems pretty straightforward. Are these changes still wanted?

[sergey-goncharov]

This seems pretty straightforward. Are these changes still wanted?

I think so.

[JacquesCarette]

Some low-hanging fruit just need people with spare cycles!