open import Cat.Prelude

import Cat.Reasoning

module Cat.Univalent.Instances.Opposite
  {o ℓ} {C : Precategory o ℓ}
  where

private
  module C = Cat.Reasoning C
  module Cop = Cat.Reasoning (C ^op)

Opposites of univalent categories🔗

A simple case of closure of univalence is the duality involution: Since isomorphisms in ${\mathcal{C}}^{\mathrm{op}}$ are the same as isomorphisms in $\mathcal{C}\text{,}$ the former is univalent iff the latter is.

opposite-is-category : is-category C → is-category (C ^op)
opposite-is-category x .to-path i = x .to-path $
  C.make-iso (i .Cop.from) (i .Cop.to) (i .Cop.invl) (i .Cop.invr)
opposite-is-category x .to-path-over p =
  Cop.≅-pathp refl _ $ Univalent.Hom-pathp-refll-iso x (C.idl _)