search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Suggested improvements for `IsPullback` #334

Open JacquesCarette opened 2 years ago

JacquesCarette commented 2 years ago

(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 commented 2 years ago

These all seem like great changes!

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

jacquescomeaux commented 3 weeks ago

This seems pretty straightforward. Are these changes still wanted?

sergey-goncharov commented 3 weeks ago

This seems pretty straightforward. Are these changes still wanted?

I think so.

JacquesCarette commented 3 weeks ago

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