---

Step * of Lemma transprt-fun_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 +⊢ Compositon(A)].
  (transprt-fun(Gamma;A;cA) ∈ {Gamma ⊢ _:((A)[0(𝕀)] ⟶ (A)[1(𝕀)])})
BY
{ (Intro
   THEN (Assert Gamma.𝕀 j⊢ BY
               Auto)
   THEN Auto
   THEN Assert ⌜transprt-fun(Gamma;A;cA) ∈ {Gamma ⊢ _:Π(A)[0(𝕀)] ((A)[1(𝕀)])p}⌝⋅) }

1
.....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}

2
1. Gamma : CubicalSet{j}
2. Gamma.𝕀 j⊢
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 +⊢ Compositon(A)
5. transprt-fun(Gamma;A;cA) ∈ {Gamma ⊢ _:Π(A)[0(𝕀)] ((A)[1(𝕀)])p}
⊢ transprt-fun(Gamma;A;cA) ∈ {Gamma ⊢ _:((A)[0(𝕀)] ⟶ (A)[1(𝕀)])}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  +\mvdash{}  Compositon(A)].
    (transprt-fun(Gamma;A;cA)  \mmember{}  \{Gamma  \mvdash{}  \_:((A)[0(\mBbbI{})]  {}\mrightarrow{}  (A)[1(\mBbbI{})])\})


By

---

Latex:
(Intro
  THEN  (Assert  Gamma.\mBbbI{}  j\mvdash{}  BY
                          Auto)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}transprt-fun(Gamma;A;cA)  \mmember{}  \{Gamma  \mvdash{}  \_:\mPi{}(A)[0(\mBbbI{})]  ((A)[1(\mBbbI{})])p\}\mkleeneclose{}\mcdot{})

---

Home Index