---

Step * of Lemma cubical-pair-eta

No Annotations
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:Σ A B}].  (cubical-pair(w.1;w.2) = w ∈ {X ⊢ _:Σ A B})
BY
{ (Intros
   THEN Symmetry
   THEN BLemma `cubical-term-equal`
   THEN ((RepeatFor 2 ((Ext THENA Auto))
          THEN RepUR ``cubical-fst cubical-snd cubical-pair cubical-sigma`` 0
          THEN DVar `w'⋅
          THEN RepUR ``cubical-sigma`` 4
          THEN GenConclAtAddr [2]
          THEN DVar `v'
          THEN Reduce 0
          THEN Auto)⋅
   ORELSE Auto
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].    (cubical-pair(w.1;w.2)  =  w)


By

---

Latex:
(Intros
  THEN  Symmetry
  THEN  BLemma  `cubical-term-equal`
  THEN  ((RepeatFor  2  ((Ext  THENA  Auto))
                THEN  RepUR  ``cubical-fst  cubical-snd  cubical-pair  cubical-sigma``  0
                THEN  DVar  `w'\mcdot{}
                THEN  RepUR  ``cubical-sigma``  4
                THEN  GenConclAtAddr  [2]
                THEN  DVar  `v'
                THEN  Reduce  0
                THEN  Auto)\mcdot{}
  ORELSE  Auto
  ))

---

Home Index