---

Step * 1 3 of Lemma subset-iota-is-id

.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ (v)iota ∈ A:I:fset(ℕ) ⟶ H, phi(I) ⟶ Type × (I:fset(ℕ)
                                               ⟶ J:fset(ℕ)
                                               ⟶ f:J ⟶ I
                                               ⟶ a:H, phi(I)
                                               ⟶ (A I a)
                                               ⟶ (A J f(a)))
BY
{ (RepeatFor 2 (DVar `v') THEN All Reduce THEN RepUR ``csm-ap-type csm-ap subset-iota`` 0) }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. A : I:fset(ℕ) ⟶ H, phi(I) ⟶ Type
4. v1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:H, phi(I) ⟶ (A I a) ⟶ (A J f(a))
5. (∀I:fset(ℕ). ∀a:H, phi(I). ∀u:A I a.  ((v1 I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:H, phi(I). ∀u:A I a.
     ((v1 I K f ⋅ g a u) = (v1 J K g f(a) (v1 I J f a u)) ∈ (A K f ⋅ g(a))))
⊢ <λI,a. (A I a), λI,J,f,a,u. (v1 I J f a u)> ∈ A:I:fset(ℕ) ⟶ H, phi(I) ⟶ Type × (I:fset(ℕ)
                                                                     ⟶ J:fset(ℕ)
                                                                     ⟶ f:J ⟶ I
                                                                     ⟶ a:H, phi(I)
                                                                     ⟶ (A I a)
                                                                     ⟶ (A J f(a)))

---

Latex:

---

Latex:
.....wf..... 
1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  v  :  \{H,  phi  \mvdash{}  \_\}
\mvdash{}  (v)iota  \mmember{}  A:I:fset(\mBbbN{})  {}\mrightarrow{}  H,  phi(I)  {}\mrightarrow{}  Type  \mtimes{}  (I:fset(\mBbbN{})
                                                                                              {}\mrightarrow{}  J:fset(\mBbbN{})
                                                                                              {}\mrightarrow{}  f:J  {}\mrightarrow{}  I
                                                                                              {}\mrightarrow{}  a:H,  phi(I)
                                                                                              {}\mrightarrow{}  (A  I  a)
                                                                                              {}\mrightarrow{}  (A  J  f(a)))


By

---

Latex:
(RepeatFor  2  (DVar  `v')  THEN  All  Reduce  THEN  RepUR  ``csm-ap-type  csm-ap  subset-iota``  0)

---

Home Index