Fix type of exported natural isomorphisms

[jacquescomeaux]

These two natural isomorphisms are not oped enough

{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)

module Minimal {o ℓ e} {𝒞 : Category o ℓ e} (cocartesian : Cocartesian 𝒞) where

open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
open import Categories.Functor using (id; Functor)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

open Cocartesian cocartesian using (⊥; _+-; -+_)
open CocartesianMonoidal 𝒞 cocartesian using () renaming (⊥+--id to ⊥+--id′; -+⊥-id to -+⊥-id′)

module Bad where

  open Functor using (op)

  ⊥+--id : NaturalIsomorphism (op (⊥ +-)) id
  ⊥+--id = ⊥+--id′

  -+⊥-id : NaturalIsomorphism (op (-+ ⊥)) id
  -+⊥-id = -+⊥-id′

module Good where

  open NaturalIsomorphism using (op′)

  ⊥+--id : NaturalIsomorphism (⊥ +-) id
  ⊥+--id = op′ ⊥+--id′

  -+⊥-id : NaturalIsomorphism (-+ ⊥) id
  -+⊥-id = op′ -+⊥-id′