Commit 2023-08-28 12:46 7c2f3841

feat: generalize sheaf condition to only the relevant pullbacks existing (#6750) We define a predicate Presieve.hasPullbacks which says that the pullback of every pair of arrows in the presieve exists. This allows to generalize Equalizer.Presieve.sheaf_condition to categories that don't necessarily have all pullbacks (such as Stonean).