---

Step * of Lemma fiber-point_wf

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[f:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[t:{X ⊢ _:T}]. ∀[c:{X ⊢ _:(Path_A a app(f; t))}].
  (fiber-point(t;c) ∈ {X ⊢ _:Fiber(f;a)})
BY
{ (Auto THEN RepUR ``fiber-point cubical-fiber`` 0 THEN MemCD THEN Try (Trivial)) }

1
.....implicit subterm..... 
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.T ⊢ (Path_(A)p (a)p app((f)p; q))

2
.....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]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[t:\{X  \mvdash{}  \_:T\}].
\mforall{}[c:\{X  \mvdash{}  \_:(Path\_A  a  app(f;  t))\}].
    (fiber-point(t;c)  \mmember{}  \{X  \mvdash{}  \_:Fiber(f;a)\})


By

---

Latex:
(Auto  THEN  RepUR  ``fiber-point  cubical-fiber``  0  THEN  MemCD  THEN  Try  (Trivial))

---

Home Index