omega-category.agda

open import Level
-- "Wok" stands for "weak omega kategory".
mutual
  record Wok {i} (Obj : Set i) : Set (suc i) where
    coinductive
    constructor Wok:
    infix  1 Hom
    infixr 9 compo
    field Arr : (a b : Obj) -> Set i
    field Hom : (a b : Obj) -> Wok (Arr a b)

    -- aren't these supposed to be functors?
    -- I guess we'll try to prove that they always are later.
    field ident : ∀{a} -> Arr a a
    field compo : ∀{a b c} (f : Arr a b) (g : Arr b c) -> Arr a c

    field idl : ∀{a b} f -> Iso (Hom a b) f (compo ident f)
    field idr : ∀{a b} f -> Iso (Hom a b) f (compo f ident)
    field assoc : ∀{a b c d} (f : Arr a b) (g : Arr b c) (h : Arr c d) ->
                  Iso (Hom a d) (compo f (compo g h)) (compo (compo f g) h)

  record Iso {i Obj} (C : Wok {i} Obj) (a b : Obj) : Set i where
    coinductive
    field a→b : Wok.Arr C a b
    field b→a : Wok.Arr C b a
    field ida : Iso (Wok.Hom C a a) (Wok.ident C) (Wok.compo C a→b b→a)
    field idb : Iso (Wok.Hom C b b) (Wok.ident C) (Wok.compo C b→a a→b)