open import Cat.Allegory.Base
open import Cat.Prelude

import Cat.Allegory.Reasoning
import Cat.Diagram.Idempotent

module Cat.Allegory.Morphism {o β β'} (A : Allegory o β β') where

open Cat.Allegory.Reasoning A public
open Cat.Diagram.Idempotent cat public

private variable
w x y z : Ob
a b c f g h : Hom x y


# Morphisms in an allegoryπ

This module defines a couple of important classes of morphisms that can be found in an allegory.

# Reflexive morphismsπ

A morphism in an allegory is reflexive if

is-reflexive : Hom x x β Type _
is-reflexive f = id β€ f


The composition of two reflexive morphisms is reflexive, and the identity morphism is trivially reflexive.

reflexive-id : is-reflexive (id {x})
reflexive-id = β€-refl

reflexive-β : is-reflexive f β is-reflexive g β is-reflexive (f β g)
reflexive-β {f = f} {g = g} f-refl g-refl =
id      =β¨ sym (idl _) β©=
id β id β€β¨ f-refl β g-refl β©β€
f β g β€β


The intersection of reflexive morphisms is reflexive.

reflexive-β© : is-reflexive f β is-reflexive g β is-reflexive (f β© g)


The dual of a reflexive morphism is also reflexive.

reflexive-dual : is-reflexive f β is-reflexive (f β )
reflexive-dual {f = f} f-refl =
dual-β€α΅£ A $id β =β¨ dual-id A β©= id β€β¨ f-refl β©β€ f β€β  If and is reflexive, then is reflexive. reflexive-β€ : f β€ g β is-reflexive f β is-reflexive g reflexive-β€ w f-refl = β€-trans f-refl w  If is reflexive, then reflexiveβdiagonal : is-reflexive f β id β€ f β© f β reflexiveβdiagonal f-refl = β©-univ f-refl (reflexive-dual f-refl)  # Symmetric morphismsπ A morphism is symmetric if is-symmetric : Hom x x β Type _ is-symmetric f = f β€ f β  The identity morphism is trivially symmetric. symmetric-id : is-symmetric (id {x}) symmetric-id {x = x} = subst (id {x} β€_) (sym$ dual-id A) (β€-refl {f = id {x}})


The composition of symmetric morphisms and is symmetric if

symmetric-β
: is-symmetric f β is-symmetric g
β g β f β€ f β g
β is-symmetric (f β g)
symmetric-β {f = f} {g = g} f-sym g-sym w =
f β g     β€β¨ f-sym β g-sym β©β€
f β  β g β  =β¨ sym dual-β β©=
(g β f) β  β€β¨ dual-β€ w β©β€
(f β g) β  β€β


The dual of a symmetric morphism is symmetric.

symmetric-dual : is-symmetric f β is-symmetric (f β )
symmetric-dual {f = f} f-sym = dual-β€α΅£ A $f β β =β¨ dual f β©= f β€β¨ f-sym β©β€ f β β€β  The intersection of symmetric morphisms is symmetric. symmetric-β© : is-symmetric f β is-symmetric g β is-symmetric (f β© g) symmetric-β© {f = f} {g = g} f-sym g-sym = f β© g β€β¨ β©-pres f-sym g-sym β©β€ f β β© g β =β¨ sym$ dual-β© A β©=


If is symmetric, then it is equal to its dual.

symmetricβself-dual
: is-symmetric f β f β‘ f β
symmetricβself-dual f-sym =
β€-antisym f-sym (dual-β€β A f-sym)


# Transitive morphismsπ

A morphism is transitive if

is-transitive : Hom x x β Type _
is-transitive f = f β f β€ f


The identity morphism is transitive.

transitive-id : is-transitive (id {x})
transitive-id = β€-eliml β€-refl


The composition of two transitive morphisms and is transitive if

transitive-β
: is-transitive f β is-transitive g
β g β f β€ f β g
β is-transitive (f β g)
transitive-β {f = f} {g = g} f-trans g-trans w =
(f β g) β (f β g) β€β¨ β€-extend-inner w β©β€
(f β f) β (g β g)   β€β¨ f-trans β g-trans β©β€
f β g             β€β


A useful little lemma is that if is transitive, then

transitive-β©l : is-transitive f β (f β© g) β (f β© h) β€ f



We can use these lemmas to show that the intersection of transitive morphisms is transitive.

transitive-β©
: is-transitive f β is-transitive g β is-transitive (f β© g)
transitive-β© {f = f} {g = g} f-trans g-trans =


If is transitive, then so is its dual.

transitive-dual : is-transitive f β is-transitive (f β )
transitive-dual {f = f} f-trans =
f β  β f β  =β¨ sym dual-β β©=
(f β f) β  β€β¨ dual-β€ f-trans β©β€
f β        β€β


# Cotransitive morphismsπ

A morphism is cotransitive if

Warning

There is another notion of cotransitive relation, which stipulates that for all if then either or This is a poor choice of a name, as it is not a transitive relation in

Other sources call cotransitive morphisms βsymmetric idempotentsβ, though we avoid this terminology, as cotranstive morphisms are not symmetric.

is-cotransitive : Hom x x β Type _
is-cotransitive f = f β€ f β f


The identity morphism is cotransitive.

cotransitive-id : is-cotransitive (id {x})
cotransitive-id = β€-introl β€-refl


The composition of two cotransitive morphisms and is cotransitive if

cotransitive-β
: is-cotransitive f β is-cotransitive g
β f β g β€ g β f
β is-cotransitive (f β g)
cotransitive-β {f = f} {g = g} f-cotrans g-cotrans w =
f β g             β€β¨ f-cotrans β g-cotrans β©β€
(f β f) β (g β g) β€β¨ β€-extend-inner w β©β€
(f β g) β (f β g) β€β


If the intersection of and is cotransitive, then

cotransitive-β©-β
β f β© g β€ f β g
f β g β€β


If is reflexive, then it is cotransitive.

reflexiveβcotransitive
: is-reflexive f β is-cotransitive f
reflexiveβcotransitive {f = f} f-refl =
f      =β¨ sym (idl f) β©=
id β f β€β¨ f-refl β f β©β€
f β f β€β


If is transitive and symmetric, then it is cotransitive.

transitive+symmetricβcotransitive
: is-transitive f β is-symmetric f β is-cotransitive f
transitive+symmetricβcotransitive {f = f} f-trans f-sym =
f β f β  β f β€β¨ f βΆ dual-β€β A f-sym β f β©β€
f β f β f   β€β¨ f βΆ f-trans β©β€
f β f       β€β


# Coreflexive morphismsπ

is-coreflexive : Hom x x β Type _
is-coreflexive f = f β€ id


The composition of two coreflexive morphisms is coreflexive, and the identity morphism is trivially coreflexive.

coreflexive-β : is-coreflexive f β is-coreflexive g β is-coreflexive (f β g)
coreflexive-β {f = f} {g = g} f-corefl g-corefl =
f β g   β€β¨ f-corefl β g-corefl β©β€
id β id =β¨ idl _ β©=
id      β€β

coreflexive-id : is-coreflexive (id {x})
coreflexive-id = β€-refl


Coreflexive morphisms are closed under intersection.

coreflexive-β©
: β {x} {f g : Hom x x}
β is-coreflexive f β is-coreflexive g β is-coreflexive (f β© g)
coreflexive-β© {f = f} {g = g} f-corefl g-corefl =
id      β€β


Coreflexive morphisms are closed under duals.

coreflexive-dual : is-coreflexive f β is-coreflexive (f β )
coreflexive-dual {f = f} f-corefl = dual-β€β A $f β€β¨ f-corefl β©β€ id =β¨ sym$ dual-id A β©=
id β  β€β


If and is coreflexive, then is coreflexive.

coreflexive-β€ : f β€ g β is-coreflexive g β is-coreflexive f
coreflexive-β€ w g-corefl = β€-trans w g-corefl


If is coreflexive, then it is transitive, cotransitive, and symmetric. Coreflexive morphisms are also anti-symmetric, see coreflexiveβantisymmetric.

coreflexiveβtransitive
: is-coreflexive f β is-transitive f
coreflexiveβtransitive {f = f} f-corefl =
f β f  β€β¨ f-corefl β f β©β€
id β f =β¨ idl _ β©=
f      β€β

coreflexiveβcotransitive
: is-coreflexive f β is-cotransitive f
coreflexiveβcotransitive {f = f} f-corefl =
f β f β  β f β€β¨ f βΆ β€-eliml (coreflexive-dual f-corefl) β©β€
f β f       β€β

coreflexiveβsymmetric
: is-coreflexive f β is-symmetric f
coreflexiveβsymmetric {f = f} f-corefl =
f β f β  β f   β€β¨ f-corefl β β€-refl β f-corefl β©β€
id β f β  β id =β¨ idl _ β idr _ β©=
f β  β€β


As coreflexive morphisms are both transitive ( and cotransitive ( they are idempotent.

coreflexiveβidempotent : is-coreflexive f β is-idempotent f
coreflexiveβidempotent f-corefl =
β€-antisym (coreflexiveβtransitive f-corefl) (coreflexiveβcotransitive f-corefl)


Furthermore, composition of coreflexive morphisms is equivalent to intersection.

coreflexive-β-β©
: β {x} {f g : Hom x x}
β is-coreflexive f β is-coreflexive g
β f β g β‘ f β© g
coreflexive-β-β© {f = f} {g = g} f-corefl g-corefl =
β€-antisym β€-to β€-from
where
β€-to : f β g β€ f β© g
β€-to = β©-univ (β€-elimr g-corefl) (β€-eliml f-corefl)

β€-from : f β© g β€ f β g
β€-from =
cotransitive-β©-β $coreflexiveβcotransitive$


This has a useful corollary: coreflexive morphisms always commute!

coreflexive-comm
: β {x} {f g : Hom x x}
β is-coreflexive f β is-coreflexive g
β f β g β‘ g β f
coreflexive-comm f-corefl g-corefl =


# Functional morphismsπ

A morphism is functional when In these are the relations such that every is related to at most one To see this, note that is defined as Therefore, means that if there exists any such that and then and must be equal. Put more plainly, every is related to at most one

is-functional : Hom x y β Type _
is-functional f = f β f β  β€ id


First, a useful lemma: coreflexive morphisms are always functional.

coreflexiveβfunctional : is-coreflexive f β is-functional f
coreflexiveβfunctional f-corefl =
coreflexive-β f-corefl (coreflexive-dual f-corefl)


This immediately implies that the identity morphism is functional.

functional-id : is-functional (id {x})
functional-id = coreflexiveβfunctional coreflexive-id


Functional morphisms are closed under composition and intersection.

functional-β : is-functional f β is-functional g β is-functional (f β g)
functional-β {f = f} {g = g} f-func g-func =
(f β g) β (f β g) β  β€β¨ β -cancel-inner g-func β©β€
f β f β              β€β¨ f-func β©β€
id                  β€β

functional-β© : is-functional f β is-functional g β is-functional (f β© g)
functional-β© {f = f} {g = g} f-func g-func =
id                                        β€β


# Entire morphismsπ

A morphism is entire when In these are the relations where each must be related to at least one To see this, recall that is defined as If then we can reduce this statement down to

is-entire : Hom x y β Type _
is-entire f = id β€ f β  β f


Reflexive morphisms are always entire.

reflexiveβentire : is-reflexive f β is-entire f
reflexiveβentire f-refl =
reflexive-β (reflexive-dual f-refl) f-refl


From this, we can deduce that the identity morphism is entire.

entire-id : is-entire (id {x})
entire-id = reflexiveβentire reflexive-id


Entire morphisms are closed under composition.

entire-β : is-entire f β is-entire g β is-entire (f β g)
entire-β {f = f} {g = g} f-entire g-entire =
g β  β g             β€β¨ g β  βΆ β€-introl f-entire β©β€
g β  β (f β  β f) β g =β¨ extendl (pulll (sym dual-β)) β©=
(f β g) β  β (f β g) β€β


# Domainsπ

The domain of a morphism is defined as denoted In the domain of a relation is a relation that relates two elements whenever and for some

domain : Hom x y β Hom x x
domain f = id β© f β  β f


The domain of a morphism is always coreflexive.

domain-coreflexive : β (f : Hom x y) β is-coreflexive (domain f)

domain-elimr : f β domain g β€ f
domain-elimr = β€-elimr (domain-coreflexive _)

domain-eliml : domain f β g β€ g
domain-eliml = β€-eliml (domain-coreflexive _)

domain-idempotent : is-idempotent (domain f)
domain-idempotent = coreflexiveβidempotent (domain-coreflexive _)

domain-dual : domain f β  β‘ domain f
domain-dual = sym (symmetricβself-dual (coreflexiveβsymmetric (domain-coreflexive _)))

domain-comm : domain f β domain g β‘ domain g β domain f
domain-comm = coreflexive-comm (domain-coreflexive _) (domain-coreflexive _)


Furthermore, the domain enjoys the following universal property: Let and such that is coreflexive. Then if and only if

domain-universalr : is-coreflexive g β domain f β€ g β f β€ f β g
domain-universalr {g = g} {f = f} g-corefl w =
f β (id β© f β  β f) β€β¨ f βΆ w β©β€
f β g              β€β

domain-universall : is-coreflexive g β f β€ f β g β domain f β€ g
domain-universall {g = g} {f = f} g-corefl w =
((f β  β f) β g) β© id     β€β¨ modular' g (f β  β f) id β©β€
(f β  β f β© id β g β ) β g β€β¨ β€-trans β©-le-r (β€-eliml β€-refl) β g β©β€
g β  β g                  β€β¨ β€-eliml (coreflexive-dual g-corefl) β©β€
g                        β€β


This has a nice corollary:

domain-absorb : β (f : Hom x y) β f β domain f β‘ f
domain-absorb f =
β€-antisym
domain-elimr
(domain-universalr (domain-coreflexive f) β€-refl)


We can nicely characterize the domain of an intersection.

domain-β© : domain (f β© g) β‘ id β© f β  β g
domain-β© {f = f} {g = g} = β€-antisym β€-to β€-from where
β€-to : domain (f β© g) β€ id β© f β  β g
β€-to =

β€-from : id β© f β  β g β€ domain (f β© g)
β€-from =
id β© (f β  β (g β© β f β  β  β id β)) β© id     =β¨ ap! (idr _ β dual f) β©=


Furthermore, the domain of is contained in the domain of

domain-β : domain (f β g) β€ domain g
domain-β {f = f} {g = g} =
domain-universall (domain-coreflexive g) $β€-pushr (domain-universalr (domain-coreflexive g) β€-refl)  If then domain-β€ : f β€ g β domain f β€ domain g domain-β€ w = β©-pres-r (dual-β€ w β w)  The domain of the identity morphism is simply the identity morphism. domain-id : domain (id {x}) β‘ id domain-id = β€-antisym β©-le-l (β©-univ β€-refl (β€-introl symmetric-id))  Characterizing composition of domains is somewhat more difficult, though it is possible. Namely, we shall show the following: domain-smashr : β (f : Hom x z) (g : Hom x y) β domain (f β domain g) β‘ domain f β domain g domain-smashr f g = β€-antisym β€-to β€-from where  We begin by noting that the composition is coreflexive.  fg-corefl : is-coreflexive (domain f β domain g) fg-corefl = coreflexive-β (domain-coreflexive f) (domain-coreflexive g)  To show the forward direction, we can apply the universal property of domains to transform the goal into We can then solve this goal by repeatedly appealing to the fact that domains are coreflexive.  β€-to : domain (f β domain g) β€ domain f β domain g β€-to = domain-universall fg-corefl$
f β domain g                           =Λβ¨ apβ _β_ (domain-absorb f) domain-idempotent β©=Λ
(f β domain f) β (domain g β domain g) =β¨ extendl (extendr domain-comm) β©=
(f β domain g) β (domain f β domain g) β€β


To show the reverse direction, we apply the universal property of the intersection, reducing the goal to

We then solve the goal by an extended series of appeals to the coreflexivity of domains.

  β€-from : domain f β domain g β€ domain (f β domain g)
β€-from = β©-univ fg-corefl $domain f β domain g =Λβ¨ ap (domain f β_) domain-idempotent β©=Λ domain f β domain g β domain g =β¨ extendl domain-comm β©= domain g β domain f β domain g =β¨ ap (_β domain f β domain g) (sym domain-dual) β©= domain g β β domain f β domain g β€β¨ domain g β βΆ β©-le-r β domain g β©β€ domain g β β (f β β f) β domain g =β¨ extendl (pulll (sym dual-β)) β©= (f β domain g) β β f β domain g β€β  We can also characterize postcomposition by a domain, though this is restricted to an inequality in the general case. domain-swapl : β (f : Hom y z) (g : Hom x y) β domain f β g β€ g β domain (f β g) domain-swapl f g = (id β© (f β β f)) β g β€β¨ β©-distribr β©β€ (id β g β© (f β β f) β g) =β¨ apβ _β©_ id-comm-sym (sym (assoc (f β ) f g)) β©= (g β id β© f β β f β g) β€β¨ modular id g (f β β f β g) β©β€ g β (id β© β g β β f β β f β g β) =β¨ ap! (pulll (sym dual-β)) β©= g β (id β© (f β g) β β (f β g)) β€β  We can strengthen this to an equality when is functional. domain-swap : β (f : Hom y z) (g : Hom x y) β is-functional g β domain f β g β‘ g β domain (f β g) domain-swap f g w = β€-antisym (domain-swapl f g)$
g β id β© g β (f β g) β  β (f β g) β€β¨ β©-pres-r (β€-extendl (β -pulll w)) β©β€
g β id β© id β f β  β f β g        =β¨ apβ _β©_ id-comm (idl _) β©=
id β g β© f β  β f β g             β€β¨ modular' g id (f β  β f β g) β©β€
(id β© (f β  β f β g) β g β ) β g   β€β¨ β©-pres-r (β€-pullr (β€-cancelr w)) β g β©β€
(id β© f β  β f) β g β€β


We also note that domains are always functional.

domain-functional : (f : Hom x y) β is-functional (domain f)
domain-functional f = coreflexiveβfunctional (domain-coreflexive f)


The domain of an entire morphism is the identity.

domain-entire : is-entire f β domain f β‘ id
domain-entire f-entire =
β€-antisym
(domain-coreflexive _)


# Antisymmetric morphismsπ

A morphism is anti-symmetric if

is-antisymmetric : Hom x x β Type _
is-antisymmetric f = f β© f β  β€ id


Identity morphisms are anti-symmetric.

antisymmetric-id
: is-antisymmetric (id {x})
antisymmetric-id =
id            β€β


If and is anti-symmetric, then is anti-symmetric.

antisymmetric-β€
: f β€ g β is-antisymmetric g β is-antisymmetric f
antisymmetric-β€ {f = f} {g = g} w g-antisym =
id      β€β


If is anti-symmetric and reflexive, then

reflexive+antisymmetricβdiagonal
: is-reflexive f β is-antisymmetric f β f β© f β  β‘ id
reflexive+antisymmetricβdiagonal f-refl f-antisym =
β€-antisym f-antisym (reflexiveβdiagonal f-refl)


If is coreflexive, then it is anti-symmetric.

coreflexiveβantisymmetric : is-coreflexive f β is-antisymmetric f
coreflexiveβantisymmetric {f = f} f-corefl =