---

Step * 3 of Lemma empty-cubical-subset

.....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
BY
{ (D -1 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  A  :  Top
3.  B  :  Top
4.  AF  :  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)))
\mvdash{}  let  A,F  =  AF 
    in  (\mforall{}I@0:fset(\mBbbN{}).  \mforall{}a:I,0(I@0).  \mforall{}u:A  I@0  a.    ((F  I@0  I@0  1  a  u)  =  u))
          \mwedge{}  (\mforall{}I@0,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:I,0(I@0).  \mforall{}u:A  I@0  a.
                    ((F  I@0  K  f  \mcdot{}  g  a  u)  =  (F  J  K  g  f(a)  (F  I@0  J  f  a  u))))  \mmember{}  Type


By

---

Latex:
(D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index