Theory pair

⊢ (∀a. ABS_prod (REP_prod a) = a) ∧
  ∀r. (λp. ∃x y. p = (λa b. a = x ∧ b = y)) r ⇔ REP_prod (ABS_prod r) = r

⊢ ∀x y. (x,y) = ABS_prod (λa b. a = x ∧ b = y)

⊢ ∀f x y. CURRY f x y = f (x,y)

⊢ ∀R1 R2. R1 LEX R2 = (λ(s,t) (u,v). R1 s u ∨ s = u ∧ R2 t v)

⊢ ∀x. (FST x,SND x) = x

⊢ ∀f g p. (f ## g) p = (f (FST p),g (SND p))

⊢ ∀P Q p. PROD_ALL P Q p ⇔ P (FST p) ∧ Q (SND p)

⊢ ∀R1 R2. R1 ### R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)

⊢ ∀a. SWAP a = (SND a,FST a)

⊢ ∀f v. UNCURRY f v = f (FST v) (SND v)

⊢ ∀p f. pair_CASE p f = f (FST p) (SND p)

⊢ ∃rep. TYPE_DEFINITION (λp. ∃x y. p = (λa b. a = x ∧ b = y)) rep

⊢ ∀p. setFST p = (λx. x = FST p)

⊢ ∀p. setSND p = (λx. x = SND p)

⊢ ∀x. ∃q r. x = (q,r)

⊢ ∀x y a b. (x,y) = (a,b) ⇔ x = a ∧ y = b

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

⊢ ∀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)

⊢ CURRY = (λf x y. f (x,y))

⊢ CURRY f = CURRY g ⇔ f = g

⊢ ∀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))

⊢ ∀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)

⊢ ∀f. CURRY (UNCURRY f) = f

⊢ flip (UNCURRY f) x = UNCURRY (flip (flip ∘ f) x)

⊢ (∃p. P (FST p) (SND p)) ⇔ ∃p1 p2. P p1 p2

⊢ $? (UNCURRY (λx. P x)) ⇔ ∃x. $? (P x)

⊢ (∀p. P (FST p) (SND p)) ⇔ ∀p1 p2. P p1 p2

⊢ $! (UNCURRY (λx. P x)) ⇔ ∀x. $! (P x)

⊢ ∀f. UNCURRY f = (λx. f (FST x) (SND x))

⊢ (∃p. P p) ⇔ ∃p_1 p_2. P (p_1,p_2)

⊢ (∀p. P p) ⇔ ∀p_1 p_2. P (p_1,p_2)

⊢ $! (UNCURRY f) ⇔ $! ($! ∘ f)

⊢ ∀x y. FST (x,y) = x

⊢ FST p = x ⇔ ∃y. p = (x,y)

⊢ ∀p f g. FST ((f ## g) p) = f (FST p)

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

⊢ ∀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)

⊢ ∀x. FST (SWAP x) = SND x

⊢ FST ∘ (g ## f) = g ∘ FST ∧ FST ∘ (g ## f) ∘ f' = g ∘ FST ∘ f'

⊢ FST ∘ SWAP = SND ∧ FST ∘ SWAP ∘ f = SND ∘ f

⊢ (x,y) ∈ UNCURRY R ⇔ R x y

⊢ ∀P. (λp. P p) = (λ(p1,p2). P (p1,p2))

⊢ ∀P M N. P (let (x,y) = M in N x y) = (let (x,y) = M in P (N x y))

⊢ ∀M N b. (let (x,y) = M in N x y) b = (let (x,y) = M in N x y b)

⊢ ∀R1 R2 v1 v2 R1' R2' v1' v2'.
    v1 = v1' ∧ v2 = v2' ∧
    (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ (R1 a c ⇔ R1' a c)) ∧
    (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ∧ a = c ⇒ (R2 b d ⇔ R2' b d)) ⇒
    ((R1 LEX R2) v1 v2 ⇔ (R1' LEX R2') v1' v2')

⊢ (R1 LEX R2) (a,b) (c,d) ⇔ R1 a c ∨ a = c ∧ R2 b d

⊢ (∀x y. R1 x y ⇒ R2 x y) ∧ (∀x y. R3 x y ⇒ R4 x y) ⇒
  (R1 LEX R3) x y ⇒
  (R2 LEX R4) x y

⊢ (x,y) = (a,b) ⇔ x = a ∧ y = b

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

⊢ ∀p q. p = q ⇔ FST p = FST q ∧ SND p = SND q

⊢ ∀P. (∃!f. P f) ⇔ ∃!p. P (λa. (FST p a,SND p a))

⊢ (∀a. a ∈ setFST ab ⇒ f1 a = f2 a) ∧ (∀b. b ∈ setSND ab ⇒ g1 b = g2 b) ⇒
  (f1 ## g1) ab = (f2 ## g2) ab

⊢ I ## I = I

⊢ ∀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)

⊢ ∀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)

⊢ setFST ((f ## g) ab) = (λc. ∃a. c = f a ∧ a ∈ setFST ab) ∧
  setSND ((f ## g) ab) = (λd. ∃b. d = g b ∧ b ∈ setSND ab)

⊢ ∀f g x y. (f ## g) (x,y) = (f x,g y)

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

⊢ ∀R1 R2. R1 ### R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)

⊢ $= ### $= = $=

⊢ (∀x. R1 x x) ∧ (∀y. R2 y y) ⇒ ∀xy. (R1 ### R2) xy xy

⊢ (∀x y. R1 x y ⇔ R1 y x) ∧ (∀a b. R2 a b ⇔ R2 b a) ⇒
  ∀xy ab. (R1 ### R2) xy ab ⇔ (R1 ### R2) ab xy

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

⊢ (∀x y z. R1 x y ∧ R1 y z ⇒ R1 x z) ∧ (∀a b c. R2 a b ∧ R2 b c ⇒ R2 a c) ⇒
  ∀xy ab uv. (R1 ### R2) xy ab ∧ (R1 ### R2) ab uv ⇒ (R1 ### R2) xy uv

⊢ ∀P. (∃x y. P x y) ⇔ ∃(x,y). P x y

⊢ ∀P. (∀x y. P x y) ⇔ ∀(x,y). P x y

⊢ ∀p p' P P' Q Q'.
    p = p' ∧ (∀x y. p' = (x,y) ⇒ (P x ⇔ P' x)) ∧
    (∀x y. p' = (x,y) ⇒ (Q y ⇔ Q' y)) ⇒
    (PROD_ALL P Q p ⇔ PROD_ALL P' Q' p')

⊢ (∀x. P x ⇒ P' x) ∧ (∀y. Q y ⇒ Q' y) ⇒ PROD_ALL P Q p ⇒ PROD_ALL P' Q' p

⊢ PROD_ALL P Q (x,y) ⇔ P x ∧ Q y

⊢ ∀x y. SND (x,y) = y

⊢ SND p = y ⇔ ∃x. p = (x,y)

⊢ ∀p f g. SND ((f ## g) p) = g (SND p)

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

⊢ ∀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)

⊢ ∀x. SND (SWAP x) = FST x

⊢ SND ∘ (g ## f) = f ∘ SND ∧ SND ∘ (g ## f) ∘ f' = f ∘ SND ∘ f'

⊢ SND ∘ SWAP = FST ∧ SND ∘ SWAP ∘ f = FST ∘ f

⊢ ∀x. SWAP (SWAP x) = x

⊢ SWAP = (λa. (SND a,FST a))

⊢ SWAP ∘ SWAP = I ∧ SWAP ∘ SWAP ∘ f = f

⊢ S f (UNCURRY g) = UNCURRY (S (S ∘ $o f ∘ $,) g)

⊢ ∀f' f M' M.
    M = M' ∧ (∀x y. M' = (x,y) ⇒ f x y = f' x y) ⇒
    UNCURRY f M = UNCURRY f' M'

⊢ (λ(x1,x2). y) x = y

⊢ ∀f. UNCURRY (CURRY f) = f

⊢ ∀f x y. UNCURRY f (x,y) = f x y

⊢ UNCURRY f x = y ⇔ ∃a b. x = (a,b) ∧ f a b = y

⊢ UNCURRY f = UNCURRY g ⇔ f = g

⊢ ∀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))

⊢ ∀f'. f' (UNCURRY f x) = UNCURRY ($o f' ∘ f) x

⊢ ∀M. UNCURRY M f0 x = UNCURRY (flip (flip ∘ M) x) f0

⊢ ∀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 f (SWAP x) = UNCURRY (flip f) x

⊢ ∀f v. UNCURRY f v = f (FST v) (SND v)

⊢ UNCURRY = flip pair_CASE

⊢ ∀R Q. WF R ∧ WF Q ⇒ WF (R LEX Q)

⊢ ∀R Q. WF R ∧ WF Q ⇒ WF (R ### Q)

⊢ DATATYPE (pair $,)

⊢ f ∘ UNCURRY g = UNCURRY ($o f ∘ g)

⊢ ∀f. ∃fn. ∀x y. fn (x,y) = f x y

⊢ ∀x. ∃q r. x = (q,r)

⊢ pair_CASE (SWAP v) f = pair_CASE v (flip f)

⊢ pair_CASE = flip UNCURRY

⊢ ∀M M' f.
    M = M' ∧ (∀x y. M' = (x,y) ⇒ f x y = f' x y) ⇒
    pair_CASE M f = pair_CASE M' f'

⊢ pair_CASE (x,y) f = f x y

⊢ pair_CASE p f = v ⇔ ∃x y. p = (x,y) ∧ f x y = v

⊢ ∀f'. f' (pair_CASE p f) ⇔ ∃x y. p = (x,y) ∧ f' (f x y)

⊢ pair_CASE (x,y) f = f x y

⊢ pair_CASE (x,y) = (λf. f x y)

⊢ ∀P. (∀p_1 p_2. P (p_1,p_2)) ⇒ ∀p. P p

⊢ (f ## g) p = (w,v) ⇔ ∃x y. p = (x,y) ∧ w = f x ∧ v = g y

⊢ reflexive (R1 LEX R2) ⇔ reflexive R1 ∨ reflexive R2

⊢ setFST (a,b) = (λx. x = a)

⊢ setSND (a,b) = (λx. x = b)

⊢ symmetric R1 ∧ symmetric R2 ⇒ symmetric (R1 LEX R2)

⊢ total R1 ∧ total R2 ⇒ total (R1 LEX R2)

⊢ transitive R1 ∧ transitive R2 ⇒ transitive (R1 LEX R2)