---

Step * 1 1 of Lemma discrete-pair-inv-property


1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. b : {X ⊢ _:discr(a:A × B[a])}
5. I : fset(ℕ)
6. a : X(I)
⊢ b(a) = <fst(b(a)), snd(b(a))> ∈ (a:A × B[a])
BY
{ ((GenConclTerm ⌜b(a)⌝⋅ THENA Auto) THEN RepUR ``discrete-cubical-type`` -2 THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  X  :  CubicalSet\{j\}
4.  b  :  \{X  \mvdash{}  \_:discr(a:A  \mtimes{}  B[a])\}
5.  I  :  fset(\mBbbN{})
6.  a  :  X(I)
\mvdash{}  b(a)  =  <fst(b(a)),  snd(b(a))>


By

---

Latex:
((GenConclTerm  \mkleeneopen{}b(a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``discrete-cubical-type``  -2
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index