module Cat.Allegory.Morphism {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where

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→Xf : X \to X in an allegory is reflexive if id≤fid \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)
reflexive-∩ f-refl g-refl = ∩-univ f-refl g-refl

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≤gf \le g and ff is reflexive, then gg is reflexive.

reflexive-≤ : f ≤ g → is-reflexive f → is-reflexive g
reflexive-≤ w f-refl = ≤-trans f-refl w

If ff is reflexive, then id≤f∩foid \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→Xf : X \to X is symmetric if f≤fof \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 ff and gg is symmetric if gf≤fggf \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 ⟩=
  (f ∩ g) † ≤∎

If ff 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→Xf : X \to X is transitive if ff≤fff \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 ff and gg is transitive if gf≤fggf \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 ff is transitive, then (f∩g)(f∩h)≤f(f \cap g)(f \cap h) \le f.

transitive-∩l : is-transitive f → (f ∩ g) ∘ (f ∩ h) ≤ f
transitive-∩l f-trans = ≤-trans (∩-le-l ◆ ∩-le-l) f-trans

transitive-∩r : is-transitive h → (f ∩ h) ∘ (g ∩ h) ≤ h
transitive-∩r h-trans = ≤-trans (∩-le-r ◆ ∩-le-r) h-trans

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 =
  ∩-univ (transitive-∩l f-trans) (transitive-∩r g-trans)

If ff 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→Xf : X \to X is cotransitive if f≤fff \le ff.

\ Warning

There is another notion of cotransitive relation, which stipulates that for all x,y,zx, y, z, if R(x,z)R(x,z), then either R(x,y)R(x,y) or R(y,z)R(y,z). This is a poor choice of a name, as it is not a transitive relation in Relco\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 ff and gg is cotransitive if fg≤gffg \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 ff and gg is cotransitive, then f∩g≤fgf \cap g \le fg.

cotransitive-∩-∘
  : is-cotransitive (f ∩ g)
  → f ∩ g ≤ f ∘ g
cotransitive-∩-∘ {f = f} {g = g} f∩g-cotrans =
  f ∩ g             ≤⟨ f∩g-cotrans ⟩≤
  (f ∩ g) ∘ (f ∩ g) ≤⟨ ∩-le-l ◆ ∩-le-r ⟩≤
  f ∘ g ≤∎

If ff 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 ff 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           ≤⟨ ≤-conj f ⟩≤
  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 =
  f ∩ g   ≤⟨ ∩-pres f-corefl g-corefl ⟩≤
  id ∩ id =⟨ ∩-idempotent ⟩=
  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≤gf \le g and gg is coreflexive, then ff is coreflexive.

coreflexive-≤ : f ≤ g → is-coreflexive g → is-coreflexive f
coreflexive-≤ w g-corefl = ≤-trans w g-corefl

If ff 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           ≤⟨ ≤-conj f ⟩≤
  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             ≤⟨ ≤-conj f ⟩≤
  f ∘ f † ∘ f   ≤⟨ f-corefl ◆ ≤-refl ◆ f-corefl ⟩≤
  id ∘ f † ∘ id =⟨ idl _ ∙ idr _ ⟩=
  f † ≤∎

As coreflexive morphisms are both transitive (ff≤fff \le f) and cotransitive (f≤fff \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 $
      coreflexive-∩ f-corefl g-corefl

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 =
  coreflexive-∘-∩ f-corefl g-corefl
  ·· ∩-comm
  ·· sym (coreflexive-∘-∩ g-corefl f-corefl)

Functional Morphisms🔗

A morphism $$ is functional when ffo≤idff^o \le id. In Rel\mathbf{Rel}, these are the relations R↪X×YR \hookrightarrow X \times Y such that every xx is related to at most one yy. To see this, note that RRo(y,y′)RR^o(y,y') is defined as ∃(x:X).R(x,y)×R(x,y′)\exists (x : X). R(x,y) \times R(x,y'). Therefore, RRo(y,y′)⊆y=y′RR^o(y,y') \subseteq y = y' means that if there exists any xx such that R(x,y)R(x,y) and R(x,y′)R(x,y'), then yy and y′y' must be equal. Put more plainly, every xx is related to at most one yy!

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 =
  (f ∩ g) ∘ (f ∩ g) †                       =⟨ ap ((f ∩ g) ∘_) (dual-∩ A) ⟩=
  (f ∩ g) ∘ (f † ∩ g †)                     ≤⟨ ∩-distrib ⟩≤
  (f ∘ f † ∩ g ∘ f †) ∩ (f ∘ g † ∩ g ∘ g †) ≤⟨ ∩-pres ∩-le-l ∩-le-r ⟩≤
  f ∘ f † ∩ g ∘ g †                         ≤⟨ ∩-pres f-func g-func ⟩≤
  id ∩ id                                   =⟨ ∩-idempotent ⟩=
  id                                        ≤∎

Entire Morphisms🔗

A morphism is entire when id≤fofid \le f^of. In Rel\mathbf{Rel}, these are the relations R↪X×YR \hookrightarrow X \times Y where each xx must be related to at least one yy. To see this, recall that RoR(x,x′)R^oR(x,x') is defined as ∃(y:Y).R(x,y)×R(x′,y)\exists (y : Y). R(x,y) \times R(x',y). If x=x′⊆RoR(x,x′)x = x' \subseteq R^oR(x,x'), then we can reduce this statement down to ∀(x:X).∃(y:Y).R(x,y)\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 =
  id                  ≤⟨ 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→Yf : X \to Y is defined as id∩(fof)id \cap (f^of), denoted dom(f)\mathrm{dom}(f). In Rel\mathbf{Rel}, the domain of a relation R:X×Y→ΩR : X \times Y \to \Omega is a relation X×X→ΩX \times X \to \Omega that relates two elements x,x′:Xx, x' : X whenever x=x′x = x', and R(x,y)R(x,y) for some yy.

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-coreflexive f = ∩-le-l

Furthermore, the domain enjoys the following universal property: Let f:X→Yf : X \to Y and g:X→Xg : X \to X such that gg is coreflexive. Then dom(f)≤g\mathrm{dom}(f) \le g if and only if f≤fgf \le fg.

domain-universalr : is-coreflexive g → domain f ≤ g → f ≤ f ∘ g
domain-universalr {g = g} {f = f} g-corefl w =
  f                  ≤⟨ ∩-univ (≤-intror ≤-refl) ≤-refl ⟩≤
  (f ∘ id) ∩ f       ≤⟨ modular id f f ⟩≤
  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 =
  id ∩ (f † ∘ f)           ≤⟨ ∩-pres-r (≤-pushr w) ⟩≤
  id ∩ ((f † ∘ f) ∘ g)     =⟨ ∩-comm ⟩=
  ((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: fdom(f)=ff\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 =
    ∩-univ
      (domain-coreflexive (f ∩ g))
      (≤-trans ∩-le-r (dual-≤ ∩-le-l ◆ ∩-le-r))

  ≤-from : id ∩ f † ∘ g ≤ domain (f ∩ g)
  ≤-from =
    id ∩ f † ∘ g                               ≤⟨ ∩-univ ∩-le-l (∩-univ (∩-univ ∩-le-r ∩-le-l) ∩-le-l ) ⟩≤
    id ∩ (f † ∘ g ∩ id) ∩ id                   ≤⟨ ∩-pres-r (∩-pres-l (modular g (f †) id)) ⟩≤
    id ∩ (f † ∘ (g ∩ ⌜ f † † ∘ id ⌝)) ∩ id     =⟨ ap! (idr _ ∙ dual f) ⟩=
    id ∩ (f † ∘ (g ∩ f)) ∩ id                  ≤⟨ ∩-pres-r (modular′ (g ∩ f) (f †) id) ⟩≤
    id ∩ (f † ∩ ⌜ id ∘ (g ∩ f) † ⌝) ∘ (g ∩ f)  =⟨ ap! (idl _) ⟩=
    id ∩ (f † ∩ ⌜ g ∩ f ⌝ †) ∘ ⌜ g ∩ f ⌝       =⟨ ap! ∩-comm ⟩=
    id ∩ (f † ∩ (f ∩ g) †) ∘ (f ∩ g)           ≤⟨ ∩-pres-r (∩-le-r ◀ (f ∩ g)) ⟩≤
    id ∩ (f ∩ g) † ∘ (f ∩ g)                   ≤∎

Furthermore, the domain of fgfg is contained in the domain of gg.

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≤gf \le g, then dom(f)≤dom(g)\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:

dom(fdom(g))=dom(f)dom(g)\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 dom(f)dom(g)\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

fdom(g)≤(fdom(g))(dom(f)dom(g))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

dom(f)dom(g)≤(fdom(g))ofdom(g)\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 gg 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 ∩ (f ∘ g) † ∘ (f ∘ g))   ≤⟨ ∩-distribl ⟩≤
  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 _)
    (∩-univ ≤-refl f-entire)

Antisymmetric Morphisms🔗

A morphism is anti-symmetric if f∩fo≤idf \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 ∩ ⌜ id † ⌝ =⟨ ap! (dual-id A) ⟩=
  id ∩ id       =⟨ ∩-idempotent ⟩=
  id            ≤∎

If f≤gf \le g and gg is anti-symmetric, then ff is anti-symmetric.

antisymmetric-≤
  : f ≤ g → is-antisymmetric g → is-antisymmetric f
antisymmetric-≤ {f = f} {g = g} w g-antisym =
  f ∩ f † ≤⟨ ∩-pres w (dual-≤ w) ⟩≤
  g ∩ g † ≤⟨ g-antisym ⟩≤
  id      ≤∎

If ff is anti-symmetric and reflexive, then f∩fo=idf \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 ff is coreflexive, then it is anti-symmetric.

coreflexive→antisymmetric : is-coreflexive f → is-antisymmetric f
coreflexive→antisymmetric {f = f} f-corefl =
  f ∩ f † ≤⟨ ∩-pres f-corefl (coreflexive-dual f-corefl) ⟩≤
  id ∩ id =⟨ ∩-idempotent ⟩=
  id ≤∎