---

Step * of Lemma fst-transprt-sigma

No Annotations
∀[X:j⊢]. ∀[A:{X.𝕀 ⊢ _}]. ∀[B:{X.𝕀.A ⊢ _}]. ∀[cA:X.𝕀 +⊢ Compositon(A)]. ∀[cB:X.𝕀.A +⊢ Compositon(B)].
∀[pr:{X ⊢ _:(Σ A B)[0(𝕀)]}].
  (transprt(X;sigma_comp(cA;cB);pr).1 = transprt(X;cA;pr.1) ∈ {X ⊢ _:(A)[1(𝕀)]})
BY
{ (Intros
   THEN (Subst' transprt(X;sigma_comp(cA;cB);pr).1 ~ (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] 0
         THENA (RepUR ``transprt comp_term sigma_comp let cubical-pair cubical-fst`` 0
                THEN RepUR ``fill_term csm-ap-term`` 0
                THEN CsmUnfoldingComp)
         )
   THEN (((Assert (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A) BY
                 (InferEqualTypeGen THENL [(EqCDA THEN Auto); Auto]))
          THEN Assert ⌜pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}⌝⋅
          )
   THENM ((InstLemma `fill_term_1` [⌜X⌝;⌜0(𝔽)⌝;⌜A⌝]⋅ THENA Auto)
          THEN (RWO "csm-face-0" (-1) THENA Auto)
          THEN (InstHyp [⌜discr(⋅).1⌝;⌜pr.1⌝;⌜(cA)1(X.𝕀)⌝] (-1)⋅ THENA Auto))
   )) }

1
.....assertion..... 
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
⊢ pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}

2
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
8. pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}
9. ∀[u:{X.𝕀, 0(𝔽) ⊢ _:A}]. ∀[a0:{X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ u[0]]}]. ∀[cT:X.𝕀 ⊢ Compositon(A)].
     ((fill cT [0(𝔽) ⊢→ u] a0)[1(𝕀)] = comp cT [0(𝔽) ⊢→ u] a0 ∈ {X ⊢ _:(A)[1(𝕀)]})
10. (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}
⊢ (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = transprt(X;cA;pr.1) ∈ {X ⊢ _:(A)[1(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[B:\{X.\mBbbI{}.A  \mvdash{}  \_\}].  \mforall{}[cA:X.\mBbbI{}  +\mvdash{}  Compositon(A)].  \mforall{}[cB:X.\mBbbI{}.A  +\mvdash{}  Compositon(B)].
\mforall{}[pr:\{X  \mvdash{}  \_:(\mSigma{}  A  B)[0(\mBbbI{})]\}].
    (transprt(X;sigma\_comp(cA;cB);pr).1  =  transprt(X;cA;pr.1))


By

---

Latex:
(Intros
  THEN  (Subst'  transprt(X;sigma\_comp(cA;cB);pr).1 
              \msim{}  (fill  (cA)1(X.\mBbbI{})  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{}).1]  pr.1)[1(\mBbbI{})]  0
              THENA  (RepUR  ``transprt  comp\_term  sigma\_comp  let  cubical-pair  cubical-fst``  0
                            THEN  RepUR  ``fill\_term  csm-ap-term``  0
                            THEN  CsmUnfoldingComp)
              )
  THEN  (((Assert  (cA)1(X.\mBbbI{})  \mmember{}  X.\mBbbI{}  +\mvdash{}  Compositon(A)  BY
                              (InferEqualTypeGen  THENL  [(EqCDA  THEN  Auto);  Auto]))
                THEN  Assert  \mkleeneopen{}pr.1  \mmember{}  \{X  \mvdash{}  \_:(A)[0(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  discr(\mcdot{}).1[0]]\}\mkleeneclose{}\mcdot{}
                )
  THENM  ((InstLemma  `fill\_term\_1`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}0(\mBbbF{})\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (RWO  "csm-face-0"  (-1)  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}discr(\mcdot{}).1\mkleeneclose{};\mkleeneopen{}pr.1\mkleeneclose{};\mkleeneopen{}(cA)1(X.\mBbbI{})\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))
  ))

---

Home Index