Indiscrete precategories

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-27.

module category-theory.indiscrete-precategories where
Imports
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.fully-faithful-functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories
open import category-theory.pregroupoids
open import category-theory.preunivalent-categories
open import category-theory.strict-categories
open import category-theory.subterminal-precategories
open import category-theory.terminal-category

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.unit-type
open import foundation.universe-levels

Idea

Given a type X, we can define its associated indiscrete precategory as the precategory whose hom-sets are contractible everywhere.

This construction demonstrates one essential aspect about precategories: While it displays obj-Precategory as a retraction, every indiscrete precategory is subterminal.

Definitions

The indiscrete precategory associated to a type

The objects and hom-sets of the indiscrete precategory associated to a type

module _
  {l : Level} (X : UU l)
  where

  obj-indiscrete-Precategory : UU l
  obj-indiscrete-Precategory = X

  hom-set-indiscrete-Precategory :
    obj-indiscrete-Precategory  obj-indiscrete-Precategory  Set lzero
  hom-set-indiscrete-Precategory _ _ = unit-Set

  hom-indiscrete-Precategory :
    obj-indiscrete-Precategory  obj-indiscrete-Precategory  UU lzero
  hom-indiscrete-Precategory x y = type-Set (hom-set-indiscrete-Precategory x y)

The precategory structure of the indiscrete precategory associated to a type

module _
  {l : Level} (X : UU l)
  where

  comp-hom-indiscrete-Precategory :
    {x y z : obj-indiscrete-Precategory X} 
    hom-indiscrete-Precategory X y z 
    hom-indiscrete-Precategory X x y 
    hom-indiscrete-Precategory X x z
  comp-hom-indiscrete-Precategory _ _ = star

  associative-comp-hom-indiscrete-Precategory :
    {x y z w : obj-indiscrete-Precategory X} 
    (h : hom-indiscrete-Precategory X z w)
    (g : hom-indiscrete-Precategory X y z)
    (f : hom-indiscrete-Precategory X x y) 
    comp-hom-indiscrete-Precategory {x} {y} {w}
      ( comp-hom-indiscrete-Precategory {y} {z} {w} h g)
      ( f) 
    comp-hom-indiscrete-Precategory {x} {z} {w}
      ( h)
      ( comp-hom-indiscrete-Precategory {x} {y} {z} g f)
  associative-comp-hom-indiscrete-Precategory h g f = refl

  inv-associative-comp-hom-indiscrete-Precategory :
    {x y z w : obj-indiscrete-Precategory X} 
    (h : hom-indiscrete-Precategory X z w)
    (g : hom-indiscrete-Precategory X y z)
    (f : hom-indiscrete-Precategory X x y) 
    comp-hom-indiscrete-Precategory {x} {z} {w}
      ( h)
      ( comp-hom-indiscrete-Precategory {x} {y} {z} g f) 
    comp-hom-indiscrete-Precategory {x} {y} {w}
      ( comp-hom-indiscrete-Precategory {y} {z} {w} h g)
      ( f)
  inv-associative-comp-hom-indiscrete-Precategory h g f = refl

  associative-composition-operation-indiscrete-Precategory :
    associative-composition-operation-binary-family-Set
      ( hom-set-indiscrete-Precategory X)
  pr1 associative-composition-operation-indiscrete-Precategory {x} {y} {z} =
    comp-hom-indiscrete-Precategory {x} {y} {z}
  pr1
    ( pr2
        associative-composition-operation-indiscrete-Precategory
          { x} {y} {z} {w} h g f) =
    associative-comp-hom-indiscrete-Precategory {x} {y} {z} {w} h g f
  pr2
    ( pr2
        associative-composition-operation-indiscrete-Precategory
          { x} {y} {z} {w} h g f) =
    inv-associative-comp-hom-indiscrete-Precategory {x} {y} {z} {w} h g f

  id-hom-indiscrete-Precategory :
    {x : obj-indiscrete-Precategory X}  hom-indiscrete-Precategory X x x
  id-hom-indiscrete-Precategory = star

  left-unit-law-comp-hom-indiscrete-Precategory :
    {x y : obj-indiscrete-Precategory X} 
    (f : hom-indiscrete-Precategory X x y) 
    comp-hom-indiscrete-Precategory {x} {y} {y}
      ( id-hom-indiscrete-Precategory {y})
      ( f) 
    f
  left-unit-law-comp-hom-indiscrete-Precategory f = refl

  right-unit-law-comp-hom-indiscrete-Precategory :
    {x y : obj-indiscrete-Precategory X} 
    (f : hom-indiscrete-Precategory X x y) 
    comp-hom-indiscrete-Precategory {x} {x} {y}
      ( f)
      ( id-hom-indiscrete-Precategory {x}) 
    f
  right-unit-law-comp-hom-indiscrete-Precategory f = refl

  is-unital-composition-operation-indiscrete-Precategory :
    is-unital-composition-operation-binary-family-Set
      ( hom-set-indiscrete-Precategory X)
      ( λ {x} {y} {z}  comp-hom-indiscrete-Precategory {x} {y} {z})
  pr1 is-unital-composition-operation-indiscrete-Precategory x =
    id-hom-indiscrete-Precategory {x}
  pr1 (pr2 is-unital-composition-operation-indiscrete-Precategory) {x} {y} =
    left-unit-law-comp-hom-indiscrete-Precategory {x} {y}
  pr2 (pr2 is-unital-composition-operation-indiscrete-Precategory) {x} {y} =
    right-unit-law-comp-hom-indiscrete-Precategory {x} {y}

  indiscrete-Precategory : Precategory l lzero
  pr1 indiscrete-Precategory = obj-indiscrete-Precategory X
  pr1 (pr2 indiscrete-Precategory) = hom-set-indiscrete-Precategory X
  pr1 (pr2 (pr2 indiscrete-Precategory)) =
    associative-composition-operation-indiscrete-Precategory
  pr2 (pr2 (pr2 indiscrete-Precategory)) =
    is-unital-composition-operation-indiscrete-Precategory

The pregroupoid structure of the indiscrete precategory associated to a type

module _
  {l : Level} (X : UU l)
  where

  is-iso-hom-indiscrete-Precategory :
    {x y : obj-indiscrete-Precategory X}
    (f : hom-indiscrete-Precategory X x y) 
    is-iso-Precategory (indiscrete-Precategory X) {x} {y} f
  pr1 (is-iso-hom-indiscrete-Precategory _) = star
  pr1 (pr2 (is-iso-hom-indiscrete-Precategory _)) = refl
  pr2 (pr2 (is-iso-hom-indiscrete-Precategory _)) = refl

  iso-obj-indiscrete-Precategory :
    (x y : obj-indiscrete-Precategory X) 
    iso-Precategory (indiscrete-Precategory X) x y
  pr1 (iso-obj-indiscrete-Precategory x y) = star
  pr2 (iso-obj-indiscrete-Precategory x y) =
    is-iso-hom-indiscrete-Precategory {x} {y} star

  is-pregroupoid-indiscrete-Precategory :
    is-pregroupoid-Precategory (indiscrete-Precategory X)
  is-pregroupoid-indiscrete-Precategory x y =
    is-iso-hom-indiscrete-Precategory {x} {y}

  indiscrete-Pregroupoid : Pregroupoid l lzero
  pr1 indiscrete-Pregroupoid = indiscrete-Precategory X
  pr2 indiscrete-Pregroupoid = is-pregroupoid-indiscrete-Precategory

The predicate on a precategory of being indiscrete

For completeness, we also record the predicate on a precategory of being indiscrete.

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  is-indiscrete-Precategory : UU (l1  l2)
  is-indiscrete-Precategory =
    (x y : obj-Precategory C)  is-contr (hom-Precategory C x y)

  is-prop-is-indiscrete-Precategory : is-prop is-indiscrete-Precategory
  is-prop-is-indiscrete-Precategory =
    is-prop-iterated-Π 2  x y  is-property-is-contr)

  is-indiscrete-prop-Precategory : Prop (l1  l2)
  pr1 is-indiscrete-prop-Precategory = is-indiscrete-Precategory
  pr2 is-indiscrete-prop-Precategory = is-prop-is-indiscrete-Precategory

The indiscrete precategory associated to a type is indiscrete

module _
  {l : Level} (X : UU l)
  where

  is-indiscrete-indiscrete-Precategory :
    is-indiscrete-Precategory (indiscrete-Precategory X)
  is-indiscrete-indiscrete-Precategory x y = is-contr-unit

Properties

If an indiscrete precategory is preunivalent then it is a strict category

Proof: If an indiscrete precategory is preunivalent, that means every identity type of the objects embeds into the unit type, hence the objects form a set.

module _
  {l : Level} (X : UU l)
  where

  is-strict-category-is-preunivalent-indiscrete-Precategory :
    is-preunivalent-Precategory (indiscrete-Precategory X) 
    is-strict-category-Precategory (indiscrete-Precategory X)
  is-strict-category-is-preunivalent-indiscrete-Precategory H x y =
    is-prop-is-emb
      ( iso-eq-Precategory (indiscrete-Precategory X) x y)
      ( H x y)
      ( is-prop-Σ
        ( is-prop-unit)
        ( is-prop-is-iso-Precategory (indiscrete-Precategory X) {x} {y}))

The construction of indiscrete-Precategory is a section of obj-Precategory

is-section-indiscrete-Precategory :
  {l : Level}  obj-Precategory  indiscrete-Precategory {l} ~ id
is-section-indiscrete-Precategory X = refl

Indiscrete precategories are subterminal

module _
  {l : Level} (X : UU l)
  where

  is-subterminal-indiscrete-Precategory :
    is-subterminal-Precategory (indiscrete-Precategory X)
  is-subterminal-indiscrete-Precategory x y = is-equiv-id

A wikidata identifier was not available for this concept.

Recent changes