Opposite preunivalent categories

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2024-03-11.

module category-theory.opposite-preunivalent-categories where
Imports 
open import category-theory.isomorphisms-in-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories
open import category-theory.preunivalent-categories

open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.involutions
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.subtypes
open import foundation.universe-levels

Idea

Let C be a preunivalent category, its opposite preunivalent category Cᵒᵖ is given by reversing every morphism.

Lemma

A precategory is preunivalent if and only if the opposite is preunivalent

abstract
  is-preunivalent-opposite-is-preunivalent-Precategory :
    {l1 l2 : Level} (C : Precategory l1 l2) →
    is-preunivalent-Precategory C →
    is-preunivalent-Precategory (opposite-Precategory C)
  is-preunivalent-opposite-is-preunivalent-Precategory C is-preunivalent-C x y =
    is-emb-htpy-emb
      ( comp-emb
        ( emb-equiv
          ( compute-iso-opposite-Precategory C ∘e equiv-inv-iso-Precategory C))
        ( _ , is-preunivalent-C x y))
      ( λ where
        refl →
          eq-type-subtype
            ( is-iso-prop-Precategory (opposite-Precategory C))
            ( refl))

abstract
  is-preunivalent-is-preunivalent-opposite-Precategory :
    {l1 l2 : Level} (C : Precategory l1 l2) →
    is-preunivalent-Precategory (opposite-Precategory C) →
    is-preunivalent-Precategory C
  is-preunivalent-is-preunivalent-opposite-Precategory C =
    is-preunivalent-opposite-is-preunivalent-Precategory
      ( opposite-Precategory C)

Definitions

The opposite preunivalent category

module _
  {l1 l2 : Level} (C : Preunivalent-Category l1 l2)
  where

  obj-opposite-Preunivalent-Category : UU l1
  obj-opposite-Preunivalent-Category =
    obj-opposite-Precategory (precategory-Preunivalent-Category C)

  hom-set-opposite-Preunivalent-Category :
    (x y : obj-opposite-Preunivalent-Category) → Set l2
  hom-set-opposite-Preunivalent-Category =
    hom-set-opposite-Precategory (precategory-Preunivalent-Category C)

  hom-opposite-Preunivalent-Category :
    (x y : obj-opposite-Preunivalent-Category) → UU l2
  hom-opposite-Preunivalent-Category =
    hom-opposite-Precategory (precategory-Preunivalent-Category C)

  comp-hom-opposite-Preunivalent-Category :
    {x y z : obj-opposite-Preunivalent-Category} →
    hom-opposite-Preunivalent-Category y z →
    hom-opposite-Preunivalent-Category x y →
    hom-opposite-Preunivalent-Category x z
  comp-hom-opposite-Preunivalent-Category =
    comp-hom-opposite-Precategory (precategory-Preunivalent-Category C)

  involutive-eq-associative-comp-hom-opposite-Preunivalent-Category :
    {x y z w : obj-opposite-Preunivalent-Category}
    (h : hom-opposite-Preunivalent-Category z w)
    (g : hom-opposite-Preunivalent-Category y z)
    (f : hom-opposite-Preunivalent-Category x y) →
    comp-hom-opposite-Preunivalent-Category
      ( comp-hom-opposite-Preunivalent-Category h g)
      ( f) ＝ⁱ
    comp-hom-opposite-Preunivalent-Category
      ( h)
      ( comp-hom-opposite-Preunivalent-Category g f)
  involutive-eq-associative-comp-hom-opposite-Preunivalent-Category =
    involutive-eq-associative-comp-hom-opposite-Precategory
      ( precategory-Preunivalent-Category C)

  associative-comp-hom-opposite-Preunivalent-Category :
    {x y z w : obj-opposite-Preunivalent-Category}
    (h : hom-opposite-Preunivalent-Category z w)
    (g : hom-opposite-Preunivalent-Category y z)
    (f : hom-opposite-Preunivalent-Category x y) →
    comp-hom-opposite-Preunivalent-Category
      ( comp-hom-opposite-Preunivalent-Category h g)
      ( f) ＝
    comp-hom-opposite-Preunivalent-Category
      ( h)
      ( comp-hom-opposite-Preunivalent-Category g f)
  associative-comp-hom-opposite-Preunivalent-Category =
    associative-comp-hom-opposite-Precategory
      ( precategory-Preunivalent-Category C)

  id-hom-opposite-Preunivalent-Category :
    {x : obj-opposite-Preunivalent-Category} →
    hom-opposite-Preunivalent-Category x x
  id-hom-opposite-Preunivalent-Category =
    id-hom-opposite-Precategory (precategory-Preunivalent-Category C)

  left-unit-law-comp-hom-opposite-Preunivalent-Category :
    {x y : obj-opposite-Preunivalent-Category}
    (f : hom-opposite-Preunivalent-Category x y) →
    comp-hom-opposite-Preunivalent-Category
      ( id-hom-opposite-Preunivalent-Category)
      ( f) ＝
    f
  left-unit-law-comp-hom-opposite-Preunivalent-Category =
    left-unit-law-comp-hom-opposite-Precategory
      ( precategory-Preunivalent-Category C)

  right-unit-law-comp-hom-opposite-Preunivalent-Category :
    {x y : obj-opposite-Preunivalent-Category}
    (f : hom-opposite-Preunivalent-Category x y) →
    comp-hom-opposite-Preunivalent-Category
      ( f) (id-hom-opposite-Preunivalent-Category) ＝
    ( f)
  right-unit-law-comp-hom-opposite-Preunivalent-Category =
    right-unit-law-comp-hom-opposite-Precategory
      ( precategory-Preunivalent-Category C)

  precategory-opposite-Preunivalent-Category : Precategory l1 l2
  precategory-opposite-Preunivalent-Category =
    opposite-Precategory (precategory-Preunivalent-Category C)

  opposite-Preunivalent-Category : Preunivalent-Category l1 l2
  pr1 opposite-Preunivalent-Category =
    precategory-opposite-Preunivalent-Category
  pr2 opposite-Preunivalent-Category =
    is-preunivalent-opposite-is-preunivalent-Precategory
      ( precategory-Preunivalent-Category C)
      ( is-preunivalent-Preunivalent-Category C)

Properties

The opposite construction is an involution on the type of preunivalent categories

is-involution-opposite-Preunivalent-Category :
  {l1 l2 : Level} → is-involution (opposite-Preunivalent-Category {l1} {l2})
is-involution-opposite-Preunivalent-Category C =
  eq-type-subtype
    ( is-preunivalent-prop-Precategory)
    ( is-involution-opposite-Precategory (precategory-Preunivalent-Category C))

involution-opposite-Preunivalent-Category :
  (l1 l2 : Level) → involution (Preunivalent-Category l1 l2)
pr1 (involution-opposite-Preunivalent-Category l1 l2) =
  opposite-Preunivalent-Category
pr2 (involution-opposite-Preunivalent-Category l1 l2) =
  is-involution-opposite-Preunivalent-Category

is-equiv-opposite-Preunivalent-Category :
  {l1 l2 : Level} → is-equiv (opposite-Preunivalent-Category {l1} {l2})
is-equiv-opposite-Preunivalent-Category =
  is-equiv-is-involution is-involution-opposite-Preunivalent-Category

equiv-opposite-Preunivalent-Category :
  (l1 l2 : Level) → Preunivalent-Category l1 l2 ≃ Preunivalent-Category l1 l2
equiv-opposite-Preunivalent-Category l1 l2 =
  equiv-involution (involution-opposite-Preunivalent-Category l1 l2)

Recent changes