---

Step * of Lemma cubical-type-subtype-cubical-subset

∀[I:fset(ℕ)]. ∀[psi:𝔽(I)].  ({formal-cube(I) ⊢ _} ⊆r {I,psi ⊢ _})
BY
{ (Intros THEN (D 0 THENA Auto) THEN RepeatFor 2 (DVar `x') THEN MemTypeCD THEN All Reduce THEN D -1 THEN All Reduce) }

1
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. A : I@0:fset(ℕ) ⟶ formal-cube(I)(I@0) ⟶ Type
4. x1 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:formal-cube(I)(I@0) ⟶ (A I@0 a) ⟶ (A J f(a))
5. ∀I@0:fset(ℕ). ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.  ((x1 I@0 I@0 1 a u) = u ∈ (A I@0 a))
6. ∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g f(a) (x1 I@0 J f a u)) ∈ (A K f ⋅ g(a)))
⊢ <A, x1> ∈ A:I@0:fset(ℕ) ⟶ I,psi(I@0) ⟶ Type × (I@0:fset(ℕ)
                                                  ⟶ J:fset(ℕ)
                                                  ⟶ f:J ⟶ I@0
                                                  ⟶ a:I,psi(I@0)
                                                  ⟶ (A I@0 a)
                                                  ⟶ (A J f(a)))

2
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. A : I@0:fset(ℕ) ⟶ formal-cube(I)(I@0) ⟶ Type
4. x1 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:formal-cube(I)(I@0) ⟶ (A I@0 a) ⟶ (A J f(a))
5. ∀I@0:fset(ℕ). ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.  ((x1 I@0 I@0 1 a u) = u ∈ (A I@0 a))
6. ∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g f(a) (x1 I@0 J f a u)) ∈ (A K f ⋅ g(a)))
⊢ (∀I@0:fset(ℕ). ∀a:I,psi(I@0). ∀u:A I@0 a.  ((x1 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,psi(I@0). ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g f(a) (x1 I@0 J f a u)) ∈ (A K f ⋅ g(a))))

3
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. A : I@0:fset(ℕ) ⟶ formal-cube(I)(I@0) ⟶ Type
4. x1 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:formal-cube(I)(I@0) ⟶ (A I@0 a) ⟶ (A J f(a))
5. (∀I@0:fset(ℕ). ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.  ((x1 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:formal-cube(I)(I@0). ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g f(a) (x1 I@0 J f a u)) ∈ (A K f ⋅ g(a))))
6. A1 : I@0:fset(ℕ) ⟶ I,psi(I@0) ⟶ Type
7. A2 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:I,psi(I@0) ⟶ (A1 I@0 a) ⟶ (A1 J f(a))
⊢ (∀I@0:fset(ℕ). ∀a:I,psi(I@0). ∀u:A1 I@0 a.  ((A2 I@0 I@0 1 a u) = u ∈ (A1 I@0 a)))
  ∧ (∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:I,psi(I@0). ∀u:A1 I@0 a.
       ((A2 I@0 K f ⋅ g a u) = (A2 J K g f(a) (A2 I@0 J f a u)) ∈ (A1 K f ⋅ g(a)))) ∈ Type

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].    (\{formal-cube(I)  \mvdash{}  \_\}  \msubseteq{}r  \{I,psi  \mvdash{}  \_\})


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `x')
  THEN  MemTypeCD
  THEN  All  Reduce
  THEN  D  -1
  THEN  All  Reduce)

---

Home Index