The representing arrow category

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-26.
Last modified on 2024-04-11.

module category-theory.representing-arrow-category where
Imports 
open import category-theory.categories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.booleans
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.unit-type
open import foundation.universe-levels

Idea

The representing arrow is the category that represents arrows in a (pre-)category. We model it after implication on the booleans.

Definition

The objects and hom-sets of the representing arrow

obj-representing-arrow-Category : UU lzero
obj-representing-arrow-Category = bool

hom-set-representing-arrow-Category :
  obj-representing-arrow-Category → obj-representing-arrow-Category → Set lzero
hom-set-representing-arrow-Category true true = unit-Set
hom-set-representing-arrow-Category true false = empty-Set
hom-set-representing-arrow-Category false _ = unit-Set

hom-representing-arrow-Category :
  obj-representing-arrow-Category → obj-representing-arrow-Category → UU lzero
hom-representing-arrow-Category x y =
  type-Set (hom-set-representing-arrow-Category x y)

The underlying precategory of the representing arrow

comp-hom-representing-arrow-Category :
  {x y z : obj-representing-arrow-Category} →
  hom-representing-arrow-Category y z →
  hom-representing-arrow-Category x y →
  hom-representing-arrow-Category x z
comp-hom-representing-arrow-Category {true} {true} {true} _ _ = star
comp-hom-representing-arrow-Category {false} _ _ = star

associative-comp-hom-representing-arrow-Category :
  {x y z w : obj-representing-arrow-Category} →
  (h : hom-representing-arrow-Category z w)
  (g : hom-representing-arrow-Category y z)
  (f : hom-representing-arrow-Category x y) →
  ( comp-hom-representing-arrow-Category
    { x} (comp-hom-representing-arrow-Category {y} h g) f) ＝
  ( comp-hom-representing-arrow-Category
    { x} h (comp-hom-representing-arrow-Category {x} g f))
associative-comp-hom-representing-arrow-Category
  { true} {true} {true} {true} h g f =
  refl
associative-comp-hom-representing-arrow-Category {false} h g f = refl

id-hom-representing-arrow-Category :
  {x : obj-representing-arrow-Category} → hom-representing-arrow-Category x x
id-hom-representing-arrow-Category {true} = star
id-hom-representing-arrow-Category {false} = star

left-unit-law-comp-hom-representing-arrow-Category :
  {x y : obj-representing-arrow-Category} →
  (f : hom-representing-arrow-Category x y) →
  comp-hom-representing-arrow-Category
    { x} (id-hom-representing-arrow-Category {y}) f ＝
  f
left-unit-law-comp-hom-representing-arrow-Category {true} {true} f = refl
left-unit-law-comp-hom-representing-arrow-Category {false} f = refl

right-unit-law-comp-hom-representing-arrow-Category :
  {x y : obj-representing-arrow-Category} →
  (f : hom-representing-arrow-Category x y) →
  comp-hom-representing-arrow-Category
    { x} f (id-hom-representing-arrow-Category {x}) ＝
  f
right-unit-law-comp-hom-representing-arrow-Category {true} {true} f = refl
right-unit-law-comp-hom-representing-arrow-Category {false} f = refl

representing-arrow-Precategory : Precategory lzero lzero
representing-arrow-Precategory =
  make-Precategory
    ( obj-representing-arrow-Category)
    ( hom-set-representing-arrow-Category)
    ( λ {x} {y} {z} → comp-hom-representing-arrow-Category {x} {y} {z})
    ( λ x → id-hom-representing-arrow-Category {x})
    ( λ {x} {y} {z} {w} →
      associative-comp-hom-representing-arrow-Category {x} {y} {z} {w})
    ( λ {x} {y} → left-unit-law-comp-hom-representing-arrow-Category {x} {y})
    ( λ {x} {y} → right-unit-law-comp-hom-representing-arrow-Category {x} {y})

The representing arrow category

is-category-representing-arrow-Category :
  is-category-Precategory representing-arrow-Precategory
is-category-representing-arrow-Category true true =
    is-equiv-has-converse-is-prop
    ( is-set-bool true true)
    ( is-prop-type-subtype
      ( is-iso-prop-Precategory representing-arrow-Precategory {true} {true})
      ( is-prop-unit))
    ( λ _ → refl)
is-category-representing-arrow-Category true false =
  is-equiv-is-empty
    ( iso-eq-Precategory representing-arrow-Precategory true false)
    ( hom-iso-Precategory representing-arrow-Precategory)
is-category-representing-arrow-Category false true =
  is-equiv-is-empty
    ( iso-eq-Precategory representing-arrow-Precategory false true)
    ( hom-inv-iso-Precategory representing-arrow-Precategory)
is-category-representing-arrow-Category false false =
  is-equiv-has-converse-is-prop
    ( is-set-bool false false)
    ( is-prop-type-subtype
      ( is-iso-prop-Precategory representing-arrow-Precategory {false} {false})
      ( is-prop-unit))
    ( λ _ → refl)

representing-arrow-Category : Category lzero lzero
pr1 representing-arrow-Category = representing-arrow-Precategory
pr2 representing-arrow-Category = is-category-representing-arrow-Category

Properties

The representing arrow represents arrows in a category

This remains to be formalized.

A wikidata identifier was not available for this concept.

Recent changes