---

Step * of Lemma discrete-cubical-term-is-constant-on-irr-face

No Annotations
∀[T:Type]. ∀[I:fset(ℕ)]. ∀[as,bs:fset(names(I))].
  ∀[t:{I,irr_face(I;as;bs) ⊢ _:discr(T)}]. (t = discr(t(irr-face-morph(I;as;bs))) ∈ {I,irr_face(I;as;bs) ⊢ _:discr(T)}) 
  supposing ↑fset-disjoint(NamesDeq;as;bs)
BY
{ (Auto
   THEN (InstLemma `discrete-cubical-term-is-map` [⌜T⌝;⌜I,irr_face(I;as;bs)⌝]⋅ THENA Auto)
   THEN D -1
   THEN SubsumeC ⌜I,irr_face(I;as;bs) ij⟶ discrete-cube(T)⌝⋅
   THEN Try (Trivial)
   THEN (Assert irr-face-morph(I;as;bs) ∈ {f:I ⟶ I| (irr_face(I;as;bs) f) = 1}  BY
               (MemTypeCD THEN EAuto 1))
   THEN (Enough to prove ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].
                           ((irr_face(I;as;bs) g) = 1 ⇒ (g = irr-face-morph(I;as;bs) ⋅ g ∈ J ⟶ I))
          Because (InstLemma `discrete-map-is-constant2` [⌜parm{i|j}⌝;⌜T⌝;⌜I⌝;⌜irr_face(I;as;bs)⌝;⌜t⌝;
                   ⌜irr-face-morph(I;as;bs)⌝]⋅
                   THEN Auto
                   ))) }

1
1. T : Type
2. I : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. ↑fset-disjoint(NamesDeq;as;bs)
6. t : {I,irr_face(I;as;bs) ⊢ _:discr(T)}
7. {I,irr_face(I;as;bs) ⊢ _:discr(T)} ⊆r I,irr_face(I;as;bs) ij⟶ discrete-cube(T)
8. I,irr_face(I;as;bs) ij⟶ discrete-cube(T) ⊆r {I,irr_face(I;as;bs) ⊢ _:discr(T)}
9. irr-face-morph(I;as;bs) ∈ {f:I ⟶ I| (irr_face(I;as;bs) f) = 1} 
⊢ ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((irr_face(I;as;bs) g) = 1 ⇒ (g = irr-face-morph(I;as;bs) ⋅ g ∈ J ⟶ I))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[as,bs:fset(names(I))].
    \mforall{}[t:\{I,irr\_face(I;as;bs)  \mvdash{}  \_:discr(T)\}].  (t  =  discr(t(irr-face-morph(I;as;bs)))) 
    supposing  \muparrow{}fset-disjoint(NamesDeq;as;bs)


By

---

Latex:
(Auto
  THEN  (InstLemma  `discrete-cubical-term-is-map`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}I,irr\_face(I;as;bs)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  SubsumeC  \mkleeneopen{}I,irr\_face(I;as;bs)  ij{}\mrightarrow{}  discrete-cube(T)\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial)
  THEN  (Assert  irr-face-morph(I;as;bs)  \mmember{}  \{f:I  {}\mrightarrow{}  I|  (irr\_face(I;as;bs)  f)  =  1\}    BY
                          (MemTypeCD  THEN  EAuto  1))
  THEN  (Enough  to  prove  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].
                                                  ((irr\_face(I;as;bs)  g)  =  1  {}\mRightarrow{}  (g  =  irr-face-morph(I;as;bs)  \mcdot{}  g))
                Because  (InstLemma  `discrete-map-is-constant2`  [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}irr\_face(I;as;bs)\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};
                                  \mkleeneopen{}irr-face-morph(I;as;bs)\mkleeneclose{}]\mcdot{}
                                  THEN  Auto
                                  )))

---

Home Index