Require Import Showable String List DepEquiv HoTT.

Axiom FunExt : Funext.

Definition lift {A} {B: A → Type} {C : A → Type} {B_ C_} `{(∀ a, B a ⇀ (C a)) ≃? (B_ ⇀ C_)} : (∀ a, B a → C a) → B_ ⇀ C_ := fun f ⇒ pe_fun (fun a b ⇒ creturn (f a b)).

Definition unlift {A} {B: A → Type} {C : A → Type} {B_ C_}
           {H :(∀ a, B a ⇀ (C a)) ≃? (B_ ⇀ C_)} :
  (B_ → C_) → ∀ a, B a ⇀ (C a) := fun ff ⇒ pe_inv (IsPartialEquiv := pe_isequiv (CanonicalPartialEquiv := H)) (clift ff).

Definition lift2 {A A'} {B: A → A' → Type} {C: A → A' → Type} {D : A → A' → Type} {B_ C_ D_}
           `{(∀ a a', B a a' → C a a' ⇀ D a a') ≃? (B_ → C_ ⇀ D_)} :
  (∀ a a', B a a' → C a a' → D a a') → B_ → C_ ⇀ D_ :=
  fun ff ⇒ pe_fun (fun a a' b c ⇒ creturn (ff a a' b c)).

Instance HODepEquiv_easy A (B: A → Type) C {HC : IsHSet C} C' {HC' : IsHSet C'}
           (H:B ≈ C)
   : (∀ a, B a ⇀ C') ≃? (C ⇀ C') | 0
  :=
    {| pe_fun := Build_Mon (to_simpl_dom : (∀ a : A, B a ⇀ C') → C ⇀ C') _ _;
       pe_isequiv := {| pe_inv := Build_Mon to_dep_dom _ _ |}|}.

Instance HODepEquiv {A} {B: A → Type} {C} {HC : IsHSet C}
           `{B ≈ C} {B': A → Type} {C'} {HC' : IsHSet C'}
           `{B' ≈ C'}
  : (∀ a, B a ⇀ (B' a)) ≃? (C ⇀ C'):=
  {| pe_fun := Build_Mon (fun f ⇒ to_simpl_dom (fun a b ⇒ x <- f a b; to_simpl x)) _ _ ;
     pe_isequiv := {| pe_inv := Build_Mon (fun f a b ⇒ x <- to_dep_dom f a b; to_dep _ x) _ _ |}|}.

Instance HODepEquiv2_sym A A' B_1 B_2 (B_3 : A → A' → Type) {C_1 C_2 C_3}
         {HC_1 : IsHSet C_1} {HC_2 : IsHSet C_2} {HC_3 : IsHSet C_3}
         (H: (∀ a a', B_2 a a' → B_1 a a' ⇀ B_3 a a') ≃? (C_2 → C_1 ⇀ C_3)) :
  (∀ a a', B_1 a a' → B_2 a a' ⇀ B_3 a a') ≃? (C_1 → C_2 ⇀ C_3) | 100
    :=
  {| pe_fun := Build_Mon (fun ff b_ c_ ⇒ pe_fun (fun a a' c b ⇒ ff a a' b c) c_ b_) _ _;
     pe_isequiv := {|pe_inv := Build_Mon (fun ff a a' b c ⇒ (pe_inv (IsPartialEquiv := pe_isequiv (CanonicalPartialEquiv := H))) (fun c b ⇒ ff b c) _ _ c b) _ _ |}|}.

Hint Extern 1 (IsPartialEquiv ?f) ⇒ apply (pe_isequiv (CanonicalPartialEquiv := _)) :
             typeclass_instances.

Definition to_simpl_dom2 {A A' B_1 B_2} {B_3 : A → A' → Type} {C_1 C_2 C_3}
           {HC_1 : IsHSet C_1} {HC_2 : IsHSet C_2} {HC_3 : IsHSet C_3}
           `{∀ a, ((∀ a':A', B_2 a a' ⇀ B_3 a a') ≃? (C_2 ⇀ C_3))}
           `{DepEquiv A B_1 C_1}:
         (∀ a a', B_1 a → B_2 a a' ⇀ B_3 a a') → C_1 → C_2 ⇀ C_3 :=
  fun f ⇒ let f' := fun a b ⇒ pe_fun (fun a' ⇒ f a a' b) in
        fun b_ c ⇒ to_simpl_dom (fun a b ⇒ f' a b c) b_.

Definition to_dep_dom2 {A A' B_1 B_2} {B_3 : A → A' → Type} {C_1 C_2 C_3 }
           {HC_1 : IsHSet C_1} {HC_2 : IsHSet C_2} {HC_3 : IsHSet C_3}
           `{∀ a, ((∀ a':A', B_2 a a' ⇀ B_3 a a') ≃? (C_2 ⇀ C_3))} `{DepEquiv A B_1 C_1}:
         (C_1 → C_2 ⇀ C_3) → ∀ a a', B_1 a → B_2 a a' ⇀ B_3 a a' :=
  fun f a a' b c ⇒
    pe_inv (IsPartialEquiv := pe_isequiv (CanonicalPartialEquiv := H a))
           (fun x ⇒ c <- to_simpl b; f c x) a' c.

Instance HODepEquiv2
         A A' (B_1: A → Type) (B_2: A → A' → Type) (B_3 : A → A' → Type)
         C_1 C_2 C_3
         {HC_1 : IsHSet C_1} {HC_2 : IsHSet C_2} {HC_3 : IsHSet C_3}
         (H:∀ a, ((∀ a':A', B_2 a a' ⇀ B_3 a a') ≃? (C_2 ⇀ C_3))) `{DepEquiv A B_1 C_1} :
  (∀ a a', B_1 a → B_2 a a' ⇀ B_3 a a') ≃? (C_1 → C_2 ⇀ C_3)
  :=
  {| pe_fun := Build_Mon to_simpl_dom2 _ _ ;
     pe_isequiv := {| pe_inv := Build_Mon to_dep_dom2 _ _ |}|}.



Instance DepEquiv_with_pe A A' B C (f : A' → A) {HC : IsHSet C} {Hf: IsInjective f}
         {HP : B ≈ C} : (fun a ⇒ B (f a)) ≈ C :=
  Build_DepEquiv A' (fun a ⇒ B (f a)) C HC (fun a c ⇒ P (f a) c)
                (fun a' ⇒ total_equiv (f a'))
                (λ a : A', partial_equiv (f a))
                (fun c ⇒ a <- c_to_a c; f^?-1 a) _ showC.