---

Step * 1 of Lemma cubical-id-box_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. alpha : X(I)
10. box : A-open-box(X;(Id_A a b);I;alpha;J;x;i)
11. ¬(fresh-cname(I) ∈ J)
12. A-face-name(term-A-face(a;I;alpha;0)) = <fresh-cname(I), 0> ∈ (nameset([fresh-cname(I) / I]) × ℕ2)
13. A-face-name(term-A-face(b;I;alpha;1)) = <fresh-cname(I), 1> ∈ (nameset([fresh-cname(I) / I]) × ℕ2)
14. ¬(x = fresh-cname(I) ∈ Cname)
15. v : {x:Cname| ¬(x ∈ I)} 
16. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
⊢ (∀f∈lift-id-faces(X;A;I;alpha;box).A-face-compatible(X;A;[v / I];iota(v)(alpha);term-A-face(a;I;alpha;0);f)
     ∧ A-face-compatible(X;A;[v / I];iota(v)(alpha);term-A-face(b;I;alpha;1);f))
BY
{ ((((D 0 THENA Auto)
     THEN (RepUR ``lift-id-faces`` -1 THEN RepUR ``lift-id-faces`` 0)
     THEN (RWO "length-map" (-1) THENA Auto)
     THEN RenameVar `j' (-1)
     THEN (RWO "select-map" 0 THENA Auto)
     THEN Reduce 0
     THEN DVar `box'
     THEN (GenConclTerm ⌜box[j]⌝⋅ THENA Auto)
     THEN RenameVar `fc' (-2)
     THEN RepeatFor 2 (D -2)
     THEN RepUR ``lift-id-face A-face-compatible`` 0
     THEN D 0
     THEN (D 0 THENA Auto)
     THEN (GenConclTerm ⌜set-path-name(X;A;I-[x1];(x1:=i1)(alpha);fresh-cname(I);f2)⌝⋅
           THENA (Auto
                  THEN (DoSubsume THEN Auto)
                  THEN RepUR ``cubical-type-at cubical-identity cubical-path`` 0
                  THEN BLemma `subtype_quotient`
                  THEN Auto)
           )
     THEN Thin (-1)
     THEN RepeatFor 2 (D -1)
     THEN D -3
     THEN Reduce (-2)
     THEN Eliminate ⌜z⌝⋅
     THEN ThinVar `z'
     THEN RepeatFor 2 (D -2)
     THEN Reduce 0)
    THENL [(Thin (-1)
            THEN Thin (-1)
            THEN ThinVar `f2'
            THEN (GenConcl ⌜0 = c ∈ ℕ2⌝⋅ THENA Auto)
            THEN PromoteHyp (-2) 1
            THEN HypSubst' (-1) (-2)
            ⋅
            THEN Thin (-1)
            THEN ThinVar `box'
            THEN RepeatFor 2 (Thin 12))
          ; (Thin (-1)
             THEN Thin (-2)
             THEN ThinVar `f2'
             THEN (GenConcl ⌜1 = c ∈ ℕ2⌝⋅ THENA Auto)
             THEN PromoteHyp (-2) 1
             THEN HypSubst' (-1) (-2)
             ⋅
             THEN SwapVars `a' `b'
             THEN Thin (-1)
             THEN ThinVar `box'
             THEN RepeatFor 2 (Thin 12)
             THEN PromoteHyp 6 5)]
   )
   THEN RenameVar `%%' (-1)
   ) }

1
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)} 
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
⊢ (a(alpha) (fresh-cname(I):=c)(iota(v)(alpha)) (x1:=i1))
= (v2 (x1:=i1)(iota(v)(alpha)) (fresh-cname(I):=c))
∈ A(((x1:=i1) o (fresh-cname(I):=c))(iota(v)(alpha)))

2
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)} 
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
⊢ (a(alpha) (fresh-cname(I):=c)(iota(v)(alpha)) (x1:=i1))
= (v2 (x1:=i1)(iota(v)(alpha)) (fresh-cname(I):=c))
∈ A(((x1:=i1) o (fresh-cname(I):=c))(iota(v)(alpha)))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  J  :  nameset(I)  List
7.  x  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  alpha  :  X(I)
10.  box  :  A-open-box(X;(Id\_A  a  b);I;alpha;J;x;i)
11.  \mneg{}(fresh-cname(I)  \mmember{}  J)
12.  A-face-name(term-A-face(a;I;alpha;0))  =  <fresh-cname(I),  0>
13.  A-face-name(term-A-face(b;I;alpha;1))  =  <fresh-cname(I),  1>
14.  \mneg{}(x  =  fresh-cname(I))
15.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
16.  fresh-cname(I)  =  v
\mvdash{}  (\mforall{}f\mmember{}lift-id-faces(X;A;I;alpha;box).
          A-face-compatible(X;A;[v  /  I];iota(v)(alpha);term-A-face(a;I;alpha;0);f)
          \mwedge{}  A-face-compatible(X;A;[v  /  I];iota(v)(alpha);term-A-face(b;I;alpha;1);f))


By

---

Latex:
((((D  0  THENA  Auto)
      THEN  (RepUR  ``lift-id-faces``  -1  THEN  RepUR  ``lift-id-faces``  0)
      THEN  (RWO  "length-map"  (-1)  THENA  Auto)
      THEN  RenameVar  `j'  (-1)
      THEN  (RWO  "select-map"  0  THENA  Auto)
      THEN  Reduce  0
      THEN  DVar  `box'
      THEN  (GenConclTerm  \mkleeneopen{}box[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
      THEN  RenameVar  `fc'  (-2)
      THEN  RepeatFor  2  (D  -2)
      THEN  RepUR  ``lift-id-face  A-face-compatible``  0
      THEN  D  0
      THEN  (D  0  THENA  Auto)
      THEN  (GenConclTerm  \mkleeneopen{}set-path-name(X;A;I-[x1];(x1:=i1)(alpha);fresh-cname(I);f2)\mkleeneclose{}\mcdot{}
                  THENA  (Auto
                                THEN  (DoSubsume  THEN  Auto)
                                THEN  RepUR  ``cubical-type-at  cubical-identity  cubical-path``  0
                                THEN  BLemma  `subtype\_quotient`
                                THEN  Auto)
                  )
      THEN  Thin  (-1)
      THEN  RepeatFor  2  (D  -1)
      THEN  D  -3
      THEN  Reduce  (-2)
      THEN  Eliminate  \mkleeneopen{}z\mkleeneclose{}\mcdot{}
      THEN  ThinVar  `z'
      THEN  RepeatFor  2  (D  -2)
      THEN  Reduce  0)
    THENL  [(Thin  (-1)
                    THEN  Thin  (-1)
                    THEN  ThinVar  `f2'
                    THEN  (GenConcl  \mkleeneopen{}0  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
                    THEN  PromoteHyp  (-2)  1
                    THEN  HypSubst'  (-1)  (-2)
                    \mcdot{}
                    THEN  Thin  (-1)
                    THEN  ThinVar  `box'
                    THEN  RepeatFor  2  (Thin  12))
                ;  (Thin  (-1)
                      THEN  Thin  (-2)
                      THEN  ThinVar  `f2'
                      THEN  (GenConcl  \mkleeneopen{}1  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
                      THEN  PromoteHyp  (-2)  1
                      THEN  HypSubst'  (-1)  (-2)
                      \mcdot{}
                      THEN  SwapVars  `a'  `b'
                      THEN  Thin  (-1)
                      THEN  ThinVar  `box'
                      THEN  RepeatFor  2  (Thin  12)
                      THEN  PromoteHyp  6  5)]
  )
  THEN  RenameVar  `\%\%'  (-1)
  )

---

Home Index