csystem.ctt

module csystem where
import prelude
import sigma
import equiv
import nat
import category

mkFt (ob : nat -> U) (ft0 : (n : nat) -> ob (suc n) -> ob n) : (n : nat) -> ob n -> Sigma nat ob = split
  zero  -> \(x : ob zero) -> (zero, x)
  suc n -> \(x : ob (suc n)) -> (n, ft0 n x)

--
-- C0-Systems
-- Objects of C0-systems are given by a length indexed family "ob : nat -> U", to avoid equalities on object lengths
-- The morphisms (p : (x y : A) -> Path A (ft x) y -> hom x y) depend on a path in "Path A (ft x) y" because we can't
-- enforce a definitional equality in "Path A (ft f*(X)) Y" in this square :
--
--      q(f, X)
-- f*(X) ----> X
-- |           |
-- |           | p_X
-- |           |
-- Y -------> ft(X)
--      f
--
isC0System (ob : nat -> U) (hom : Sigma nat ob -> Sigma nat ob -> U) (isC : isPrecategory (Sigma nat ob, hom)) : U
  = let A : U = Sigma nat ob
        CD : categoryData = (A,hom)
        C : precategory = (CD, isC)
    in (ASet : (n : nat) -> set (ob n))
     * (ft0 : (n : nat) -> ob (suc n) -> ob n)
     * (let ft (x : A) : A = mkFt ob ft0 x.1 x.2
        in
       (p : (x y : A) -> Path A (ft x) y -> hom x y)
     * (sq : (n : nat) -> (X : ob (suc n)) -> (Y : A) ->
             (f : hom Y (n, ft0 n X)) ->
             (f_star : ob (suc Y.1)) * (ftf : Path A (Y.1, ft0 Y.1 f_star) Y)
           * (q : hom (suc Y.1, f_star) (suc n, X))
           * Path (hom (suc Y.1, f_star) (n, ft0 n X))
                (cC C (suc Y.1, f_star) Y (n, ft0 n X) (p (suc Y.1, f_star) Y ftf) f)
                (cC C (suc Y.1, f_star) (suc n, X) (n, ft0 n X) q (p (suc n, X) (n, ft0 n X) (<_> (n, ft0 n X))))
       )
     * (sqPath : (n : nat) -> (X : ob (suc n)) ->
               (p0 : Path A (suc n, (sq n X (n, ft0 n X) (cPath C (n, ft0 n X))).1) (suc n, X))
             * (PathP (<i>cH C (p0@i) (suc n, X)) (sq n X (n, ft0 n X) (cPath C (n, ft0 n X))).2.2.1 (cPath C (suc n, X)))
       )
     * ((n : nat) -> (X : ob (suc n)) ->
        (Y : A) -> (f : hom Y (n, ft0 n X)) ->
        (Z : A) -> (g : hom Z Y) ->
        (let f_star : ob (suc Y.1) = (sq n X Y f).1
             g' : hom Z (Y.1, ft0 Y.1 f_star) = transport (<i>cH C Z ((sq n X Y f).2.1@-i)) g
         in (p0 : Path A (suc Z.1, (sq Y.1 f_star Z g').1)
                       (suc Z.1, (sq n X Z (cC C Z Y (n, ft0 n X) g f)).1))
          * PathP (<i> cH C (p0@i) (suc n, X))
                (cC C (suc Z.1, (sq Y.1 f_star Z g').1) (suc Y.1, f_star) (suc n, X)
                  (sq Y.1 f_star Z g').2.2.1 (sq n X Y f).2.2.1)
                (sq n X Z (cC C Z Y (n, ft0 n X) g f)).2.2.1)))

C0System : U = (ob : nat -> U) * (hom : Sigma nat ob -> Sigma nat ob -> U) * (isC : isPrecategory (Sigma nat ob, hom))
             * isC0System ob hom isC

c0C (C : C0System) : precategory = ((Sigma nat C.1, C.2.1), C.2.2.1)

c0ASet (C : C0System) : set (cA (c0C C)) = setSig nat C.1 natSet C.2.2.2.1
c0Ft (C : C0System) (x : cA (c0C C)) : cA (c0C C) = mkFt C.1 C.2.2.2.2.1 x.1 x.2

c0P (C : C0System) : (x y : cA (c0C C)) -> Path (cA (c0C C)) (c0Ft C x) y -> C.2.1 x y = C.2.2.2.2.2.1

c0CanSq (C : C0System) : U
  = (n : nat) * (X : C.1 (suc n)) * (Y : cA (c0C C)) * (C.2.1 Y (n, C.2.2.2.2.1 n X))

c0Star (C : C0System) (T : c0CanSq C) : cA (c0C C)
  = (suc T.2.2.1.1, (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2).1)
c0FtStar (C : C0System) (T : c0CanSq C)
  : Path (cA (c0C C)) (c0Ft C (c0Star C T)) T.2.2.1
  = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2).2.1

c0Q (C : C0System) (T : c0CanSq C) : C.2.1 (c0Star C T) (suc T.1, T.2.1)
  = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2).2.2.1

c0Square (C : C0System) (T : c0CanSq C)
  : (let X : cA (c0C C) = (suc T.1, T.2.1) in
     Path (C.2.1 (c0Star C T) (c0Ft C X))
        (cC (c0C C) (c0Star C T) T.2.2.1 (c0Ft C X) (c0P C (c0Star C T) T.2.2.1 (c0FtStar C T)) T.2.2.2)
        (cC (c0C C) (c0Star C T) X (c0Ft C X) (c0Q C T) (c0P C X (c0Ft C X) (<_> (c0Ft C X)))))
  = (C.2.2.2.2.2.2.1 T.1 T.2.1 T.2.2.1 T.2.2.2).2.2.2

c0FtH (C : C0System) (Y X : cA (c0C C)) (f : cH (c0C C) Y X) : cH (c0C C) Y (c0Ft C X)
  = cC (c0C C) Y X (c0Ft C X) f (c0P C X (c0Ft C X) (<_> c0Ft C X))

--
-- A C0-system is a C-system if all of its canonical squares ("c0CanSq C") are pullback squares
--

isCSystemCospan (C : C0System) (T : c0CanSq C) : cospan (c0C C)
  = let X : cA (c0C C) = (suc T.1, T.2.1) in
    (c0Ft C X,
     (T.2.2.1, T.2.2.2),
     (X, c0P C X (c0Ft C X) (<_>c0Ft C X)))

isCSystemCospanCone (C : C0System) (T : c0CanSq C) : cospanCone (c0C C) (isCSystemCospan C T)
  = (c0Star C T,
     c0P C (c0Star C T) T.2.2.1 (c0FtStar C T),
     c0Q C T,
     c0Square C T)

isCSystemType (C : C0System) (T : c0CanSq C) : U
  = isPullback (c0C C)
      (isCSystemCospan C T)
      (isCSystemCospanCone C T)
isCSystem (C : C0System) : U
  = (T : c0CanSq C) -> isCSystemType C T

isCSystemProp (C : C0System) : prop (isCSystem C)
  = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystemType C T)
    (\(T : c0CanSq C) -> isPullbackProp (c0C C) (isCSystemCospan C T) (isCSystemCospanCone C T))

CSystem : U = (ob : nat -> U) * (hom : Sigma nat ob -> Sigma nat ob -> U) * (isC : isPrecategory (Sigma nat ob, hom))
            * (c0 : isC0System ob hom isC) * isCSystem (ob, hom, isC, c0)

--
-- Definition of a universe category
--

uc : U
   = (C : precategory)
   * (_ : isCategory C)
   * (pt : hasFinal C)
   * (V : cA C) * (VT : cA C) * (p : cH C VT V)
   * ((f : homTo C V) -> hasPullback C (V, f, VT, p))

-- An equivalence of universe categories is an equivalence of categories compatible with the "p" morphism
ucEquiv (A B : uc) : U
  = (e : catEquiv A.1 B.1)
  * (V : Path (cA B.1) (e.1.1 A.2.2.2.1) B.2.2.2.1)
  * (VT : Path (cA B.1) (e.1.1 A.2.2.2.2.1) B.2.2.2.2.1)
  * (PathP (<i>cH B.1 (VT@i) (V@i)) (e.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1) B.2.2.2.2.2.1)

ucEquivPath (A B : uc) (e : ucEquiv A B) : Path uc A B
  = let p : Path ((C:category)*catEquiv A.1 C.1) ((A.1, A.2.1), catPathEquiv A.1) ((B.1, B.2.1), e.1)
          = isContrProp ((C:category)*catEquiv A.1 C.1) (catEquivEqPath' (A.1, A.2.1)) ((A.1, A.2.1), catPathEquiv A.1) ((B.1, B.2.1), e.1)
        opaque p
        pFinal : PathP (<i> hasFinal (p@i).1.1) A.2.2.1  B.2.2.1
               = lemPathPProp (hasFinal A.1)
                            (hasFinal B.1)
                            (hasFinalProp A.1 A.2.1)
                            (<i>hasFinal (p@i).1.1)
                            A.2.2.1 B.2.2.1
        opaque pFinal
        pV : PathP (<i> cA (p@i).1.1) A.2.2.2.1 B.2.2.2.1
           = <i> comp (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.1)
                  [(i=0)-><_>A.2.2.2.1 ,(i=1)-><k>e.2.1@k]
        pVT : PathP (<i> cA (p@i).1.1) A.2.2.2.2.1 B.2.2.2.2.1
            = <i> comp (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.2.1)
                   [(i=0)-><_>A.2.2.2.2.1 ,(i=1)-><k>e.2.2.1@k]
        pP : PathP (<i> cH (p@i).1.1 (pVT@i) (pV@i)) A.2.2.2.2.2.1 B.2.2.2.2.2.1
           = <i> comp (<k> cH (p@i).1.1
                       (fill (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.2.1) [(i=0)-><_>A.2.2.2.2.1 ,(i=1)-><k>e.2.2.1@k]@k)
                       (fill (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.1) [(i=0)-><_>A.2.2.2.1 ,(i=1)-><k>e.2.1@k]@k))
                  ((p@i).2.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1)
                  [(i=0)-><_>A.2.2.2.2.2.1, (i=1)-><k>e.2.2.2@k]
        opaque pV
        opaque pVT
        opaque pP
        pPb : PathP (<i> (f : homTo (p@i).1.1 (pV@i)) -> hasPullback (p@i).1.1 (pV@i, f, pVT@i, pP@i)) A.2.2.2.2.2.2 B.2.2.2.2.2.2
            = lemPathPProp ((f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0))
                         ((f : homTo B.1 (pV@1)) -> hasPullback B.1 (pV@1, f, pVT@1, pP@1))
                         (propPi (homTo A.1 (pV@0)) (\(f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0))
                          (\(f : homTo A.1 (pV@0)) -> hasPullbackProp A.1 A.2.1 (pV@0, f, pVT@0, pP@0)))
                         (<i>(f : homTo (p@i).1.1 (pV@i)) -> hasPullback (p@i).1.1 (pV@i, f, pVT@i, pP@i))
                         A.2.2.2.2.2.2 B.2.2.2.2.2.2
        opaque pPb
        t:nat=zero
    in <i> ((p@i).1.1
           ,(p@i).1.2
           ,pFinal@i
           ,pV@i, pVT@i, pP@i
           ,pPb@i)


--
-- Definition of a C0-system from a universe category
--
ucToC0 (C : uc) : CSystem = hole
  where
    V : cA C.1 = C.2.2.2.1
    VT : cA C.1 = C.2.2.2.2.1
    p : cH C.1 VT V = C.2.2.2.2.2.1
    mutual
      ob : (n : nat) -> U = split
        zero -> Unit
        suc n -> (A : ob n) * cH C.1 (int n A) V
      int : (n : nat) -> ob n -> cA C.1 = split
        zero -> \(_:Unit) -> C.2.2.1.1
        suc n -> \(X : ob (suc n)) -> (pb n X).1.1
      F (n : nat) (X : ob (suc n)) : homTo C.1 V = (int n X.1, X.2)
      cs (n : nat) (X : ob (suc n)) : cospan C.1 = (V, F n X, VT, p)
      pb (n : nat) (X : ob (suc n)) : hasPullback C.1 (cs n X)
        = C.2.2.2.2.2.2 (int n X.1, X.2)
    obSet : (n : nat) -> set (ob n) = split
      zero -> setUnit
      suc n -> setSig (ob n) (\(A : ob n) -> cH C.1 (int n A) V) (obSet n) (\(A : ob n) -> cHSet C.1 (int n A) V)
    obD : U = Sigma nat ob
    intD (x : obD) : cA C.1 = int x.1 x.2
    homD (a b : obD) : U = C.1.1.2 (intD a) (intD b)
    homDSet (a b : obD) : set (homD a b) = cHSet C.1 (intD a) (intD b)
    DPath (a : obD) : homD a a = cPath C.1 (intD a)
    DC (a b c : obD) (f : homD a b) (g : homD b c) : homD a c = cC C.1 (intD a) (intD b) (intD c) f g
    DPathL (a b : obD) (g : homD a b) : Path (homD a b) (DC a a b (DPath a) g) g = C.1.2.2.2.2.1 (intD a) (intD b) g
    DPathR (a b : obD) (g : homD a b) : Path (homD a b) (DC a b b g (DPath b)) g = C.1.2.2.2.2.2.1 (intD a) (intD b) g
    DPathC (a b c d : obD) (f : homD a b) (g : homD b c) (h : homD c d)
         : Path (homD a d) (DC a c d (DC a b c f g) h) (DC a b d f (DC b c d g h))
         = C.1.2.2.2.2.2.2 (intD a) (intD b) (intD c) (intD d) f g h
    DD : categoryData = (obD, homD)
    D : isPrecategory DD
      = (DPath, DC, homDSet, DPathL, DPathR, DPathC)
    DC : precategory = (DD, D)
    -- ^ Definition of the precategory

    ft0 (n : nat) (x : ob (suc n)) : ob n = x.1
    ft (x : obD) : obD = mkFt ob ft0 x.1 x.2
    p0 : (n : nat) -> (x : ob n) -> homD (n, x) (ft (n, x)) = split
      zero  -> \(A:Unit) -> DPath (zero, A)
      suc n -> \(X:ob (suc n)) -> (pb n X).1.2.1
    pD (x y : obD) (p : Path obD (ft x) y) : homD x y = transport (<i>homD x (p@i)) (p0 x.1 x.2)

    fstar (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1)) : obD
      = (suc Y.1, Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)

    -- The C-system constructed from the universe category has the definitional equality ft(f*(X)) = Y,
    -- but this cannot be required to hold definitionally in the definition of C-systems, so what we need
    -- to prove contains transports by reflexivity.
    -- To simplify the proofs, the proofs are done without this transport first, and transported to the
    -- right types afterwards.
    q_ (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
      : (q : homD (fstar n X Y f) (suc n, X))
      * (qSq : Path (homD (fstar n X Y f) (n, X.1))
                  (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f)
                  (cC DC (fstar n X Y f) (suc n, X) (n, X.1) q (p0 (suc n) X)))
      * (_ : Path (cH C.1 (intD (fstar n X Y f)) VT)
                (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT q (pb n X).1.2.2.1)
                (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1)
      * isPullback DC ((n, X.1), (Y, f), ((suc n, X), p0 (suc n) X)) (fstar n X Y f, p0 (suc Y.1) (fstar n X Y f).2, q, qSq)
      = let f_star : obD = fstar n X Y f
            if_star : cA C.1 = intD f_star
            gF : cH C.1 (intD Y) V = cC C.1 (intD Y) (int n X.1) V f X.2
            qq : cH C.1 if_star VT = (pb Y.1 (Y.2, gF)).1.2.2.1
            pg : cH C.1 if_star (int n X.1) = cC C.1 if_star (intD Y) (int n X.1) (p0 (suc Y.1) f_star.2) f
            hole0 : Path (cH C.1 if_star V)
                       (cC C.1 if_star (int n X.1) V pg X.2)
                       (cC C.1 if_star VT V qq p)
                  = compPath (cH C.1 if_star V)
                           (cC C.1 if_star (int n X.1) V pg X.2)
                           (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V qq p)
                           (cPathC C.1 if_star (intD Y) (int n X.1) V (pb Y.1 (Y.2, gF)).1.2.1 f X.2)
                           (pb Y.1 (Y.2, gF)).1.2.2.2
            pp : cospanCone C.1 (cs n X)
               = (if_star, pg, qq, hole0)
            q : homD (fstar n X Y f) (suc n, X) = ((pb n X).2 pp).1.1
            hole1 : Path (cH C.1 if_star V)
                       (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                       (cC C.1 if_star VT V (cC C.1 if_star (int (suc n) X) VT q (pb n X).1.2.2.1) p)
                  = transport
                      (<i> Path (cH C.1 if_star V)
                       (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                       (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2 @ -i) p))
                       (pb Y.1 (Y.2, gF)).1.2.2.2
            pbD : isPullback C.1 (int n X.1, (intD Y, f), (int (suc n) X, p0 (suc n) X))
                                 (if_star, p0 (suc Y.1) (fstar n X Y f).2, q, <i>((pb n X).2 pp).1.2.1@-i)
               = pullbackPasting C.1
                   if_star (int (suc n) X) VT
                   (intD Y) (int n X.1) V
                   q (pb n X).1.2.2.1
                   f X.2
                   (p0 (suc Y.1) f_star.2) (p0 (suc n) X) p
                   (<i>((pb n X).2 pp).1.2.1@-i)
                   (pb n X).1.2.2.2
                   hole1
                   (pb n X).2
                   (transport
                     (<i> isPullback C.1 (cs Y.1 f_star.2)
                       ((pb Y.1 f_star.2).1.1
                       ,(pb Y.1 f_star.2).1.2.1
                       ,((pb n X).2 pp).1.2.2@-i
                       ,lemPathPProp
                         (Path (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@1) p))
                         (Path (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@0) p))
                         (cHSet C.1 if_star V (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@1) p))
                         (<i>Path (cH C.1 if_star V) (cC C.1 if_star (intD Y) V (pb Y.1 (Y.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V (((pb n X).2 pp).1.2.2@-i) p))
                           (pb Y.1 f_star.2).1.2.2.2 hole1 @ i
                       ))
                     (pb Y.1 f_star.2).2)
        in (q,
            <i>((pb n X).2 pp).1.2.1@-i,
            ((pb n X).2 pp).1.2.2,
            \(A : cospanCone DC ((n, X.1), (Y, f), ((suc n, X), p0 (suc n) X))) ->
              pbD (intD A.1, A.2.1, A.2.2.1, A.2.2.2)
           )

    sqD0 (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
      : (f_star : ob (suc Y.1)) * (ftf : Path obD (Y.1, ft0 Y.1 f_star) Y)
      * (q : homD (suc Y.1, f_star) (suc n, X))
      * (qSq : Path (homD (suc Y.1, f_star) (n, X.1))
                  (cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f)
                  (cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1)))))
      * isPullback DC ((n, X.1), (Y, f), ((suc n, X), pD (suc n, X) (n, X.1) (<_> (n, X.1))))
                      ((suc Y.1, f_star), pD (suc Y.1, f_star) Y ftf, q, qSq)
      = ((fstar n X Y f).2, <_> Y, (q_ n X Y f).1,
          transport
            (<i> (qSq : Path (homD (fstar n X Y f) (n, X.1))
                           (cC DC (fstar n X Y f) Y (n, X.1) (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i) f)
                           (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i))
                 )
               * isPullback DC ((n, X.1), (Y, f), ((suc n, X), (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i)))
                               (fstar n X Y f, (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i), (q_ n X Y f).1, qSq)
                    )
            ((q_ n X Y f).2.1, (q_ n X Y f).2.2.2))

    -- Projections of the previous proof to the actual datum of the C system
    sqD (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
      : (f_star : ob (suc Y.1)) * (ftf : Path obD (Y.1, ft0 Y.1 f_star) Y)
      * (q : homD (suc Y.1, f_star) (suc n, X))
      * Path (homD (suc Y.1, f_star) (n, X.1))
           (cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f)
           (cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1))))
      = ((sqD0 n X Y f).1, (sqD0 n X Y f).2.1, (sqD0 n X Y f).2.2.1, (sqD0 n X Y f).2.2.2.1)

    pbSq (sq : (n : nat) * (X : ob (suc n)) * (Y : obD) * (homD Y (n, X.1)))
       : isPullback DC ((sq.1, sq.2.1.1), (sq.2.2.1, sq.2.2.2), ((suc sq.1, sq.2.1), pD (suc sq.1, sq.2.1) (sq.1, sq.2.1.1) (<_> (sq.1, sq.2.1.1))))
                       (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2
                       ,pD (suc sq.2.2.1.1, (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2) sq.2.2.1 (sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.1
                       ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.1
                       ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2)
       = (sqD0 sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2.2

    qPath (n : nat) (X : ob (suc n)) :
        (p0 : Path obD (fstar n X (n, X.1) (cPath DC (n, X.1))) (suc n, X))
      * (PathP (<i>cH DC (p0@i) (suc n, X)) (q_ n X (n, X.1) (cPath DC (n, X.1))).1 (cPath DC (suc n, X)))
      = let f_star : obD = fstar n X (n, X.1) (cPath DC (n, X.1))
            p1 : Path obD f_star (suc n, X) = <i> (suc n, X.1, cPathL C.1 (int n X.1) V X.2 @ i)
            if_star : cA C.1 = intD f_star
            gF : cH C.1 (int n X.1) V = cC C.1 (int n X.1) (int n X.1) V (cPath DC (n, X.1)) X.2
            qq : cH C.1 if_star VT = (pb n (X.1, gF)).1.2.2.1
            pg : cH C.1 if_star (int n X.1)
               = cC C.1 if_star (int n X.1) (int n X.1) (p0 (suc n) f_star.2) (cPath DC (n, X.1))
            hole0 : Path (cH C.1 if_star V)
                       (cC C.1 if_star (int n X.1) V pg X.2)
                       (cC C.1 if_star VT V qq p)
                  = compPath (cH C.1 if_star V)
                           (cC C.1 if_star (int n X.1) V pg X.2)
                           (cC C.1 if_star (int n X.1) V (pb n (X.1, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V qq p)
                           (cPathC C.1 if_star (int n X.1) (int n X.1) V (pb n (X.1, gF)).1.2.1 (cPath DC (n, X.1)) X.2)
                           (pb n (X.1, gF)).1.2.2.2
            pp : cospanCone C.1 (cs n X)
               = (if_star, pg, qq, hole0)
            ppPath : Path (cospanCone C.1 (cs n X)) pp (pb n X).1
                 = <i> (intD (p1@i),
                        cPathR C.1 (intD (p1@i)) (int n X.1) (p0 (suc n) (p1@i).2) @ i,
                        (pb n (X.1, cPathL C.1 (int n X.1) V X.2 @ i)).1.2.2.1,
                        lemPathPProp (Path (cH C.1 if_star V) (cC C.1 if_star (int n X.1) V pg X.2) (cC C.1 if_star VT V qq p))
                                   (Path (cH C.1 (int (suc n) X) V)
                                     (cC C.1 (int (suc n) X) (int n X.1) V (p0 (suc n) X) X.2)
                                     (cC C.1 (int (suc n) X) VT V (pb n X).1.2.2.1 p))
                                   (cHSet C.1 if_star V (cC C.1 if_star (int n X.1) V pg X.2) (cC C.1 if_star VT V qq p))
                                   (<i>Path (cH C.1 (intD (p1@i)) V)
                                     (cC C.1 (intD (p1@i)) (int n X.1) V (cPathR C.1 (intD (p1@i)) (int n X.1) (p0 (suc n) (p1@i).2) @ i) X.2)
                                     (cC C.1 (intD (p1@i)) VT V ((pb n (X.1, cPathL C.1 (int n X.1) V X.2 @ i)).1.2.2.1) p))
                                   hole0
                                   (pb n X).1.2.2.2
                                   @ i
                       )
            pph : cospanConeHom C.1 (cs n X) pp (pb n X).1
                = transport (<i> cospanConeHom C.1 (cs n X) (ppPath@-i) (pb n X).1) (cospanConePath C.1 (cs n X) (pb n X).1)
            pphPath : Path (cospanConeHom C.1 (cs n X) pp (pb n X).1) ((pb n X).2 pp).1 pph
                  = ((pb n X).2 pp).2 pph
            qPath : Path (cH DC f_star (suc n, X)) ((pb n X).2 pp).1.1 (transport (<i> cH C.1 (ppPath@-i).1 (int (suc n) X)) (cPath DC (suc n, X)))
                = <i>(pphPath@i).1
        in
        ( p1
        , <i> substPathP
                (cH DC (p1@1) (suc n, X)) (cH DC (p1@0) (suc n, X))
                (<i>cH DC (p1@-i) (suc n, X)) (cPath DC (suc n, X)) (q_ n X (n, X.1) (cPath DC (n, X.1))).1
                (<i>qPath@-i)
                @ -i
        )

    qComp (n : nat) (X : ob (suc n))
          (Y : obD) (f : homD Y (n, X.1))
          (Z : obD) (g : homD Z Y)
        : (p0 : Path obD (fstar Y.1 (fstar n X Y f).2 Z g)
                       (fstar n X Z (cC DC Z Y (n, X.1) g f)))
        * PathP (<i> cH DC (p0@i) (suc n, X))
              (cC DC (fstar Y.1 (fstar n X Y f).2 Z g) (fstar n X Y f) (suc n, X)
                (q_ Y.1 (fstar n X Y f).2 Z g).1 (q_ n X Y f).1)
              (q_ n X Z (cC DC Z Y (n, X.1) g f)).1
      = let F : homD Z (n, X.1) = cC DC Z Y (n, X.1) g f
            f_star : obD = fstar n X Z F
            if_star : cA C.1 = intD f_star
            gF : cH C.1 (intD Z) V = cC C.1 (intD Z) (int n X.1) V F X.2
            qq : cH C.1 if_star VT = (pb Z.1 (Z.2, gF)).1.2.2.1
            pg : cH C.1 if_star (int n X.1) = cC C.1 if_star (intD Z) (int n X.1) (p0 (suc Z.1) f_star.2) F
            hole0 : Path (cH C.1 if_star V)
                       (cC C.1 if_star (int n X.1) V pg X.2)
                       (cC C.1 if_star VT V qq p)
                  = compPath (cH C.1 if_star V)
                           (cC C.1 if_star (int n X.1) V pg X.2)
                           (cC C.1 if_star (intD Z) V (pb Z.1 (Z.2, gF)).1.2.1 gF)
                           (cC C.1 if_star VT V qq p)
                           (cPathC C.1 if_star (intD Z) (int n X.1) V (pb Z.1 (Z.2, gF)).1.2.1 F X.2)
                           (pb Z.1 (Z.2, gF)).1.2.2.2
            pp : cospanCone C.1 (cs n X)
               = (if_star, pg, qq, hole0)
            f_star2 : obD = fstar Y.1 (fstar n X Y f).2 Z g
            if_star2 : cA C.1 = intD f_star2
            q2 : cH DC f_star2 (fstar n X Y f) = (q_ Y.1 (fstar n X Y f).2 Z g).1
            pg2 : cH C.1 if_star2 (int n X.1)
                = cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F
            qq2 : cH C.1 if_star2 VT
                = (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1
            p1 : Path obD f_star2 f_star
               = <i> (suc Z.1, Z.2, cPathC C.1 (intD Z) (intD Y) (int n X.1) V g f X.2 @ -i)
            pp2 : cospanCone C.1 (cs n X)
                = (if_star2, pg2, qq2,
                   transport (<i>Path (cH C.1 (intD(p1@-i)) V)
                              (cC C.1 (intD(p1@-i)) (int n X.1) V (cC DC (p1@-i) Z (n,X.1) (p0 (suc Z.1) (p1@-i).2) F) X.2)
                              (cC C.1 (intD(p1@-i)) VT V (pb Z.1 (Z.2, cPathC C.1 (intD Z) (intD Y) (int n X.1) V g f X.2 @ i)).1.2.2.1 p))
                             hole0)
            ppPath : Path (cospanCone C.1 (cs n X)) pp2 pp
                 = <i> (intD (p1@i),
                        cC DC (p1@i) Z (n,X.1) (p0 (suc Z.1) (p1@i).2) F,
                        (pb Z.1 (Z.2, cPathC C.1 (intD Z) (intD Y) (int n X.1) V g f X.2 @ -i)).1.2.2.1,
                        lemPathPProp
                         (Path (cH C.1 if_star2 V) (cC C.1 if_star2 (int n X.1) V pg2 X.2) (cC C.1 if_star2 VT V qq2 p))
                         (Path (cH C.1 if_star V) (cC C.1 if_star (int n X.1) V pg X.2) (cC C.1 if_star VT V qq p))
                         (cHSet C.1 if_star2 V (cC C.1 if_star2 (int n X.1) V pg2 X.2) (cC C.1 if_star2 VT V qq2 p))
                         (<i>Path (cH C.1 (intD(p1@i)) V)
                           (cC C.1 (intD(p1@i)) (int n X.1) V (cC DC (p1@i) Z (n,X.1) (p0 (suc Z.1) (p1@i).2) F) X.2)
                           (cC C.1 (intD(p1@i)) VT V (pb Z.1 (Z.2, cPathC C.1 (intD Z) (intD Y) (int n X.1) V g f X.2 @ -i)).1.2.2.1 p))
                         pp2.2.2.2 hole0 @ i)

            hole3 : Path (cH C.1 if_star2 (int n X.1))
                       (cC DC f_star2 (suc n, X) (n,X.1)
                        (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1)
                        (p0 (suc n) X)
                       )
                       (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
                  = undefined
            --       = compPath (cH C.1 if_star2 (int n X.1))
            --                (cC DC f_star2 (suc n, X) (n,X.1)
            --                  (cC DC f_star2 (fstar n X Y f) (suc n, X) q2 (q_ n X Y f).1)
            --                  (p0 (suc n) X))
            --                (cC DC f_star2 (fstar n X Y f) (n,X.1)
            --                  q2
            --                  (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X)))
            --                (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
            --                (cPathC DC f_star2 (fstar n X Y f) (suc n, X) (n,X.1) q2 (q_ n X Y f).1 (p0 (suc n) X))
            --        (compPath (cH C.1 if_star2 (int n X.1))
            --                (cC DC f_star2 (fstar n X Y f) (n,X.1)
            --                  q2
            --                  (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (p0 (suc n) X)))
            --                (cC DC f_star2 (fstar n X Y f) (n,X.1)
            --                  q2
            --                  (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f))
            --                (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
            --                (<i> cC DC f_star2 (fstar n X Y f) (n,X.1) q2
            --                       ((q_ n X Y f).2.1@-i))
            --        (compPath (cH C.1 if_star2 (int n X.1))
            --                (cC DC f_star2 (fstar n X Y f) (n,X.1)
            --                  q2
            --                  (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f))
            --                (cC DC f_star2 Y (n,X.1)
            --                  (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2))
            --                  f)
            --                (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
            --                (<i>cPathC DC f_star2 (fstar n X Y f) Y (n, X.1) q2 (p0 (suc Y.1) (fstar n X Y f).2) f@-i)
            --        (compPath (cH C.1 if_star2 (int n X.1))
            --                (cC DC f_star2 Y (n,X.1)
            --                  (cC DC f_star2 (fstar n X Y f) Y q2 (p0 (suc Y.1) (fstar n X Y f).2))
            --                  f)
            --                (cC DC f_star2 Y (n,X.1)
            --                  (cC DC f_star2 Z Y (p0 (suc Z.1) f_star2.2) g)
            --                  f)
            --                (cC DC f_star2 Z (n,X.1) (p0 (suc Z.1) f_star2.2) F)
            --                (<i>cC DC f_star2 Y (n,X.1)
            --                   ((q_ Y.1 (fstar n X Y f).2 Z g).2.1@-i) f)
            --                (cPathC DC f_star2 Z Y (n, X.1) (p0 (suc Z.1) f_star2.2) g f))))
            -- opaque hole3

            hole4 : Path (cH C.1 if_star2 VT)
                       (cC C.1 if_star2 (int (suc n) X) VT
                         (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1)
                         (pb n X).1.2.2.1)
                       (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1
                  = undefined
            --       = compPath (cH C.1 if_star2 VT)
            --                (cC C.1 if_star2 (int (suc n) X) VT
            --                 (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1)
            --                 (pb n X).1.2.2.1)
            --                (cC C.1 if_star2 (intD (fstar n X Y f)) VT
            --                 q2
            --                 (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1))
            --                (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1
            --                (cPathC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) VT q2 (q_ n X Y f).1 (pb n X).1.2.2.1)
            --        (compPath (cH C.1 if_star2 VT)
            --                (cC C.1 if_star2 (intD (fstar n X Y f)) VT
            --                 q2
            --                 (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT (q_ n X Y f).1 (pb n X).1.2.2.1))
            --                (cC C.1 if_star2 (intD (fstar n X Y f)) VT
            --                 q2
            --                 (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1)
            --                (pb Z.1 (Z.2, cC C.1 (intD Z) (intD Y) V g (cC C.1 (intD Y) (int n X.1) V f X.2))).1.2.2.1
            --                (<i> cC C.1 if_star2 (intD (fstar n X Y f)) VT q2 ((q_ n X Y f).2.2@i))
            --                (q_ Y.1 (fstar n X Y f).2 Z g).2.2)
            -- opaque hole4

            pph : cospanConeHom C.1 (cs n X) pp (pb n X).1
                = transport
                  (<i>cospanConeHom C.1 (cs n X) (ppPath@i) (pb n X).1)
                  ( cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1
                  , hole3
                  , hole4
                  )
            pphPath : Path (cospanConeHom C.1 (cs n X) pp (pb n X).1) ((pb n X).2 pp).1 pph
                  = ((pb n X).2 pp).2 pph
            qPath : Path (cH C.1 if_star (int (suc n) X))
                     (transport (<i>cH C.1 (intD(p1@i)) (int (suc n) X))
                       (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1))
                     (q_ n X Z (cC DC Z Y (n, X.1) g f)).1
                = <i>(pphPath@-i).1
        in (p1,
            substPathP (cH DC (p1@0) (suc n, X)) (cH DC (p1@1) (suc n, X))
                     (<i> cH DC (p1@i) (suc n, X))
                     (cC C.1 if_star2 (intD (fstar n X Y f)) (int (suc n) X) q2 (q_ n X Y f).1)
                     (q_ n X Z (cC DC Z Y (n, X.1) g f)).1
                     qPath)

    qComp' (n : nat) (X : ob (suc n))
           (Y : obD) (f : homD Y (n, X.1))
           (Z : obD) (g : homD Z Y)
        : (let g' : homD Z Y = transport (<_> homD Z Y) g in
          (p0 : Path obD (fstar Y.1 (fstar n X Y f).2 Z g')
                       (fstar n X Z (cC DC Z Y (n, X.1) g f)))
        * PathP (<i> cH DC (p0@i) (suc n, X))
              (cC DC (fstar Y.1 (fstar n X Y f).2 Z g') (fstar n X Y f) (suc n, X)
                (q_ Y.1 (fstar n X Y f).2 Z g').1 (q_ n X Y f).1)
              (q_ n X Z (cC DC Z Y (n, X.1) g f)).1)
        = transport
          (<j> (p0 : Path obD (fstar Y.1 (fstar n X Y f).2 Z (transRefl (homD Z Y) g @ -j))
                            (fstar n X Z (cC DC Z Y (n, X.1) g f)))
             * PathP (<i> cH DC (p0@i) (suc n, X))
                   (cC DC (fstar Y.1 (fstar n X Y f).2 Z (transRefl (homD Z Y) g @ -j)) (fstar n X Y f) (suc n, X)
                     (q_ Y.1 (fstar n X Y f).2 Z (transRefl (homD Z Y) g @ -j)).1 (q_ n X Y f).1)
                   (q_ n X Z (cC DC Z Y (n, X.1) g f)).1)
          (qComp n X Y f Z g)

    hole : CSystem
         = (ob, homD, D, (obSet, ft0, pD, sqD, qPath, qComp'), pbSq)