---

Step * 1 of Lemma empty-cubical-subset


1. I : fset(ℕ)
2. A : Top
3. B : Top
⊢ <A, B> ∈ A:I@0:fset(ℕ) ⟶ I,0(I@0) ⟶ Type × (I@0:fset(ℕ)
                                               ⟶ J:fset(ℕ)
                                               ⟶ f:J ⟶ I@0
                                               ⟶ a:I,0(I@0)
                                               ⟶ (A I@0 a)
                                               ⟶ (A J f(a)))
BY
{ ((MemCD THENA Auto)
   THEN RepeatFor 4 (((FunExt THENA Auto)
                      THEN Try ((RenameVar `X' 4
                                 THEN (InstLemma `empty-cubical-subset-I_cube` [⌜I⌝;⌜X⌝]⋅ THENA Declaration)
                                 THEN D -1
                                 THEN Hypothesis))
                      ))
   ) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  A  :  Top
3.  B  :  Top
\mvdash{}  <A,  B>  \mmember{}  A:I@0:fset(\mBbbN{})  {}\mrightarrow{}  I,0(I@0)  {}\mrightarrow{}  Type  \mtimes{}  (I@0:fset(\mBbbN{})
                                                                                              {}\mrightarrow{}  J:fset(\mBbbN{})
                                                                                              {}\mrightarrow{}  f:J  {}\mrightarrow{}  I@0
                                                                                              {}\mrightarrow{}  a:I,0(I@0)
                                                                                              {}\mrightarrow{}  (A  I@0  a)
                                                                                              {}\mrightarrow{}  (A  J  f(a)))


By

---

Latex:
((MemCD  THENA  Auto)
  THEN  RepeatFor  4  (((FunExt  THENA  Auto)
                                        THEN  Try  ((RenameVar  `X'  4
                                                              THEN  (InstLemma  `empty-cubical-subset-I\_cube`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
                                                                          THENA  Declaration
                                                                          )
                                                              THEN  D  -1
                                                              THEN  Hypothesis))
                                        ))
  )

---

Home Index