---

Step * of Lemma csm-fiber-comp-sq

∀[G,A,T,a,cA,cT,H,s,f:Top].  ((fiber-comp(G;T;A;f;a;cT;cA))s ~ fiber-comp(H;(T)s;(A)s;(f)s;(a)s;(cT)s;(cA)s))
BY
{ (Intros
   THEN Unfold `fiber-comp` 0
   THEN (RWW  "csm-sigma_comp csm-path_comp csm-cubical-app" 0 THENA Auto)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN RepUR ``csm-comp-structure`` 0
   THEN Try ((CsmUnfolding THEN Trivial))) }

1
1. G : Top
2. A : Top
3. T : Top
4. a : Top
5. cA : Top
6. cT : Top
7. H : Top
8. s : Top
9. f : Top
⊢ ((A)p)s+ ~ ((A)s)p

---

Latex:

---

Latex:
\mforall{}[G,A,T,a,cA,cT,H,s,f:Top].
    ((fiber-comp(G;T;A;f;a;cT;cA))s  \msim{}  fiber-comp(H;(T)s;(A)s;(f)s;(a)s;(cT)s;(cA)s))


By

---

Latex:
(Intros
  THEN  Unfold  `fiber-comp`  0
  THEN  (RWW    "csm-sigma\_comp  csm-path\_comp  csm-cubical-app"  0  THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  RepUR  ``csm-comp-structure``  0
  THEN  Try  ((CsmUnfolding  THEN  Trivial)))

---

Home Index