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 $f : X \to X$ in an allegory is reflexive if $id \le f$.

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 $f \le g$ and $f$ is reflexive, then $g$ is reflexive. reflexive-β€ : f β€ g β is-reflexive f β is-reflexive g reflexive-β€ w f-refl = β€-trans f-refl w  If $f$ is reflexive, then $id \le f \cap f^o$. reflexiveβdiagonal : is-reflexive f β id β€ f β© f β reflexiveβdiagonal f-refl = β©-univ f-refl (reflexive-dual f-refl)  # Symmetric Morphismsπ A morphism $f : X \to X$ is symmetric if $f \le f^o$. 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 $f$ and $g$ is symmetric if $gf \le fg$.

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 $f$ 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 $f : X \to X$ is transitive if $ff \le f$.

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 $f$ and $g$ is transitive if $gf \le fg$.

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 $f$ is transitive, then $(f \cap g)(f \cap h) \le f$.

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 $f$ 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 $f : X \to X$ is cotransitive if $f \le ff$.

Warning

There is another notion of cotransitive relation, which stipulates that for all $x, y, z$, if $R(x,z)$, then either $R(x,y)$ or $R(y,z)$. This is a poor choice of a name, as it is not a transitive relation in $\mathbf{Rel}^{co}$.

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 $f$ and $g$ is cotransitive if $fg \le gf$.

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 $f$ and $g$ is cotransitive, then $f \cap g \le fg$.

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


If $f$ 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 $f$ 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 $f \le g$ and $g$ is coreflexive, then $f$ is coreflexive.

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


If $f$ 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 ($ff \le f$) and cotransitive ($f \le ff$), 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 $ff^o \le id$. In $\mathbf{Rel}$, these are the relations $R \hookrightarrow X \times Y$ such that every $x$ is related to at most one $y$. To see this, note that $RR^o(y,y')$ is defined as $\exists (x : X). R(x,y) \times R(x,y')$. Therefore, $RR^o(y,y') \subseteq y = y'$ means that if there exists any $x$ such that $R(x,y)$ and $R(x,y')$, then $y$ and $y'$ must be equal. Put more plainly, every $x$ is related to at most one $y$!

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 $id \le f^of$. In $\mathbf{Rel}$, these are the relations $R \hookrightarrow X \times Y$ where each $x$ must be related to at least one $y$. To see this, recall that $R^oR(x,x')$ is defined as $\exists (y : Y). R(x,y) \times R(x',y)$. If $x = x' \subseteq R^oR(x,x')$, then we can reduce this statement down to $\forall (x : X). \exists (y : Y). R(x,y)$.

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 $f : X \to Y$ is defined as $id \cap (f^of)$, denoted $\mathrm{dom}(f)$. In $\mathbf{Rel}$, the domain of a relation $R : X \times Y \to \Omega$ is a relation $X \times X \to \Omega$ that relates two elements $x, x' : X$ whenever $x = x'$, and $R(x,y)$ for some $y$.

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 $f : X \to Y$ and $g : X \to X$ such that $g$ is coreflexive. Then $\mathrm{dom}(f) \le g$ if and only if $f \le fg$.

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: $f\mathrm{dom}(f) = f$.

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 $fg$ is contained in the domain of $g$.

domain-β : domain (f β g) β€ domain g
domain-β {f = f} {g = g} =
domain-universall (domain-coreflexive g) $β€-pushr (domain-universalr (domain-coreflexive g) β€-refl)  If $f \le g$, then $\mathrm{dom}(f) \le \mathrm{dom}(g)$. 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: $\mathrm{dom}(f\mathrm{dom}(g)) = \mathrm{dom}(f)\mathrm{dom}(g)$ 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 $\mathrm{dom}(f)\mathrm{dom}(g)$ 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 $f\mathrm{dom}(g) \le (f\mathrm{dom}(g))(\mathrm{dom}(f)\mathrm{dom}(g))$ 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

$\mathrm{dom}(f)\mathrm{dom}(g) \le (f\mathrm{dom}(g))^of\mathrm{dom}(g)$

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 $g$ 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 $f \cap f^o \le id$.

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 $f \le g$ and $g$ is anti-symmetric, then $f$ is anti-symmetric.

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


If $f$ is anti-symmetric and reflexive, then $f \cap f^o = id$.

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 $f$ is coreflexive, then it is anti-symmetric.

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