agda/examples/outdated-and-incorrect/cat/Dual.agda

module Dual where

open import Prelude using (flip)
open import Logic.Equivalence
open import Category

_op : Cat -> Cat
ℂ@(cat _ _ _ _ _ _ _ _ _) op = cat Obj
           (\A B -> B ─→ A)
            id
           (\{_}{_}{_} -> flip _∘_)
           (\{_}{_} -> Eq)
           (\{_}{_}{_}{_}{_}{_}{_} -> flip cong)
           (\{_}{_}{_} -> idR)
           (\{_}{_}{_} -> idL)
           (\{_}{_}{_}{_}{_}{_}{_} -> sym assoc)
  where open module C = Cat ℂ

{-
open Poly-Cat

dualObj : {ℂ : Cat} -> Obj ℂ -> Obj (ℂ op)
dualObj {cat _ _ _ _ _ _ _ _ _}(obj A) = obj A

undualObj : {ℂ : Cat} -> Obj (ℂ op) -> Obj ℂ
undualObj {cat _ _ _ _ _ _ _ _ _}(obj A) = obj A

dualdualArr : {ℂ : Cat}{A B : Obj ℂ} -> A ─→ B -> dualObj B ─→ dualObj A
dualdualArr {cat _ _ _ _ _ _ _ _ _}{A = obj _}{B = obj _}(arr f) = arr f

dualundualArr : {ℂ : Cat}{A : Obj ℂ}{B : Obj (ℂ op)} ->
                A ─→ undualObj B -> B ─→ dualObj A
dualundualArr {cat _ _ _ _ _ _ _ _ _}{A = obj _}{B = obj _}(arr f) = arr f
-}