Theory lifting

⊢ ∀R Abs Rep Tf.
    Qt R Abs Rep Tf ⇔
    R = Tfᵀ ∘ᵣ Tf ∧ (∀a b. Tf a b ⇒ Abs a = b) ∧ ∀a. Tf (Rep a) a

⊢ ∀f g h. (f ---> g) h = g ∘ h ∘ f

⊢ Qt R Abs Rep Tf ∧ f = Abs t ∧ R t t ⇒ Tf t f

⊢ Qt R Abs Rep Tf ⇒ (Tf |==> Tf |==> $<=>) R $=

⊢ Qt R Abs Rep Tf ⇔
  (∀a. Abs (Rep a) = a) ∧ (∀a. R (Rep a) (Rep a)) ∧
  (∀c1 c2. R c1 c2 ⇔ R c1 c1 ∧ R c2 c2 ∧ Abs c1 = Abs c2) ∧
  Tf = (λc a. R c c ∧ Abs c = a)

⊢ Qt R Abs Rep Tf ⇔
  (∀c a. Tf c a ⇒ Abs c = a) ∧ (∀a. Tf (Rep a) a) ∧
  ∀c1 c2. R c1 c2 ⇔ Tf c1 (Abs c2) ∧ Tf c2 (Abs c1)

⊢ Qt R Abs Rep Tf ⇒ right_unique Tf

⊢ Qt R Abs Rep Tf ⇒ surj Tf

⊢ Qt R Abs Rep Tf ⇒ ∀x. R x x ⇒ R (Rep (Abs x)) x

⊢ Qt D AbsD RepD TfD ∧ Qt R AbsR RepR TfR ⇒
  Qt (D |==> R) (RepD ---> AbsR) (AbsD ---> RepR) (TfD |==> TfR)

⊢ Qt $= I I $=

⊢ Qt R Abs Rep Tf ⇒ Qt (LIST_REL R) (MAP Abs) (MAP Rep) (LIST_REL Tf)

⊢ f ---> I = flip $o f ∧ I ---> g = $o g

⊢ I ---> I = I

⊢ f1 ∘ f2 ---> g1 ∘ g2 = (f2 ---> g1) ∘ (f1 ---> g2)

⊢ (f ---> g) h x = g (h (f x))

⊢ Qt R1 Abs1 Rep1 Tf1 ∧ Qt R2 Abs2 Rep2 Tf2 ⇒
  Qt (R1 ### R2) (Abs1 ## Abs2) (Rep1 ## Rep2) (Tf1 ### Tf2)

⊢ Qt R Abs Rep Tf ⇒
  Qt (R |==> $<=>) (PREIMAGE Rep) (PREIMAGE Abs) (Tf |==> $<=>)