import Nat

data (~>) (k n : Nat)
    = id (k = n)
    | comp (m : Nat) (k ~> m) (m ~> n)
    | face (i : Nat) (i <= suc k) (suc k = n)
    | deg (i : Nat) (i <= n) (k = suc n)
    | comp-id (k ~> n) I
    | id-comp (k ~> n) I
    | comp-comp (m l : Nat) (k ~> m) (m ~> l) (l ~> n) I
    | face-face (i j : Nat) (i <= j) (j <= suc k) (suc (suc k) = n) I
    | deg-deg {i j : Nat} (j <= i) (i <= n) (k = suc (suc n)) I
    | face-deg-1 {i j m : Nat} (i <= j) (j <= m) (k = suc m) (suc m = n) I
    | face-deg-2 {i j : Nat} (j <= i) (i <= suc j) (j <= k) (k = n) I
    | face-deg-3 {i j m : Nat} (suc j <= i) (i <= suc m) (k = suc m) (suc m = n) I
    | trunc (x y : k ~> n) (x = y) (x = y) I I
  with
    comp-id p left = comp n p (id idp)
    comp-id p right = p
    id-comp p left = comp k (id idp) p
    id-comp p right = p
    comp-comp m l p q r left = comp l (comp m p q) r
    comp-comp m l p q r right = comp m p (comp l q r)
    face-face i j p q r left = comp (suc k) (face i (trans p q) idp) (face (suc j) (wrap q) r)
    face-face i j p q r right = comp (suc k) (face j q idp) (face i (trans (suc-le p) (wrap q)) r)
    deg-deg i j p q r left = comp (suc n) (deg (suc i) (wrap q) r) (deg j (trans p q) idp)
    deg-deg i j p q r right = comp (suc n) (deg j (suc-le (trans p q)) r) (deg i q idp)
    face-deg-1 i j m p q r s left = comp (suc k) (face i (trans (trans p q) (trans (trans-le-eq (suc-le id-le) (inv r)) (suc-le id-le))) idp) (deg (suc j) (trans-le-eq (wrap q) s) (map suc (r * s)))
    face-deg-1 i j m p q r s right = comp m (deg j q r) (face i (trans (trans p q) (suc-le id-le)) s)
    face-deg-2 i j p q r s left = comp (suc k) (face i (trans q (wrap r)) idp) (deg j (trans-le-eq r s) (map suc s))
    face-deg-2 i j p q r s right = id s
    face-deg-3 i j m p q r s left = comp (suc k) (face (suc i) (wrap (trans-le-eq q (inv r))) idp) (deg j (trans (suc-le id-le) (trans p (trans-le-eq q s))) (map suc (r * s)))
    face-deg-3 i j m p q r s right = comp m (deg j (unWrap (trans p q)) r) (face i q s)
    trunc x _ _ _ left  _ = x
    trunc _ y _ _ right _ = y
    trunc _ _ p _ i left  = p @ i
    trunc _ _ _ q i right = q @ i