Composition operations on binary families of sets

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.
Last modified on 2024-03-01.

module category-theory.composition-operations-on-binary-families-of-sets where
Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

Given a type A, a composition operation on a binary family of sets hom : A → A → Set is a map

  hom y z → hom x y → hom x z

for every triple of elements x y z : A.

For such operations, we can consider properties such as associativity and unitality.

Definitions

Composition operations in binary families of sets

module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A  A  Set l2)
  where

  composition-operation-binary-family-Set : UU (l1  l2)
  composition-operation-binary-family-Set =
    {x y z : A} 
    type-Set (hom-set y z)  type-Set (hom-set x y)  type-Set (hom-set x z)

Associative composition operations in binary families of sets

We give a slightly nonstandard definition of associativity, requiring an associativity witness in each direction. This is of course redundant as inv is a fibered involution on identity types. However, by recording both directions we maintain a definitional double inverse law which is practical in defining the opposite category.

module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A  A  Set l2)
  where

  is-associative-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set  UU (l1  l2)
  is-associative-composition-operation-binary-family-Set comp-hom =
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) 
    ( comp-hom (comp-hom h g) f  comp-hom h (comp-hom g f)) ×
    ( comp-hom h (comp-hom g f)  comp-hom (comp-hom h g) f)

  associative-composition-operation-binary-family-Set : UU (l1  l2)
  associative-composition-operation-binary-family-Set =
    Σ ( composition-operation-binary-family-Set hom-set)
      ( is-associative-composition-operation-binary-family-Set)

module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A  A  Set l2)
  (H : associative-composition-operation-binary-family-Set hom-set)
  where

  comp-hom-associative-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set
  comp-hom-associative-composition-operation-binary-family-Set = pr1 H

  witness-associative-composition-operation-binary-family-Set :
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) 
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( comp-hom-associative-composition-operation-binary-family-Set h g) (f)) 
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( h) (comp-hom-associative-composition-operation-binary-family-Set g f))
  witness-associative-composition-operation-binary-family-Set h g f =
    pr1 (pr2 H h g f)

  inv-witness-associative-composition-operation-binary-family-Set :
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) 
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( h) (comp-hom-associative-composition-operation-binary-family-Set g f)) 
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( comp-hom-associative-composition-operation-binary-family-Set h g) (f))
  inv-witness-associative-composition-operation-binary-family-Set h g f =
    pr2 (pr2 H h g f)
module _
  {l1 l2 : Level} {A : UU l1}
  (hom-set : A  A  Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)
  where

  is-associative-witness-associative-composition-operation-binary-family-Set :
    ( {x y z w : A}
      (h : type-Set (hom-set z w))
      (g : type-Set (hom-set y z))
      (f : type-Set (hom-set x y)) 
      comp-hom (comp-hom h g) f  comp-hom h (comp-hom g f)) 
    is-associative-composition-operation-binary-family-Set hom-set comp-hom
  pr1
    ( is-associative-witness-associative-composition-operation-binary-family-Set
        H h g f) =
    H h g f
  pr2
    ( is-associative-witness-associative-composition-operation-binary-family-Set
        H h g f) =
    inv (H h g f)

  is-associative-inv-witness-associative-composition-operation-binary-family-Set :
    ( {x y z w : A}
      (h : type-Set (hom-set z w))
      (g : type-Set (hom-set y z))
      (f : type-Set (hom-set x y)) 
      comp-hom h (comp-hom g f)  comp-hom (comp-hom h g) f) 
    is-associative-composition-operation-binary-family-Set hom-set comp-hom
  pr1
    ( is-associative-inv-witness-associative-composition-operation-binary-family-Set
        H h g f) =
    inv (H h g f)
  pr2
    ( is-associative-inv-witness-associative-composition-operation-binary-family-Set
        H h g f) =
    H h g f

Unital composition operations in binary families of sets

module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A  A  Set l2)
  where

  is-unital-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set  UU (l1  l2)
  is-unital-composition-operation-binary-family-Set comp-hom =
    Σ ( (x : A)  type-Set (hom-set x x))
      ( λ e 
        ( {x y : A} (f : type-Set (hom-set x y))  comp-hom (e y) f  f) ×
        ( {x y : A} (f : type-Set (hom-set x y))  comp-hom f (e x)  f))

Properties

Being associative is a property of composition operations in binary families of sets

module _
  {l1 l2 : Level} {A : UU l1}
  (hom-set : A  A  Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)
  where
  is-prop-is-associative-composition-operation-binary-family-Set :
    is-prop
      ( is-associative-composition-operation-binary-family-Set hom-set comp-hom)
  is-prop-is-associative-composition-operation-binary-family-Set =
    is-prop-iterated-implicit-Π 4
      ( λ x y z w 
        is-prop-iterated-Π 3
          ( λ h g f 
            is-prop-product
              ( is-set-type-Set
                ( hom-set x w)
                ( comp-hom (comp-hom h g) f)
                ( comp-hom h (comp-hom g f)))
              ( is-set-type-Set
                ( hom-set x w)
                ( comp-hom h (comp-hom g f))
                ( comp-hom (comp-hom h g) f))))

  is-associative-prop-composition-operation-binary-family-Set : Prop (l1  l2)
  pr1 is-associative-prop-composition-operation-binary-family-Set =
    is-associative-composition-operation-binary-family-Set hom-set comp-hom
  pr2 is-associative-prop-composition-operation-binary-family-Set =
    is-prop-is-associative-composition-operation-binary-family-Set

Being unital is a property of composition operations in binary families of sets

Proof: Suppose e e' : (x : A) → hom-set x x are both right and left units with regard to composition. It is enough to show that e = e' since the right and left unit laws are propositions (because all hom-types are sets). By function extensionality, it is enough to show that e x = e' x for all x : A. But by the unit laws we have the following chain of equalities: e x = (e' x) ∘ (e x) = e' x.

module _
  {l1 l2 : Level} {A : UU l1}
  (hom-set : A  A  Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)
  where

  abstract
    all-elements-equal-is-unital-composition-operation-binary-family-Set :
      all-elements-equal
        ( is-unital-composition-operation-binary-family-Set hom-set comp-hom)
    all-elements-equal-is-unital-composition-operation-binary-family-Set
      ( e , left-unit-law-e , right-unit-law-e)
      ( e' , left-unit-law-e' , right-unit-law-e') =
      eq-type-subtype
        ( λ x 
          product-Prop
            ( implicit-Π-Prop A
              ( λ a 
                implicit-Π-Prop A
                ( λ b 
                  Π-Prop
                    ( type-Set (hom-set a b))
                    ( λ f'  Id-Prop (hom-set a b) (comp-hom (x b) f') f'))))
            ( implicit-Π-Prop A
              ( λ a 
                implicit-Π-Prop A
                ( λ b 
                  Π-Prop
                    ( type-Set (hom-set a b))
                    ( λ f'  Id-Prop (hom-set a b) (comp-hom f' (x a)) f')))))
        ( eq-htpy
          ( λ x  inv (left-unit-law-e' (e x))  right-unit-law-e (e' x)))

  abstract
    is-prop-is-unital-composition-operation-binary-family-Set :
      is-prop
        ( is-unital-composition-operation-binary-family-Set hom-set comp-hom)
    is-prop-is-unital-composition-operation-binary-family-Set =
      is-prop-all-elements-equal
        all-elements-equal-is-unital-composition-operation-binary-family-Set

  is-unital-prop-composition-operation-binary-family-Set : Prop (l1  l2)
  pr1 is-unital-prop-composition-operation-binary-family-Set =
    is-unital-composition-operation-binary-family-Set hom-set comp-hom
  pr2 is-unital-prop-composition-operation-binary-family-Set =
    is-prop-is-unital-composition-operation-binary-family-Set

See also

  • Set-magmoids capture the structure of composition operations on binary families of sets.
  • Precategories are associative and unital composition operations on binary families of sets.
  • Nonunital precategories are associative composition operations on binary families of sets.

Recent changes