---

Step * 1 of Lemma cubical-term-equal2


1. [X] : CubicalSet
2. [A] : {X ⊢ _}
3. [u] : {X ⊢ _:A}
⊢ ∀[z:{X ⊢ _:A}]. u = z ∈ {X ⊢ _:A} supposing ∀I:Cname List. ∀a:X(I).  ((u I a) = (z I a) ∈ ((fst(A)) I a))
BY
{ ((Assert ∀I:Cname List. ∀a:X(I).  ((fst(A)) I a ∈ Type) BY
          (Auto THEN RepeatFor 2 (DVar `A') THEN All Reduce THEN Auto))
   THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto)
   THEN DVar `u'
   THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto)) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. u : I:(Cname List) ⟶ a:X(I) ⟶ ((fst(A)) I a)
4. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = A in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))
5. ∀I:Cname List. ∀a:X(I).  ((fst(A)) I a ∈ Type)
6. z : {X ⊢ _:A}
7. ∀I:Cname List. ∀a:X(I).  ((u I a) = (z I a) ∈ ((fst(A)) I a))
⊢ u = z ∈ {X ⊢ _:A}

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet
2.  [A]  :  \{X  \mvdash{}  \_\}
3.  [u]  :  \{X  \mvdash{}  \_:A\}
\mvdash{}  \mforall{}[z:\{X  \mvdash{}  \_:A\}].  u  =  z  supposing  \mforall{}I:Cname  List.  \mforall{}a:X(I).    ((u  I  a)  =  (z  I  a))


By

---

Latex:
((Assert  \mforall{}I:Cname  List.  \mforall{}a:X(I).    ((fst(A))  I  a  \mmember{}  Type)  BY
                (Auto  THEN  RepeatFor  2  (DVar  `A')  THEN  All  Reduce  THEN  Auto))
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  DVar  `u'
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))

---

Home Index