---

Step * 1 of Lemma context-subset-ap-iota


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

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

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  (A)iota  =  A


By

---

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

---

Home Index