---

Step * 1 of Lemma transprt-fun_wf

.....assertion..... 
1. Gamma : CubicalSet{j}
2. Gamma.𝕀 j⊢
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 +⊢ Compositon(A)
⊢ transprt-fun(Gamma;A;cA) ∈ {Gamma ⊢ _:Π(A)[0(𝕀)] ((A)[1(𝕀)])p}
BY
{ (Unfold `transprt-fun` 0
   THEN (InstLemma `cubical-lambda_wf` [⌜Gamma⌝;⌜(A)[0(𝕀)]⌝;⌜((A)[1(𝕀)])p⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜transprt(Gamma.(A)[0(𝕀)];(cA)p+;q)⌝] (-1)⋅ THENM Trivial)) }

1
.....wf..... 
1. Gamma : CubicalSet{j}
2. Gamma.𝕀 j⊢
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 +⊢ Compositon(A)
5. ∀[b:{Gamma.(A)[0(𝕀)] ⊢ _:((A)[1(𝕀)])p}]. ((λb) ∈ {Gamma ⊢ _:Π(A)[0(𝕀)] ((A)[1(𝕀)])p})
⊢ transprt(Gamma.(A)[0(𝕀)];(cA)p+;q) ∈ {Gamma.(A)[0(𝕀)] ⊢ _:((A)[1(𝕀)])p}

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  Gamma.\mBbbI{}  j\mvdash{}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  cA  :  Gamma.\mBbbI{}  +\mvdash{}  Compositon(A)
\mvdash{}  transprt-fun(Gamma;A;cA)  \mmember{}  \{Gamma  \mvdash{}  \_:\mPi{}(A)[0(\mBbbI{})]  ((A)[1(\mBbbI{})])p\}


By

---

Latex:
(Unfold  `transprt-fun`  0
  THEN  (InstLemma  `cubical-lambda\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}(A)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}((A)[1(\mBbbI{})])p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}transprt(Gamma.(A)[0(\mBbbI{})];(cA)p+;q)\mkleeneclose{}]  (-1)\mcdot{}  THENM  Trivial))

---

Home Index