Satisfying the inhabited linter

Composition of morphisms in the indexing diagram for (co)equalizers.

The functor walking_parallel_pair ⥤ walking_parallel_pairᵒᵖ sending left to left and right to right.

The equivalence walking_parallel_pair ⥤ walking_parallel_pairᵒᵖ sending left to left and right to right.

parallel_pair f g is the diagram in C consisting of the two morphisms f and g with common domain and codomain.

Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a parallel_pair

Construct a morphism between parallel pairs.

Construct a natural isomorphism between functors out of the walking parallel pair from its components.

Construct a natural isomorphism between parallel_pair f g and parallel_pair f' g' given equalities f = f' and g = g'.

A fork on f and g is just a cone (parallel_pair f g).

A cofork on f and g is just a cocone (parallel_pair f g).

A fork t on the parallel pair f g : X ⟶ Y consists of two morphisms t.π.app zero : t.X ⟶ X and t.π.app one : t.X ⟶ Y. Of these, only the first one is interesting, and we give it the shorter name fork.ι t.

A cofork t on the parallel_pair f g : X ⟶ Y consists of two morphisms t.ι.app zero : X ⟶ t.X and t.ι.app one : Y ⟶ t.X. Of these, only the second one is interesting, and we give it the shorter name cofork.π t.

A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.

A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying f ≫ π = g ≫ π.

If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.X such that l ≫ fork.ι s = k.

If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.X ⟶ W such that cofork.π s ≫ l = k.

This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

This is a slightly more convenient method to verify that a cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

Given a limit cone for the pair f g : X ⟶ Y, for any Z, morphisms from Z to its point are in bijection with morphisms h : Z ⟶ X such that h ≫ f = h ≫ g. Further, this bijection is natural in Z: see fork.is_limit.hom_iso_natural. This is a special case of is_limit.hom_iso', often useful to construct adjunctions.

Given a colimit cocone for the pair f g : X ⟶ Y, for any Z, morphisms from the cocone point to Z are in bijection with morphisms h : Y ⟶ Z such that f ≫ h = g ≫ h. Further, this bijection is natural in Z: see cofork.is_colimit.hom_iso_natural. This is a special case of is_colimit.hom_iso', often useful to construct adjunctions.

This is a helper construction that can be useful when verifying that a category has all equalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right), and a fork on F.map left and F.map right, we get a cone on F.

If you're thinking about using this, have a look at has_equalizers_of_has_limit_parallel_pair, which you may find to be an easier way of achieving your goal.

This is a helper construction that can be useful when verifying that a category has all coequalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right), and a cofork on F.map left and F.map right, we get a cocone on F.

If you're thinking about using this, have a look at has_coequalizers_of_has_colimit_parallel_pair, which you may find to be an easier way of achieving your goal.

Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right) and a cone on F, we get a fork on F.map left and F.map right.

Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right) and a cocone on F, we get a cofork on F.map left and F.map right.

Helper function for constructing morphisms between equalizer forks.

To construct an isomorphism between forks, it suffices to give an isomorphism between the cone points and check that it commutes with the ι morphisms.

Every fork is isomorphic to one of the form fork.of_ι _ _.

Helper function for constructing morphisms between coequalizer coforks.

To construct an isomorphism between coforks, it suffices to give an isomorphism between the cocone points and check that it commutes with the π morphisms.

Every cofork is isomorphic to one of the form cofork.of_π _ _.

has_equalizer f g represents a particular choice of limiting cone for the parallel pair of morphisms f and g.

An equalizer morphism is a monomorphism

The identity determines a cone on the equalizer diagram of f and g if f = g.

The identity on X is an equalizer of (f, g), if f = g.