---

Step * 1 2 2 of Lemma ss-fun-fun


1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z)
5. λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
6. ∀x:Point(X ⟶ Y ⟶ Z). λG,x,y. (G <x, y>)(λF,p. (F (fst(p)) (snd(p)))(x)) ≡ x
7. y : Point(X × Y ⟶ Z)@i
⊢ λp.(y <fst(p), snd(p)>) ≡ y
BY
{ (Subst' (λp.(y <fst(p), snd(p)>)) = y ∈ Point(X × Y ⟶ Z) 0
   THEN Auto
   THEN Symmetry
   THEN (All (RWW "ss-fun-point prod-ss-point" ) THENA Auto)
   THEN D -1
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  Y  :  SeparationSpace
3.  Z  :  SeparationSpace
4.  \mlambda{}F,p.  (F  (fst(p))  (snd(p)))  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  \mtimes{}  Y  {}\mrightarrow{}  Z)
5.  \mlambda{}G,x,y.  (G  <x,  y>)  \mmember{}  Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z)
6.  \mforall{}x:Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z).  \mlambda{}G,x,y.  (G  <x,  y>)(\mlambda{}F,p.  (F  (fst(p))  (snd(p)))(x))  \mequiv{}  x
7.  y  :  Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z)@i
\mvdash{}  \mlambda{}p.(y  <fst(p),  snd(p)>)  \mequiv{}  y


By

---

Latex:
(Subst'  (\mlambda{}p.(y  <fst(p),  snd(p)>))  =  y  0
  THEN  Auto
  THEN  Symmetry
  THEN  (All  (RWW  "ss-fun-point  prod-ss-point"  )  THENA  Auto)
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index