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 are the same as isomorphisms in 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 _)