---

Step * of Lemma cubical-sigma_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].  X ⊢ Σ A B
BY
{ (Auto THEN Unfold `cubical-sigma` 0 THEN MemTypeCD THEN Try (MemCD) THEN Reduce 0 THEN Auto) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. a : X(I)
6. u : u:A(a) × B((a;u))
⊢ <(fst(u) a 1), (snd(u) (a;fst(u)) 1)> = u ∈ (u:A(a) × B((a;u)))

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. ∀I:Cname List. ∀a:X(I). ∀u:u:A(a) × B((a;u)).  (<(fst(u) a 1), (snd(u) (a;fst(u)) 1)> = u ∈ (u:A(a) × B((a;u))))
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a : X(I)
11. u : u:A(a) × B((a;u))
⊢ <(fst(u) a (f o g)), (snd(u) (a;fst(u)) (f o g))>
= <((fst(u) a f) f(a) g), ((snd(u) (a;fst(u)) f) (f(a);(fst(u) a f)) g)>
∈ (u:A((f o g)(a)) × B(((f o g)(a);u)))

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].    X  \mvdash{}  \mSigma{}  A  B


By

---

Latex:
(Auto  THEN  Unfold  `cubical-sigma`  0  THEN  MemTypeCD  THEN  Try  (MemCD)  THEN  Reduce  0  THEN  Auto)

---

Home Index