---

Step * of Lemma cubical-fst_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].  (p.1 ∈ {X ⊢ _:A})
BY
{ (ProveWfLemma THEN D -1 THEN MemTypeCD THEN Reduce 0) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. p : I:(Cname List) ⟶ a:X(I) ⟶ ((fst(Σ A B)) I a)
5. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = Σ A B in (F I J f a (p I a)) = (p J f(a)) ∈ (A J f(a))
⊢ λI,a. (fst((p I a))) ∈ I:(Cname List) ⟶ a:X(I) ⟶ ((fst(A)) I a)

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. p : I:(Cname List) ⟶ a:X(I) ⟶ ((fst(Σ A B)) I a)
5. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = Σ A B in (F I J f a (p I a)) = (p J f(a)) ∈ (A J f(a))
⊢ ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).
    let A,F = A 
    in (F I J f a (fst((p I a)))) = (fst((p J f(a)))) ∈ (A J f(a))

3
.....wf..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. p : I:(Cname List) ⟶ a:X(I) ⟶ ((fst(Σ A B)) I a)
5. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = Σ A B in (F I J f a (p I a)) = (p J f(a)) ∈ (A J f(a))
6. u : I:(Cname List) ⟶ a:X(I) ⟶ ((fst(A)) I a)
⊢ ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = A in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a)) ∈ Type

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[p:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].    (p.1  \mmember{}  \{X  \mvdash{}  \_:A\})


By

---

Latex:
(ProveWfLemma  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index