agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard
verified publisher icon agda

Suggested improvements for `IsPullback`

Open JacquesCarette opened this issue 4 years ago • 4 comments

(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.

JacquesCarette avatar Jan 03 '22 20:01 JacquesCarette

These all seem like great changes!

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

TOTBWF avatar Jan 05 '22 17:01 TOTBWF