Step
*
2
2
of Lemma
context-subset-adjoin-subtype
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A@0 : I:fset(ℕ) ⟶ Gamma.A(I) ⟶ Type
5. x1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma.A(I). ∀u:A@0 I a. ((x1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma.A(I). ∀u:A@0 I a.
((x1 I K f ⋅ g a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A@0 K f ⋅ g(a))))
7. {Gamma ⊢ _} ⊆r {Gamma, phi ⊢ _}
8. ∀I:fset(ℕ). (Gamma, phi.A(I) ⊆r Gamma.A(I))
⊢ Gamma, phi.A ⊢ <A@0, x1>
BY
{ (At ⌜𝕌'⌝ MemTypeCD⋅ THEN Reduce 0) }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A@0 : I:fset(ℕ) ⟶ Gamma.A(I) ⟶ Type
5. x1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma.A(I). ∀u:A@0 I a. ((x1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma.A(I). ∀u:A@0 I a.
((x1 I K f ⋅ g a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A@0 K f ⋅ g(a))))
7. {Gamma ⊢ _} ⊆r {Gamma, phi ⊢ _}
8. ∀I:fset(ℕ). (Gamma, phi.A(I) ⊆r Gamma.A(I))
⊢ <A@0, x1> ∈ A@0:I:fset(ℕ) ⟶ Gamma, phi.A(I) ⟶ Type × (I:fset(ℕ)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ a:Gamma, phi.A(I)
⟶ (A@0 I a)
⟶ (A@0 J f(a)))
2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A@0 : I:fset(ℕ) ⟶ Gamma.A(I) ⟶ Type
5. x1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma.A(I). ∀u:A@0 I a. ((x1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma.A(I). ∀u:A@0 I a.
((x1 I K f ⋅ g a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A@0 K f ⋅ g(a))))
7. {Gamma ⊢ _} ⊆r {Gamma, phi ⊢ _}
8. ∀I:fset(ℕ). (Gamma, phi.A(I) ⊆r Gamma.A(I))
⊢ (∀I:fset(ℕ). ∀a:Gamma, phi.A(I). ∀u:A@0 I a. ((x1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, phi.A(I). ∀u:A@0 I a.
((x1 I K f ⋅ g a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A@0 K f ⋅ g(a))))
3
.....wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A@0 : I:fset(ℕ) ⟶ Gamma.A(I) ⟶ Type
5. x1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma.A(I). ∀u:A@0 I a. ((x1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma.A(I). ∀u:A@0 I a.
((x1 I K f ⋅ g a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A@0 K f ⋅ g(a))))
7. {Gamma ⊢ _} ⊆r {Gamma, phi ⊢ _}
8. ∀I:fset(ℕ). (Gamma, phi.A(I) ⊆r Gamma.A(I))
9. AF : A@0:I:fset(ℕ) ⟶ Gamma, phi.A(I) ⟶ Type × (I:fset(ℕ)
⟶ J:fset(ℕ)
⟶ f:J ⟶ I
⟶ a:Gamma, phi.A(I)
⟶ (A@0 I a)
⟶ (A@0 J f(a)))
⊢ istype(let A@0,F = AF
in (∀I:fset(ℕ). ∀a:Gamma, phi.A(I). ∀u:A@0 I a. ((F I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, phi.A(I). ∀u:A@0 I a.
((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A@0 K f ⋅ g(a)))))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. phi : \{Gamma \mvdash{} \_:\mBbbF{}\}
4. A@0 : I:fset(\mBbbN{}) {}\mrightarrow{} Gamma.A(I) {}\mrightarrow{} Type
5. x1 : I:fset(\mBbbN{}) {}\mrightarrow{} J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} a:Gamma.A(I) {}\mrightarrow{} (A@0 I a) {}\mrightarrow{} (A@0 J f(a))
6. (\mforall{}I:fset(\mBbbN{}). \mforall{}a:Gamma.A(I). \mforall{}u:A@0 I a. ((x1 I I 1 a u) = u))
\mwedge{} (\mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:Gamma.A(I). \mforall{}u:A@0 I a.
((x1 I K f \mcdot{} g a u) = (x1 J K g f(a) (x1 I J f a u))))
7. \{Gamma \mvdash{} \_\} \msubseteq{}r \{Gamma, phi \mvdash{} \_\}
8. \mforall{}I:fset(\mBbbN{}). (Gamma, phi.A(I) \msubseteq{}r Gamma.A(I))
\mvdash{} Gamma, phi.A \mvdash{} <A@0, x1>
By
Latex:
(At \mkleeneopen{}\mBbbU{}'\mkleeneclose{} MemTypeCD\mcdot{} THEN Reduce 0)
Home
Index