---

Step * 1 1 of Lemma csm-rev-type-line


1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. A1 : I:fset(ℕ) ⟶ (alpha:G(I) × Point(dM(I))) ⟶ Type
4. A2 : I:fset(ℕ)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ a:(alpha:G(I) × Point(dM(I)))
⟶ (A1 I a)
⟶ (A1 J <f(fst(a)), (snd(a) fst(a) f)>)
5. (∀I:fset(ℕ). ∀a:alpha:G(I) × Point(dM(I)). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:alpha:G(I) × Point(dM(I)). ∀u:A1 I a.
     ((A2 I K f ⋅ g a u)
     = (A2 J K g <f(fst(a)), (snd(a) fst(a) f)> (A2 I J f a u))
     ∈ (A1 K <f ⋅ g(fst(a)), (snd(a) fst(a) f ⋅ g)>)))
6. tau : K j⟶ G
7. I : fset(ℕ)
8. J : fset(ℕ)
9. f : J ⟶ I
10. a : alpha:K(I) × Point(dM(I))
11. x : A1 I <tau I (fst(a)), ¬(snd(a))>
⊢ A2 I J f <tau I (fst(a)), ¬(snd(a))> x ∈ A1 J <tau J f(fst(a)), ¬(dM-lift(J;I;f) (snd(a)))>
BY
{ (D -2 THEN Reduce 0) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. A1 : I:fset(ℕ) ⟶ (alpha:G(I) × Point(dM(I))) ⟶ Type
4. A2 : I:fset(ℕ)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ a:(alpha:G(I) × Point(dM(I)))
⟶ (A1 I a)
⟶ (A1 J <f(fst(a)), (snd(a) fst(a) f)>)
5. (∀I:fset(ℕ). ∀a:alpha:G(I) × Point(dM(I)). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:alpha:G(I) × Point(dM(I)). ∀u:A1 I a.
     ((A2 I K f ⋅ g a u)
     = (A2 J K g <f(fst(a)), (snd(a) fst(a) f)> (A2 I J f a u))
     ∈ (A1 K <f ⋅ g(fst(a)), (snd(a) fst(a) f ⋅ g)>)))
6. tau : K j⟶ G
7. I : fset(ℕ)
8. J : fset(ℕ)
9. f : J ⟶ I
10. alpha : K(I)
11. a1 : Point(dM(I))
12. x : A1 I <tau I (fst(<alpha, a1>)), ¬(snd(<alpha, a1>))>
⊢ A2 I J f <tau I alpha, ¬(a1)> x ∈ A1 J <tau J f(alpha), ¬(dM-lift(J;I;f) a1)>

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  A1  :  I:fset(\mBbbN{})  {}\mrightarrow{}  (alpha:G(I)  \mtimes{}  Point(dM(I)))  {}\mrightarrow{}  Type
4.  A2  :  I:fset(\mBbbN{})
{}\mrightarrow{}  J:fset(\mBbbN{})
{}\mrightarrow{}  f:J  {}\mrightarrow{}  I
{}\mrightarrow{}  a:(alpha:G(I)  \mtimes{}  Point(dM(I)))
{}\mrightarrow{}  (A1  I  a)
{}\mrightarrow{}  (A1  J  <f(fst(a)),  (snd(a)  fst(a)  f)>)
5.  (\mforall{}I:fset(\mBbbN{}).  \mforall{}a:alpha:G(I)  \mtimes{}  Point(dM(I)).  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u))
\mwedge{}  (\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:alpha:G(I)  \mtimes{}  Point(dM(I)).  \mforall{}u:A1  I  a.
          ((A2  I  K  f  \mcdot{}  g  a  u)  =  (A2  J  K  g  <f(fst(a)),  (snd(a)  fst(a)  f)>  (A2  I  J  f  a  u))))
6.  tau  :  K  j{}\mrightarrow{}  G
7.  I  :  fset(\mBbbN{})
8.  J  :  fset(\mBbbN{})
9.  f  :  J  {}\mrightarrow{}  I
10.  a  :  alpha:K(I)  \mtimes{}  Point(dM(I))
11.  x  :  A1  I  <tau  I  (fst(a)),  \mneg{}(snd(a))>
\mvdash{}  A2  I  J  f  <tau  I  (fst(a)),  \mneg{}(snd(a))>  x  \mmember{}  A1  J  <tau  J  f(fst(a)),  \mneg{}(dM-lift(J;I;f)  (snd(a)))>


By

---

Latex:
(D  -2  THEN  Reduce  0)

---

Home Index