---

Step * of Lemma discrete-pair-inv_wf

No Annotations
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[X:j⊢]. ∀[b:{X ⊢ _:discr(a:A × B[a])}].
  (discrete-pair-inv(X;b) ∈ {X ⊢ _:Σ discr(A) discrete-family(A;a.B[a])})
BY
{ (Intros
   THEN Unhide
   THEN (Assert λI,alpha. (fst(b(alpha))) ∈ {X ⊢ _:discr(A)} BY
               (D -1
                THEN (MemTypeCD THENW Auto)
                THEN Reduce 0
                THEN All (RepUR  ``discrete-cubical-type cubical-term-at``)
                THEN Auto))
   THEN Unfold `discrete-pair-inv` 0
   THEN MemCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. b : {X ⊢ _:discr(a:A × B[a])}
5. λI,alpha. (fst(b(alpha))) ∈ {X ⊢ _:discr(A)}
⊢ λI,alpha. (snd(b(alpha))) ∈ {X ⊢ _:(discrete-family(A;a.B[a]))[λI,alpha. (fst(b(alpha)))]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[b:\{X  \mvdash{}  \_:discr(a:A  \mtimes{}  B[a])\}].
    (discrete-pair-inv(X;b)  \mmember{}  \{X  \mvdash{}  \_:\mSigma{}  discr(A)  discrete-family(A;a.B[a])\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  \mlambda{}I,alpha.  (fst(b(alpha)))  \mmember{}  \{X  \mvdash{}  \_:discr(A)\}  BY
                          (D  -1
                            THEN  (MemTypeCD  THENW  Auto)
                            THEN  Reduce  0
                            THEN  All  (RepUR    ``discrete-cubical-type  cubical-term-at``)
                            THEN  Auto))
  THEN  Unfold  `discrete-pair-inv`  0
  THEN  MemCD
  THEN  Auto)

---

Home Index