---

Step * 2 of Lemma fiber-point_wf

.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. t : {X ⊢ _:T}
7. c : {X ⊢ _:(Path_A a app(f; t))}
⊢ c ∈ {X ⊢ _:((Path_(A)p (a)p app((f)p; q)))[t]}
BY
{ (InferEqualTypeUp THEN Try (Trivial) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. t : {X ⊢ _:T}
7. c : {X ⊢ _:(Path_A a app(f; t))}
⊢ (X ⊢ Path_A a app(f; t)) = ((Path_(A)p (a)p app((f)p; q)))[t] ∈ cubical-type{[j' | i']:l}(X)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  f  :  \{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  t  :  \{X  \mvdash{}  \_:T\}
7.  c  :  \{X  \mvdash{}  \_:(Path\_A  a  app(f;  t))\}
\mvdash{}  c  \mmember{}  \{X  \mvdash{}  \_:((Path\_(A)p  (a)p  app((f)p;  q)))[t]\}


By

---

Latex:
(InferEqualTypeUp  THEN  Try  (Trivial)  THEN  EqCDA)

---

Home Index