Theory "quotient_pair"

Signature

Definitions

PAIR_REL

⊢ ∀R1 R2. $### R1 R2 = (λ(a,b) (c,d). R1 a c ∧ R2 b d)

Theorems

UNCURRY_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f1 f2.
                  $===> R1 ($===> R2 R3) f1 f2 ⇒
                  $===> ($### R1 R2) R3 (UNCURRY f1) (UNCURRY f2)

UNCURRY_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f p.
                  UNCURRY f p =
                  abs3
                    (UNCURRY ((abs1 --> abs2 --> rep3) f) ((rep1 ## rep2) p))

SND_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀p1 p2. $### R1 R2 p1 p2 ⇒ R2 (SND p1) (SND p2)

SND_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀p. SND p = abs2 (SND ((rep1 ## rep2) p))

PAIR_REL_THM

⊢ ∀R1 R2 a b c d. $### R1 R2 (a,b) (c,d) ⇔ R1 a c ∧ R2 b d

PAIR_REL_REFL

⊢ ∀R1 R2.
      (∀x y. R1 x y ⇔ (R1 x = R1 y)) ∧ (∀x y. R2 x y ⇔ (R2 x = R2 y)) ⇒
      ∀x. $### R1 R2 x x

PAIR_REL_EQ

⊢ $### $= $= = $=

PAIR_QUOTIENT

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          QUOTIENT ($### R1 R2) (abs1 ## abs2) (rep1 ## rep2)

PAIR_MAP_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀R4 abs4 rep4.
                  QUOTIENT R4 abs4 rep4 ⇒
                  ∀f1 f2 g1 g2.
                      $===> R1 R2 f1 f2 ∧ $===> R3 R4 g1 g2 ⇒
                      $===> ($### R1 R3) ($### R2 R4) (f1 ## g1) (f2 ## g2)

PAIR_MAP_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀R4 abs4 rep4.
                  QUOTIENT R4 abs4 rep4 ⇒
                  ∀f g.
                      f ## g =
                      ((rep1 ## rep3) --> (abs2 ## abs4))
                        ((abs1 --> rep2) f ## (abs3 --> rep4) g)

PAIR_MAP_I

⊢ I ## I = I

PAIR_EQUIV

⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV ($### R1 R2)

FST_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀p1 p2. $### R1 R2 p1 p2 ⇒ R1 (FST p1) (FST p2)

FST_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀p. FST p = abs1 (FST ((rep1 ## rep2) p))

CURRY_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f1 f2.
                  $===> ($### R1 R2) R3 f1 f2 ⇒
                  $===> R1 ($===> R2 R3) (CURRY f1) (CURRY f2)

CURRY_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f a b.
                  CURRY f a b =
                  abs3 (CURRY (((abs1 ## abs2) --> rep3) f) (rep1 a) (rep2 b))

COMMA_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀a1 a2 b1 b2. R1 a1 b1 ∧ R2 a2 b2 ⇒ $### R1 R2 (a1,a2) (b1,b2)

COMMA_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀a b. (a,b) = (abs1 ## abs2) (rep1 a,rep2 b)