---

Step * 1 2 1 1 2 2 1 1 1 1 1 1 1 1 2 2 1 7 6 1 of Lemma csm-cubical-id-is-equiv


1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
11. {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}
= {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
∈ 𝕌{[i' | j']}
12. id-fiber-center(K;(A)tau) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}
13. [id-fiber-center(K;(A)tau)] ∈ K.(A)tau ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14. ((λid-fiber-contraction(G;A)))tau+
= (λ(id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau ⊢ _:(ΠΣ (A)p (Path_((A)p)p (q)p q) (Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau+}
15. K.(A)tau ⊢ Fiber((cubical-id-fun(K))p;q) = (Σ (A)p (Path_((A)p)p (q)p q))tau+ ∈ {K.(A)tau ⊢ _}
16. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ij⟶ G.A.Σ (A)p (Path_((A)p)p (q)p q).
    ∀A@0:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _}. ∀a,b:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
17. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                 1(K.(A)tau) ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p.
    ∀A@0:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _}.
    ∀a,b:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
⊢ cubical-type{[i' | j']:l}(K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)
                            )(Path_((Σ (A)p (Path_((A)p)p (q)p q))p)(tau+ o p;q) ((id-fiber-center(G;A))p)(tau+ o p;q)
                                   (q)(tau+ o p;q))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
11. {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}
= {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
∈ 𝕌{[i' | j']}
12. id-fiber-center(K;(A)tau) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}
13. [id-fiber-center(K;(A)tau)] ∈ K.(A)tau ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14. ((λid-fiber-contraction(G;A)))tau+
= (λ(id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau ⊢ _:(ΠΣ (A)p (Path_((A)p)p (q)p q) (Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau+}
15. K.(A)tau ⊢ Fiber((cubical-id-fun(K))p;q) = (Σ (A)p (Path_((A)p)p (q)p q))tau+ ∈ {K.(A)tau ⊢ _}
16. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ij⟶ G.A.Σ (A)p (Path_((A)p)p (q)p q).
    ∀A@0:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _}. ∀a,b:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
17. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                 1(K.(A)tau) ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p.
    ∀A@0:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _}.
    ∀a,b:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
⊢ K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) cubical_set{[j | i]:l}

2
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
11. {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}
= {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
∈ 𝕌{[i' | j']}
12. id-fiber-center(K;(A)tau) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}
13. [id-fiber-center(K;(A)tau)] ∈ K.(A)tau ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14. ((λid-fiber-contraction(G;A)))tau+
= (λ(id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau ⊢ _:(ΠΣ (A)p (Path_((A)p)p (q)p q) (Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau+}
15. K.(A)tau ⊢ Fiber((cubical-id-fun(K))p;q) = (Σ (A)p (Path_((A)p)p (q)p q))tau+ ∈ {K.(A)tau ⊢ _}
16. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ij⟶ G.A.Σ (A)p (Path_((A)p)p (q)p q).
    ∀A@0:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _}. ∀a,b:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
17. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                 1(K.(A)tau) ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p.
    ∀A@0:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _}.
    ∀a,b:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
⊢ cubical-type{[j' | i']:l}(K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)
                            )((Σ (A)p (Path_((A)p)p (q)p q))p)(tau+ o p;q)

3
.....subterm..... T:t
3:n
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
11. {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}
= {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
∈ 𝕌{[i' | j']}
12. id-fiber-center(K;(A)tau) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}
13. [id-fiber-center(K;(A)tau)] ∈ K.(A)tau ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14. ((λid-fiber-contraction(G;A)))tau+
= (λ(id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau ⊢ _:(ΠΣ (A)p (Path_((A)p)p (q)p q) (Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau+}
15. K.(A)tau ⊢ Fiber((cubical-id-fun(K))p;q) = (Σ (A)p (Path_((A)p)p (q)p q))tau+ ∈ {K.(A)tau ⊢ _}
16. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ij⟶ G.A.Σ (A)p (Path_((A)p)p (q)p q).
    ∀A@0:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _}. ∀a,b:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
17. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                 1(K.(A)tau) ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p.
    ∀A@0:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _}.
    ∀a,b:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
⊢ ((id-fiber-center(G;A))p)(tau+ o p;q) ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _
                                           :((Σ (A)p (Path_((A)p)p (q)p q))p)(tau+ o p;q)}

4
.....subterm..... T:t
4:n
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
11. {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}
= {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
∈ 𝕌{[i' | j']}
12. id-fiber-center(K;(A)tau) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}
13. [id-fiber-center(K;(A)tau)] ∈ K.(A)tau ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14. ((λid-fiber-contraction(G;A)))tau+
= (λ(id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau ⊢ _:(ΠΣ (A)p (Path_((A)p)p (q)p q) (Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau+}
15. K.(A)tau ⊢ Fiber((cubical-id-fun(K))p;q) = (Σ (A)p (Path_((A)p)p (q)p q))tau+ ∈ {K.(A)tau ⊢ _}
16. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ij⟶ G.A.Σ (A)p (Path_((A)p)p (q)p q).
    ∀A@0:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _}. ∀a,b:{G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
17. ∀s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                 1(K.(A)tau) ij⟶ K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p.
    ∀A@0:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _}.
    ∀a,b:{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p ⊢ _:A@0}.
      (((Path_A@0 a b))s
      = (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ Path_(A@0)s (a)s (b)s)
      ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _})
⊢ (q)(tau+ o p;q) ∈ {K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau) ⊢ _
                     :((Σ (A)p (Path_((A)p)p (q)p q))p)(tau+ o p;q)}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  G
4.  A  :  \{G  \mvdash{}  \_\}
5.  (cubical-id-fun(G))p  =  cubical-id-fun(G.A)
6.  cubical-id-fun(G)  \mmember{}  \{G  \mvdash{}  \_:(A  {}\mrightarrow{}  A)\}
7.  G.A  \mvdash{}  Fiber((cubical-id-fun(G))p;q)  =  \mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q)
8.  (cubical-id-fun(G))p  =  cubical-id-fun(G.A)
9.  ((\mlambda{}contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
=  (\mlambda{}(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
10.  (cubical-id-fun(K))p  \mmember{}  \{K.(A)tau  \mvdash{}  \_:(((A)tau)p  {}\mrightarrow{}  ((A)tau)p)\}
11.  \{K  \mvdash{}  \_:\mPi{}(A)tau  Contractible(Fiber((cubical-id-fun(K))p;q))\}
=  \{K  \mvdash{}  \_:(\mPi{}A  Contractible(Fiber((cubical-id-fun(G))p;q)))tau\}
12.  id-fiber-center(K;(A)tau)  \mmember{}  \{K.(A)tau  \mvdash{}  \_:Fiber((cubical-id-fun(K))p;q)\}
13.  [id-fiber-center(K;(A)tau)]  \mmember{}  K.(A)tau  ij{}\mrightarrow{}  K.(A)tau.Fiber((cubical-id-fun(K))p;q)
14.  ((\mlambda{}id-fiber-contraction(G;A)))tau+  =  (\mlambda{}(id-fiber-contraction(G;A))tau++)
15.  K.(A)tau  \mvdash{}  Fiber((cubical-id-fun(K))p;q)  =  (\mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q))tau+
16.  \mforall{}s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)  ij{}\mrightarrow{}  G.A.\mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q).
        \mforall{}A@0:\{G.A.\mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q)  \mvdash{}  \_\}.  \mforall{}a,b:\{G.A.\mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q)  \mvdash{}  \_:A@0\}.
            (((Path\_A@0  a  b))s
            =  (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)  \mvdash{}  Path\_(A@0)s  (a)s  (b)s))
17.  \mforall{}s:K.(A)tau.(Fiber((cubical-id-fun(K))p;q))
                                  1(K.(A)tau)  ij{}\mrightarrow{}  K.(A)tau.Fiber((cubical-id-fun(K))p;
                                                                                                  q).(Fiber((cubical-id-fun(K))p;q))p.
        \mforall{}A@0:\{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p  \mvdash{}  \_\}.
        \mforall{}a,b:\{K.(A)tau.Fiber((cubical-id-fun(K))p;q).(Fiber((cubical-id-fun(K))p;q))p  \mvdash{}  \_:A@0\}.
            (((Path\_A@0  a  b))s
            =  (K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)  \mvdash{}  Path\_(A@0)s  (a)s  (b)s))
\mvdash{}  cubical-type\{[i'  |  j']:l\}(K.(A)tau.(Fiber((cubical-id-fun(K))p;q))1(K.(A)tau)
                                                        )(Path\_((\mSigma{}  (A)p  (Path\_((A)p)p  (q)p  q))p)(tau+  o  p;q)
                                                                      ((id-fiber-center(G;A))p)(tau+  o  p;q)  (q)(tau+  o  p;q))


By

---

Latex:
MemCD

---

Home Index