Step * 2 1 of Lemma path-eq-equiv


1. CubicalSet
2. {X ⊢ _}
3. {X ⊢ _:A}
4. {X ⊢ _:A}
5. Cname List
6. alpha X(I)
7. z1 Cname
8. ¬(z1 ∈ I)
9. a1 named-path(X;A;a;b;I;alpha;z1)
10. Cname
11. ¬(z ∈ I)
12. b2 named-path(X;A;a;b;I;alpha;z)
13. (a1 iota(z1)(alpha) rename-one-name(z1;z)) b2 ∈ A(iota(z)(alpha))
⊢ ((a1 iota(z1)(alpha) rename-one-name(z1;z)) iota(z)(alpha) rename-one-name(z;z1)) a1 ∈ A(iota(z1)(alpha))
BY
TACTIC:(DVar `a1'
          THEN (InstLemma `cubical-type-ap-morph-comp` 
                [⌜X⌝;⌜A⌝;⌜[z1 I]⌝;⌜[z I]⌝;⌜[z1 I]⌝
                ;⌜rename-one-name(z1;z)⌝;⌜rename-one-name(z;z1)⌝
                ;⌜iota(z1)(alpha)⌝;⌜a1⌝]⋅
                THENA Auto
                )
          }

1
1. CubicalSet
2. {X ⊢ _}
3. {X ⊢ _:A}
4. {X ⊢ _:A}
5. Cname List
6. alpha X(I)
7. z1 Cname
8. ¬(z1 ∈ I)
9. a1 A(iota(z1)(alpha))
10. name-path-endpoints(X;A;a;b;I;alpha;z1;a1)
11. Cname
12. ¬(z ∈ I)
13. b2 named-path(X;A;a;b;I;alpha;z)
14. (a1 iota(z1)(alpha) rename-one-name(z1;z)) b2 ∈ A(iota(z)(alpha))
15. ((a1 iota(z1)(alpha) rename-one-name(z1;z)) rename-one-name(z1;z)(iota(z1)(alpha)) rename-one-name(z;z1))
(a1 iota(z1)(alpha) (rename-one-name(z1;z) rename-one-name(z;z1)))
∈ A((rename-one-name(z1;z) rename-one-name(z;z1))(iota(z1)(alpha)))
⊢ ((a1 iota(z1)(alpha) rename-one-name(z1;z)) iota(z)(alpha) rename-one-name(z;z1)) a1 ∈ A(iota(z1)(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.  alpha  :  X(I)
7.  z1  :  Cname
8.  \mneg{}(z1  \mmember{}  I)
9.  a1  :  named-path(X;A;a;b;I;alpha;z1)
10.  z  :  Cname
11.  \mneg{}(z  \mmember{}  I)
12.  b2  :  named-path(X;A;a;b;I;alpha;z)
13.  (a1  iota(z1)(alpha)  rename-one-name(z1;z))  =  b2
\mvdash{}  ((a1  iota(z1)(alpha)  rename-one-name(z1;z))  iota(z)(alpha)  rename-one-name(z;z1))  =  a1


By


Latex:
TACTIC:(DVar  `a1'
                THEN  (InstLemma  `cubical-type-ap-morph-comp` 
                            [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[z1  /  I]\mkleeneclose{};\mkleeneopen{}[z  /  I]\mkleeneclose{};\mkleeneopen{}[z1  /  I]\mkleeneclose{}
                            ;\mkleeneopen{}rename-one-name(z1;z)\mkleeneclose{};\mkleeneopen{}rename-one-name(z;z1)\mkleeneclose{}
                            ;\mkleeneopen{}iota(z1)(alpha)\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}
                            THENA  Auto
                            )
                )




Home Index