Satisfying the inhabited linter

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

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

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 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 ≫ π.

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.

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

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

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.

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.

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

If an equalizer of f and g exists, we can access an arbitrary choice of such by saying equalizer f g.

If an equalizer of f and g exists, we can access the inclusion equalizer f g ⟶ X by saying equalizer.ι f g.

An equalizer cone for a parallel pair f and g.

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the equalizer of f and g via equalizer.lift : W ⟶ equalizer f g.

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ equalizer f g satisfying l ≫ equalizer.ι f g = k.

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.

Every equalizer of (f, g), where f = g, is an isomorphism.

The equalizer of (f, g), where f = g, is an isomorphism.

Every equalizer of (f, f) is an isomorphism.

An equalizer that is an epimorphism is an isomorphism.

The equalizer inclusion for (f, f) is an isomorphism.

The equalizer of a morphism with itself is isomorphic to the source.

Helper function for constructing morphisms between coequalizer coforks.

has_coequalizer f g represents a particular choice of colimiting cocone for the parallel pair of morphisms f and g.

If a coequalizer of f and g exists, we can access an arbitrary choice of such by saying coequalizer f g.

If a coequalizer of f and g exists, we can access the corresponding projection by saying coequalizer.π f g.

An arbitrary choice of coequalizer cocone for a parallel pair f and g.

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k factors through the coequalizer of f and g via coequalizer.desc : coequalizer f g ⟶ W.

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.

A coequalizer morphism is an epimorphism

The identity determines a cocone on the coequalizer diagram of f and g, if f = g.

The identity on Y is a coequalizer of (f, g), where f = g.

Every coequalizer of (f, g), where f = g, is an isomorphism.

The coequalizer of (f, g), where f = g, is an isomorphism.

Every coequalizer of (f, f) is an isomorphism.

A coequalizer that is a monomorphism is an isomorphism.

The coequalizer projection for (f, f) is an isomorphism.

The coequalizer of a morphism with itself is isomorphic to the target.

has_equalizers represents a choice of equalizer for every pair of morphisms

has_coequalizers represents a choice of coequalizer for every pair of morphisms

A split mono f equalizes (retraction f ≫ f) and (𝟙 Y). Here we build the cone, and show in split_mono_equalizes that it is a limit cone.

A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).

A split epi f coequalizes (f ≫ section_ f) and (𝟙 X). Here we build the cocone, and show in split_epi_coequalizes that it is a colimit cocone.

A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).