---

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


1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. A1 : I:fset(ℕ) ⟶ G.𝕀(I) ⟶ Type
4. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:G.𝕀(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. let A,F = <A1, A2> 
   in (∀I:fset(ℕ). ∀a:G.𝕀(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
      ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G.𝕀(I). ∀u:A I a.
           ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))
6. tau : K j⟶ G
⊢ <λI,a. (A1 I <tau I (fst(a)), ¬(snd(a))>), λI,J,f,a,u. (A2 I J f <tau I (fst(a)), ¬(snd(a))> u)>
= <λI,a. (A1 I <tau I (fst(a)), ¬(snd(a))>), λI,J,f,a,u. (A2 I J f <tau I (fst(a)), ¬(snd(a))> u)>
∈ (A:I:fset(ℕ) ⟶ K.<λI,alpha. 𝕀(I), λI,J,f,alpha,w. f(w)>(I) ⟶ Type × (I:fset(ℕ)
                                                ⟶ J:fset(ℕ)
                                                ⟶ f:J ⟶ I
                                                ⟶ a:K.<λI,alpha. 𝕀(I), λI,J,f,alpha,w. f(w)>(I)
                                                ⟶ (A I a)
                                                ⟶ (A J f(a))))
BY
{ (All (RepUR  ``cube-context-adjoin``)
   THEN (All (RWO "interval-type-at") THENA Auto)
   THEN All (RepUR ``interval-presheaf``)
   THEN EqCD
   THEN ((RepeatFor 2 ((FunExt THENA Auto)) THEN Reduce 0) ORELSE Auto)
   THEN ((RepeatFor 3 ((FunExt THENA Auto)) THEN Reduce 0) ORELSE Auto)) }

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

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  A1  :  I:fset(\mBbbN{})  {}\mrightarrow{}  G.\mBbbI{}(I)  {}\mrightarrow{}  Type
4.  A2  :  I:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  a:G.\mBbbI{}(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a))
5.  let  A,F  =  <A1,  A2> 
      in  (\mforall{}I:fset(\mBbbN{}).  \mforall{}a:G.\mBbbI{}(I).  \mforall{}u:A  I  a.    ((F  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:G.\mBbbI{}(I).  \mforall{}u:A  I  a.
                      ((F  I  K  f  \mcdot{}  g  a  u)  =  (F  J  K  g  f(a)  (F  I  J  f  a  u))))
6.  tau  :  K  j{}\mrightarrow{}  G
\mvdash{}  <\mlambda{}I,a.  (A1  I  <tau  I  (fst(a)),  \mneg{}(snd(a))>),  \mlambda{}I,J,f,a,u.  (A2  I  J  f  <tau  I  (fst(a)),  \mneg{}(snd(a))>  u)>
=  <\mlambda{}I,a.  (A1  I  <tau  I  (fst(a)),  \mneg{}(snd(a))>),  \mlambda{}I,J,f,a,u.  (A2  I  J  f  <tau  I  (fst(a)),  \mneg{}(snd(a))>  u)>


By

---

Latex:
(All  (RepUR    ``cube-context-adjoin``)
  THEN  (All  (RWO  "interval-type-at")  THENA  Auto)
  THEN  All  (RepUR  ``interval-presheaf``)
  THEN  EqCD
  THEN  ((RepeatFor  2  ((FunExt  THENA  Auto))  THEN  Reduce  0)  ORELSE  Auto)
  THEN  ((RepeatFor  3  ((FunExt  THENA  Auto))  THEN  Reduce  0)  ORELSE  Auto))

---

Home Index