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 β‰€βˆŽ