open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning

module Cat.Univalent.Instances.Opposite
  {o β„“} {C : Precategory o β„“}

Opposites of univalent categoriesπŸ”—

A simple case of closure of univalence is the duality involution: Since isomorphisms in Cop\mathcal{C}^{\mathrm{op}} are the same as isomorphisms in C\mathcal{C}, 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 (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 _)