Step
*
2
1
of Lemma
context-subset-type-subtype
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A1 : I:fset(ℕ) ⟶ G(I) ⟶ 𝕌{j}
4. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:G(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. ∀I:fset(ℕ). ∀a:G(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
6. ∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
7. I : fset(ℕ)
8. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
9. J : fset(ℕ)
10. ∀K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
11. K : fset(ℕ)
12. ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
13. f : J ⟶ I
14. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
15. g : K ⟶ J
16. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
17. a : G, phi(I)
18. ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
19. u : A1 I a
20. (A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a))
⊢ (A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a))
BY
{ (NthHypSq (-1) THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }
1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A1 : I:fset(ℕ) ⟶ G(I) ⟶ 𝕌{j}
4. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:G(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. ∀I:fset(ℕ). ∀a:G(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
6. ∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
7. I : fset(ℕ)
8. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
9. J : fset(ℕ)
10. ∀K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
11. K : fset(ℕ)
12. ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
13. f : J ⟶ I
14. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
15. g : K ⟶ J
16. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
17. a : G, phi(I)
18. ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
19. u : A1 I a
20. (A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a))
⊢ f ⋅ g(a) ~ f ⋅ g(a)
2
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A1 : I:fset(ℕ) ⟶ G(I) ⟶ 𝕌{j}
4. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:G(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. ∀I:fset(ℕ). ∀a:G(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
6. ∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
7. I : fset(ℕ)
8. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
9. J : fset(ℕ)
10. ∀K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a.
((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
11. K : fset(ℕ)
12. ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
13. f : J ⟶ I
14. ∀g:K ⟶ J. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
15. g : K ⟶ J
16. ∀a:G(I). ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
17. a : G, phi(I)
18. ∀u:A1 I a. ((A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a)))
19. u : A1 I a
20. (A2 I K f ⋅ g a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K f ⋅ g(a))
⊢ A2 J K g f(a) ~ A2 J K g f(a)
Latex:
Latex:
1. G : CubicalSet\{j\}
2. phi : \{G \mvdash{} \_:\mBbbF{}\}
3. A1 : I:fset(\mBbbN{}) {}\mrightarrow{} G(I) {}\mrightarrow{} \mBbbU{}\{j\}
4. A2 : I:fset(\mBbbN{}) {}\mrightarrow{} J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} a:G(I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a))
5. \mforall{}I:fset(\mBbbN{}). \mforall{}a:G(I). \mforall{}u:A1 I a. ((A2 I I 1 a u) = u)
6. \mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:G(I). \mforall{}u:A1 I a.
((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
7. I : fset(\mBbbN{})
8. \mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:G(I). \mforall{}u:A1 I a.
((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
9. J : fset(\mBbbN{})
10. \mforall{}K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:G(I). \mforall{}u:A1 I a.
((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
11. K : fset(\mBbbN{})
12. \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:G(I). \mforall{}u:A1 I a. ((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
13. f : J {}\mrightarrow{} I
14. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:G(I). \mforall{}u:A1 I a. ((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
15. g : K {}\mrightarrow{} J
16. \mforall{}a:G(I). \mforall{}u:A1 I a. ((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
17. a : G, phi(I)
18. \mforall{}u:A1 I a. ((A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u)))
19. u : A1 I a
20. (A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u))
\mvdash{} (A2 I K f \mcdot{} g a u) = (A2 J K g f(a) (A2 I J f a u))
By
Latex:
(NthHypSq (-1) THEN RepeatFor 2 ((EqCD THEN Try (Trivial))))
Home
Index