---

Step * 1 of Lemma rev-rev-type-line


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
⊢ ((A)-)-
= A
∈ (A:I:fset(ℕ) ⟶ Gamma.𝕀(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma.𝕀(I) ⟶ (A I a) ⟶ (A J f(a))))
BY
{ (RepeatFor 2 (DVar `A')
   THEN (RepUR ``rev-type-line`` 0 THEN CsmUnfoldingNotInterval)
   THEN (EqCD THENA Auto)
   THEN Repeat (((FunExt THENA Auto) THEN Reduce 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. I : fset(ℕ)
6. x : Gamma.𝕀(I)
⊢ (A1 I <fst(x), ¬(¬(snd(x)))>) = (A1 I x) ∈ Type

2
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. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : Gamma.𝕀(I)
9. x : A1 I <fst(a), ¬(¬(snd(a)))>
⊢ (A2 I J f <fst(a), ¬(¬(snd(a)))> x) = (A2 I J f a x) ∈ (A1 J <fst(f(a)), ¬(¬(snd(f(a))))>)

3
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. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : Gamma.𝕀(I)
⊢ <fst(a), ¬(¬(snd(a)))> ∈ Gamma.𝕀(I)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
\mvdash{}  ((A)-)-  =  A


By

---

Latex:
(RepeatFor  2  (DVar  `A')
  THEN  (RepUR  ``rev-type-line``  0  THEN  CsmUnfoldingNotInterval)
  THEN  (EqCD  THENA  Auto)
  THEN  Repeat  (((FunExt  THENA  Auto)  THEN  Reduce  0)))

---

Home Index