---

Step * 2 1 of Lemma Kan-discrete_wf


1. X : CubicalSet
2. T : Type
3. I : Cname List
4. alpha : X(I)
5. J : nameset(I) List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-open-box(X;discr(T);I;alpha;J;x;i)
9. i@0 : ℕ||bx||
⊢ is-A-face(X;discr(T);I;alpha;(λI,alpha,J,x,i,bx. (snd(snd(hd(bx))))) I alpha J x i bx;bx[i@0])
BY
{ (RenameVar `k' (-1)
   THEN D -2
   THEN RepUR ``is-A-face cubical-type-ap-morph`` 0
   THEN RepUR ``discrete-cubical-type cubical-type-at`` 0
   THEN ∀h:hyp. RepUR ``A-face cubical-type-at discrete-cubical-type`` h ) }

1
1. X : CubicalSet
2. T : Type
3. I : Cname List
4. alpha : X(I)
5. J : nameset(I) List
6. x : nameset(I)
7. i : ℕ2
8. bx : (x:nameset(I) × i:ℕ2 × T) List
9. [%1] : A-adjacent-compatible(X;<λI,alpha. T, λI,J,f,alpha,x. x>;I;alpha;bx)
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. k : ℕ||bx||
⊢ let y,b,w = bx[k] in 
(snd(snd(hd(bx)))) = w ∈ T

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  T  :  Type
3.  I  :  Cname  List
4.  alpha  :  X(I)
5.  J  :  nameset(I)  List
6.  x  :  nameset(I)
7.  i  :  \mBbbN{}2
8.  bx  :  A-open-box(X;discr(T);I;alpha;J;x;i)
9.  i@0  :  \mBbbN{}||bx||
\mvdash{}  is-A-face(X;discr(T);I;alpha;(\mlambda{}I,alpha,J,x,i,bx.  (snd(snd(hd(bx)))))  I  alpha  J  x  i  bx;bx[i@0])


By

---

Latex:
(RenameVar  `k'  (-1)
  THEN  D  -2
  THEN  RepUR  ``is-A-face  cubical-type-ap-morph``  0
  THEN  RepUR  ``discrete-cubical-type  cubical-type-at``  0
  THEN  \mforall{}h:hyp.  RepUR  ``A-face  cubical-type-at  discrete-cubical-type``  h  )

---

Home Index