---

Step * of Lemma empty-cubical-subset

∀[I:fset(ℕ)]. ∀[A,B:Top].  I,0 ⊢ <A, B>
BY
{ (Auto THEN MemTypeCD) }

1
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)))

2
.....set predicate..... 
1. I : fset(ℕ)
2. A : Top
3. B : Top
⊢ let A,F = <A, B> 
  in (∀I@0:fset(ℕ). ∀a:I,0(I@0). ∀u:A I@0 a.  ((F I@0 I@0 1 a u) = u ∈ (A I@0 a)))
     ∧ (∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:I,0(I@0). ∀u:A I@0 a.
          ((F I@0 K f ⋅ g a u) = (F J K g f(a) (F I@0 J f a u)) ∈ (A K f ⋅ g(a))))

3
.....wf..... 
1. I : fset(ℕ)
2. A : Top
3. B : Top
4. AF : 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)))
⊢ let A,F = AF 
  in (∀I@0:fset(ℕ). ∀a:I,0(I@0). ∀u:A I@0 a.  ((F I@0 I@0 1 a u) = u ∈ (A I@0 a)))
     ∧ (∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:I,0(I@0). ∀u:A I@0 a.
          ((F I@0 K f ⋅ g a u) = (F J K g f(a) (F I@0 J f a u)) ∈ (A K f ⋅ g(a)))) ∈ Type

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[A,B:Top].    I,0  \mvdash{}  <A,  B>


By

---

Latex:
(Auto  THEN  MemTypeCD)

---

Home Index