---

Step * 2 of Lemma transprt-fun_wf


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(𝕀)])}
BY
{ (InferEqualType THEN Try (Trivial)) }

1
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}
⊢ {Gamma ⊢ _:Π(A)[0(𝕀)] ((A)[1(𝕀)])p} = {Gamma ⊢ _:((A)[0(𝕀)] ⟶ (A)[1(𝕀)])} ∈ 𝕌{[i' | j']}

---

Latex:

---

Latex:

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


By

---

Latex:
(InferEqualType  THEN  Try  (Trivial))

---

Home Index