topos

topos copied to clipboard

Oh no! We have failed to automatically upgrade your project to the latest versions of Lean and its dependencies. If your project currently builds, this is probably because of changes...

github-actions[bot]

This is a roadmap for facts about Kleisli categories, which we should promptly send off to mathlib after proving. - [x] Kleisli category - [x] Kleisli adjunction - [ ]...

Vtec234

Currently it requires all coequalizers to exist, but it suffices to only have reflexive coequalizers

b-mehta

Write a tactic `rewrite_assoc` that performs rewriting mod associativity of composition.

2

Seems like a net win and it doesn't have to be a full-blown monster tactic like tidy.

EdAyers

EdAyers

More fun with the (co)limits API! See over.lean for why we should have this.

b-mehta

[The man, the legend. Let's do it.](https://ncatlab.org/nlab/show/subobject+classifier#johnstones_exercise)

b-mehta

Generalise `limit.lift_self_id` etc to cones.

1

- `limit.lift_self_id` - `pullback.lift_self_id` - `pullback.with_id_l` - `pullback.comp_l` it's a corol of Bhavik's pasting lemma

EdAyers