(** This file continues the development of algebra [Operation]. It
    gives a way to construct operations using (conventional) curried
    functions, and shows that such curried operations are equivalent
    to the uncurried operations [Operation]. *)

Require Export HoTT.Algebra.Universal.Algebra.

Require Import
  HoTT.Types
  HoTT.Spaces.Finite
  HoTT.Spaces.Nat.Core.

Local Open Scope Algebra_scope.
Local Open Scope nat_scope.

(** Functions [head_dom'] and [head_dom] are used to get the first
    element of a nonempty operation domain [a : forall i, A (ss i)]. *)

Monomorphic Definition head_dom' {σ} (A : Carriers σ) (n : nat)
  : forall (N : n > 0) (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)),
    A (fshead' n N ss)
  := match n with
     | 0 => fun N ss _ => Empty_rec (lt_irrefl _ N)
     | n'.+1 => fun N ss a => a fin_zero
     end.

Monomorphic Definition head_dom {σ} (A : Carriers σ) {n : nat}
  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
  : A (fshead ss)
  := head_dom' A n.+1 _ ss a.

(** Functions [tail_dom'] and [tail_dom] are used to obtain the tail
    of an operation domain [a : forall i, A (ss i)]. *)

Monomorphic Definition tail_dom' {σ} (A : Carriers σ) (n : nat)
  : forall (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)) (i : Fin (nat_pred n)),
    A (fstail' n ss i)
  := match n with
     | 0 => fun ss _ i => Empty_rec i
     | n'.+1 => fun ss a i => a (fsucc i)
     end.

Monomorphic Definition tail_dom {σ} (A : Carriers σ) {n : nat}
  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
  : forall i, A (fstail ss i)
  := tail_dom' A n.+1 ss a.

(** Functions [cons_dom'] and [cons_dom] to add an element to
    the front of a given domain [a : forall i, A (ss i)]. *)

Monomorphic Definition cons_dom' {σ} (A : Carriers σ) {n : nat}
  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0),
    A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i)
  := fin_ind
      (fun n i =>
        forall (ss : Fin n -> Sort σ) (N : n > 0),
        A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i))
      (fun n' _ z x _ => x)
      (fun n' i' _ => fun _ _ _ xs => xs i').

Definition cons_dom {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n.+1 (Sort σ))
  (x : A (fshead ss)) (xs : forall i, A (fstail ss i))
  : forall i : Fin n.+1, A (ss i)
  := fun i => cons_dom' A i ss _ x xs.

(** The empty domain: *)

Definition nil_dom {σ} (A : Carriers σ) (ss : FinSeq 0 (Sort σ))
  : forall i : Fin 0, A (ss i)
  := Empty_ind (A o ss).

(** A specialization of [Operation] to finite [Fin n] arity. *)

Definition FiniteOperation {σ : Signature} (A : Carriers σ)
  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : Type
  := Operation A {| Arity := Fin n; sorts_dom := ss; sort_cod := t |}.

(** A type of curried operations
<<
CurriedOperation A [s1, ..., sn] t := A s1 -> ... -> A sn -> A t.
>>
*)

Fixpoint CurriedOperation {σ} (A : Carriers σ) {n : nat}
  : (FinSeq n (Sort σ)) -> Sort σ -> Type
  := match n with
     | 0 => fun ss t => A t
     | n'.+1 =>
        fun ss t => A (fshead ss) -> CurriedOperation A (fstail ss) t
     end.

(** Function [operation_uncurry] is used to uncurry an operation
<<
operation_uncurry A [s1, ..., sn] t (op : CurriedOperation A [s1, ..., sn] t)
  : FiniteOperation A [s1, ..., sn] t
  := fun (x1 : A s1, ..., xn : A xn) => op x1 ... xn
>>
See [equiv_operation_curry] below. *)

Fixpoint operation_uncurry {σ} (A : Carriers σ) {n : nat}
  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
    CurriedOperation A ss t -> FiniteOperation A ss t
  := match n with
     | 0 => fun ss t op _ => op
     | n'.+1 =>
        fun ss t op a =>
          operation_uncurry A (fstail ss) t (op (a fin_zero)) (a o fsucc)
     end.

Local Example computation_example_operation_uncurry
  : forall
      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
      (ss := (fscons s1 (fscons s2 fsnil)))
      (op : CurriedOperation A ss t) (a : forall i, A (ss i)),
    operation_uncurry A ss t op
    = fun a => op (a fin_zero) (a (fsucc fin_zero)).
forall (σ : Signature) (A : Carriers σ),
nat ->
forall (s1 s2 t : Sort σ) (ss := fscons s1 (fscons s2 fsnil))
(op : CurriedOperation A ss t),
(forall i : Fin 2, A (ss i)) ->
operation_uncurry A ss t op =
(fun
   a : forall i : Arity {| Arity := Fin 2; sorts_dom := ss; sort_cod := t |},
       A (sorts_dom {| Arity := Fin 2; sorts_dom := ss; sort_cod := t |} i) =>
 op (a fin_zero) (a (fsucc fin_zero)))
Proof.
forall (σ : Signature) (A : Carriers σ),
nat ->
forall (s1 s2 t : Sort σ) (ss := fscons s1 (fscons s2 fsnil))
(op : CurriedOperation A ss t),
(forall i : Fin 2, A (ss i)) ->
operation_uncurry A ss t op =
(fun
   a : forall i : Arity {| Arity := Fin 2; sorts_dom := ss; sort_cod := t |},
       A (sorts_dom {| Arity := Fin 2; sorts_dom := ss; sort_cod := t |} i) =>
 op (a fin_zero) (a (fsucc fin_zero)))
  reflexivity.
Qed.

(** Function [operation_curry] is used to curry an operation
<<
operation_curry A [s1, ..., sn] t (op : FiniteOperation A [s1, ..., sn] t)
  : CurriedOperation A [s1, ..., sn] t
  := fun (x1 : A s1) ... (xn : A xn) => op (x1, ..., xn)
>>
See [equiv_operation_curry] below. *)

Fixpoint operation_curry {σ} (A : Carriers σ) {n : nat} 
  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
    FiniteOperation A ss t -> CurriedOperation A ss t
  := match n with
     | 0 => fun ss t op => op (Empty_ind _)
     | n'.+1 =>
        fun ss t op x =>
          operation_curry A (fstail ss) t (op o cons_dom A ss x)
     end.

Local Example computation_example_operation_curry
  : forall
      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
      (ss := (fscons s1 (fscons s2 fsnil)))
      (op : FiniteOperation A ss t)
      (x1 : A s1) (x2 : A s2),
    operation_curry A ss t op
    = fun x1 x2 => op (cons_dom A ss x1 (cons_dom A _ x2 (nil_dom A _))).
forall (σ : Signature) (A : Carriers σ),
nat ->
forall (s1 s2 t : Sort σ) (ss := fscons s1 (fscons s2 fsnil))
(op : FiniteOperation A ss t),
A s1 ->
A s2 ->
operation_curry A ss t op =
(fun (x1 : A (fshead ss)) (x2 : A (fshead (fstail ss))) =>
 op
   (cons_dom A ss x1
      (cons_dom A (fstail ss) x2 (nil_dom A (fstail (fstail ss))))))
Proof.
forall (σ : Signature) (A : Carriers σ),
nat ->
forall (s1 s2 t : Sort σ) (ss := fscons s1 (fscons s2 fsnil))
(op : FiniteOperation A ss t),
A s1 ->
A s2 ->
operation_curry A ss t op =
(fun (x1 : A (fshead ss)) (x2 : A (fshead (fstail ss))) =>
 op
   (cons_dom A ss x1
      (cons_dom A (fstail ss) x2 (nil_dom A (fstail (fstail ss))))))
  reflexivity.
Qed.

Lemma expand_cons_dom' {σ} (A : Carriers σ) (n : nat)
  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0)
           (a : forall i, A (ss i)),
    cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i.
σ: Signature
A: Carriers σ
n: nat
forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0)
(a : forall i0 : Fin n, A (ss i0)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
Proof.
σ: Signature
A: Carriers σ
n: nat
forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0)
(a : forall i0 : Fin n, A (ss i0)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
  intro i.
σ: Signature
A: Carriers σ
n: nat
i: Fin n
forall (ss : FinSeq n (Sort σ)) (N : n > 0)
(a : forall i0 : Fin n, A (ss i0)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
  induction i using fin_ind; intros ss N a.
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
cons_dom' A fin_zero ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a fin_zero
σ: Signature
A: Carriers σ
n: nat
i: Fin n
IHi: forall (ss0 : FinSeq n (Sort σ)) (N0 : n > 0)
(a0 : forall i0 : Fin n, A (ss0 i0)),
cons_dom' A i ss0 N0 (head_dom' A n N0 ss0 a0) (tail_dom' A n ss0 a0) = a0 i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i0 : Fin n.+1, A (ss i0)
cons_dom' A (fsucc i) ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a (fsucc i)
  -
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
cons_dom' A fin_zero ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a fin_zero unfold cons_dom'.
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall (ss0 : Fin n0 -> Sort σ) (N0 : n0 > 0),
   A (fshead' n0 N0 ss0) ->
   (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
  (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
     (x : A (fshead' n'.+1 z ss0))
     (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
   x)
  (fun (n' : nat) (i' : Fin n')
     (_ : forall (ss0 : Fin n' -> Sort σ) (N0 : n' > 0),
          A (fshead' n' N0 ss0) ->
          (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) -> A (ss0 i'))
     (ss0 : Fin n'.+1 -> Sort σ) (N0 : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N0 ss0))
     (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
   xs i')
  fin_zero ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a fin_zero
    rewrite fin_ind_beta_zero.
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
head_dom' A n.+1 N ss a = a fin_zero
    reflexivity.
  -
σ: Signature
A: Carriers σ
n: nat
i: Fin n
IHi: forall (ss0 : FinSeq n (Sort σ)) (N0 : n > 0)
(a0 : forall i0 : Fin n, A (ss0 i0)),
cons_dom' A i ss0 N0 (head_dom' A n N0 ss0 a0) (tail_dom' A n ss0 a0) = a0 i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i0 : Fin n.+1, A (ss i0)
cons_dom' A (fsucc i) ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a (fsucc i) unfold cons_dom'.
σ: Signature
A: Carriers σ
n: nat
i: Fin n
IHi: forall (ss0 : FinSeq n (Sort σ)) (N0 : n > 0)
(a0 : forall i0 : Fin n, A (ss0 i0)),
cons_dom' A i ss0 N0 (head_dom' A n N0 ss0 a0) (tail_dom' A n ss0 a0) = a0 i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i0 : Fin n.+1, A (ss i0)
fin_ind
  (fun (n0 : nat) (i0 : Fin n0) =>
   forall (ss0 : Fin n0 -> Sort σ) (N0 : n0 > 0),
   A (fshead' n0 N0 ss0) ->
   (forall i1 : Fin (nat_pred n0), A (fstail' n0 ss0 i1)) -> A (ss0 i0))
  (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
     (x : A (fshead' n'.+1 z ss0))
     (_ : forall i0 : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i0)) =>
   x)
  (fun (n' : nat) (i' : Fin n')
     (_ : forall (ss0 : Fin n' -> Sort σ) (N0 : n' > 0),
          A (fshead' n' N0 ss0) ->
          (forall i0 : Fin (nat_pred n'), A (fstail' n' ss0 i0)) ->
          A (ss0 i'))
     (ss0 : Fin n'.+1 -> Sort σ) (N0 : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N0 ss0))
     (xs : forall i0 : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i0)) =>
   xs i')
  (fsucc i) ss N (head_dom' A n.+1 N ss a) (tail_dom' A n.+1 ss a) =
a (fsucc i)
    by rewrite fin_ind_beta_fsucc.
Qed.

Lemma expand_cons_dom `{Funext} {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
  : cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
a: forall i : Fin n.+1, A (ss i)
cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a
Proof.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
a: forall i : Fin n.+1, A (ss i)
cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a
  funext i.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
a: forall i0 : Fin n.+1, A (ss i0)
i: Fin n.+1
cons_dom A ss (head_dom A ss a) (tail_dom A ss a) i = a i
  apply expand_cons_dom'.
Defined.

Lemma path_operation_curry_to_cunurry `{Funext} {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
  : operation_uncurry A ss t o operation_curry A ss t == idmap.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_uncurry A ss t o operation_curry A ss t == idmap
Proof.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_uncurry A ss t o operation_curry A ss t == idmap
  intro a.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
operation_uncurry A ss t (operation_curry A ss t a) = a
  induction n as [| n IHn].
H: Funext
σ: Signature
A: Carriers σ
ss: FinSeq 0 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
operation_uncurry A ss t (operation_curry A ss t a) = a
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : FiniteOperation A ss0 t),
operation_uncurry A ss0 t (operation_curry A ss0 t a0) = a0
operation_uncurry A ss t (operation_curry A ss t a) = a
  -
H: Funext
σ: Signature
A: Carriers σ
ss: FinSeq 0 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
operation_uncurry A ss t (operation_curry A ss t a) = a funext d.
H: Funext
σ: Signature
A: Carriers σ
ss: FinSeq 0 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
d: forall i : Arity {| Arity := Fin 0; sorts_dom := ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin 0; sorts_dom := ss; sort_cod := t |} i)
operation_uncurry A ss t (operation_curry A ss t a) d = a d refine (ap a _).
H: Funext
σ: Signature
A: Carriers σ
ss: FinSeq 0 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
d: forall i : Arity {| Arity := Fin 0; sorts_dom := ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin 0; sorts_dom := ss; sort_cod := t |} i)
Empty_ind
  (fun e : Empty =>
   A (sorts_dom {| Arity := Fin 0; sorts_dom := ss; sort_cod := t |} e)) =
d apply path_contr.
  -
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : FiniteOperation A ss0 t),
operation_uncurry A ss0 t (operation_curry A ss0 t a0) = a0
operation_uncurry A ss t (operation_curry A ss t a) = a funext a'.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : FiniteOperation A ss0 t),
operation_uncurry A ss0 t (operation_curry A ss0 t a0) = a0
a': forall i : Arity {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |} i)
operation_uncurry A ss t (operation_curry A ss t a) a' = a a'
    refine (ap (fun x => x _) (IHn _ _) @ _).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : FiniteOperation A ss0 t),
operation_uncurry A ss0 t (operation_curry A ss0 t a0) = a0
a': forall i : Arity {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |} i)
a (cons_dom A ss (a' fin_zero) (fun x : Fin n => a' (fsucc x))) = a a'
    refine (ap a _).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: FiniteOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : FiniteOperation A ss0 t),
operation_uncurry A ss0 t (operation_curry A ss0 t a0) = a0
a': forall i : Arity {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n.+1; sorts_dom := ss; sort_cod := t |} i)
cons_dom A ss (a' fin_zero) (fun x : Fin n => a' (fsucc x)) = a'
    apply expand_cons_dom.
Qed.

Lemma path_operation_uncurry_to_curry `{Funext} {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
  : operation_curry A ss t o operation_uncurry A ss t == idmap.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_curry A ss t o operation_uncurry A ss t == idmap
Proof.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_curry A ss t o operation_uncurry A ss t == idmap
  intro a.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
operation_curry A ss t (operation_uncurry A ss t a) = a
  induction n; [reflexivity|].
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
operation_curry A ss t (operation_uncurry A ss t a) = a
  funext x.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
operation_curry A ss t (operation_uncurry A ss t a) x = a x
  refine (_ @ IHn (fstail ss) (a x)).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
operation_curry A ss t (operation_uncurry A ss t a) x =
operation_curry A (fstail ss) t (operation_uncurry A (fstail ss) t (a x))
  refine (ap (operation_curry A (fstail ss) t) _).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
(fun x0 : forall i : Fin n, A (fstail ss i) =>
 operation_uncurry A ss t a (cons_dom A ss x x0)) =
operation_uncurry A (fstail ss) t (a x)
  funext a'.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
operation_uncurry A ss t a (cons_dom A ss x a') =
operation_uncurry A (fstail ss) t (a x) a'
  simpl.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
operation_uncurry A (fstail ss) t (a (cons_dom A ss x a' fin_zero))
  (fun x0 : Fin n => cons_dom A ss x a' (fsucc x0)) =
operation_uncurry A (fstail ss) t (a x) a'
  unfold cons_dom, cons_dom'.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
operation_uncurry A (fstail ss) t
  (a
     (fin_ind
        (fun (n0 : nat) (i : Fin n0) =>
         forall (ss0 : Fin n0 -> Sort σ) (N : n0 > 0),
         A (fshead' n0 N ss0) ->
         (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
        (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) 
           (z : n'.+1 > 0) (x0 : A (fshead' n'.+1 z ss0))
           (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
         x0)
        (fun (n' : nat) (i' : Fin n')
           (_ : forall (ss0 : Fin n' -> Sort σ) (N : n' > 0),
                A (fshead' n' N ss0) ->
                (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) ->
                A (ss0 i'))
           (ss0 : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
           (_ : A (fshead' n'.+1 N ss0))
           (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
         xs i')
        fin_zero ss (leq_add_r 1 n) x a'))
  (fun x0 : Fin n =>
   fin_ind
     (fun (n0 : nat) (i : Fin n0) =>
      forall (ss0 : Fin n0 -> Sort σ) (N : n0 > 0),
      A (fshead' n0 N ss0) ->
      (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
     (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
        (x1 : A (fshead' n'.+1 z ss0))
        (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
      x1)
     (fun (n' : nat) (i' : Fin n')
        (_ : forall (ss0 : Fin n' -> Sort σ) (N : n' > 0),
             A (fshead' n' N ss0) ->
             (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) ->
             A (ss0 i'))
        (ss0 : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
        (_ : A (fshead' n'.+1 N ss0))
        (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
      xs i')
     (fsucc x0) ss (leq_add_r 1 n) x a') =
operation_uncurry A (fstail ss) t (a x) a'
  rewrite fin_ind_beta_zero.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
operation_uncurry A (fstail ss) t (a x)
  (fun x0 : Fin n =>
   fin_ind
     (fun (n0 : nat) (i : Fin n0) =>
      forall (ss0 : Fin n0 -> Sort σ) (N : n0 > 0),
      A (fshead' n0 N ss0) ->
      (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
     (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
        (x1 : A (fshead' n'.+1 z ss0))
        (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
      x1)
     (fun (n' : nat) (i' : Fin n')
        (_ : forall (ss0 : Fin n' -> Sort σ) (N : n' > 0),
             A (fshead' n' N ss0) ->
             (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) ->
             A (ss0 i'))
        (ss0 : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
        (_ : A (fshead' n'.+1 N ss0))
        (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
      xs i')
     (fsucc x0) ss (leq_add_r 1 n) x a') =
operation_uncurry A (fstail ss) t (a x) a'
  refine (ap (operation_uncurry A (fstail ss) t (a x)) _).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
(fun x0 : Fin n =>
 fin_ind
   (fun (n0 : nat) (i : Fin n0) =>
    forall (ss0 : Fin n0 -> Sort σ) (N : n0 > 0),
    A (fshead' n0 N ss0) ->
    (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
   (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
      (x1 : A (fshead' n'.+1 z ss0))
      (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
    x1)
   (fun (n' : nat) (i' : Fin n')
      (_ : forall (ss0 : Fin n' -> Sort σ) (N : n' > 0),
           A (fshead' n' N ss0) ->
           (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) -> A (ss0 i'))
      (ss0 : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
      (_ : A (fshead' n'.+1 N ss0))
      (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
    xs i')
   (fsucc x0) ss (leq_add_r 1 n) x a') =
a'
  funext i'.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss0 : FinSeq n (Sort σ)) (a0 : CurriedOperation A ss0 t),
operation_curry A ss0 t (operation_uncurry A ss0 t a0) = a0
x: A (fshead ss)
a': forall i : Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |},
A (sorts_dom {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |} i)
i': Arity {| Arity := Fin n; sorts_dom := fstail ss; sort_cod := t |}
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall (ss0 : Fin n0 -> Sort σ) (N : n0 > 0),
   A (fshead' n0 N ss0) ->
   (forall i0 : Fin (nat_pred n0), A (fstail' n0 ss0 i0)) -> A (ss0 i))
  (fun (n' : nat) (ss0 : Fin n'.+1 -> Sort σ) (z : n'.+1 > 0)
     (x0 : A (fshead' n'.+1 z ss0))
     (_ : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
   x0)
  (fun (n' : nat) (i'0 : Fin n')
     (_ : forall (ss0 : Fin n' -> Sort σ) (N : n' > 0),
          A (fshead' n' N ss0) ->
          (forall i : Fin (nat_pred n'), A (fstail' n' ss0 i)) -> A (ss0 i'0))
     (ss0 : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N ss0))
     (xs : forall i : Fin (nat_pred n'.+1), A (fstail' n'.+1 ss0 i)) =>
   xs i'0)
  (fsucc i') ss (leq_add_r 1 n) x a' =
a' i'
  by rewrite fin_ind_beta_fsucc.
Qed.

Instance isequiv_operation_curry `{Funext} {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
  : IsEquiv (operation_curry A ss t).
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
IsEquiv (operation_curry A ss t)
Proof.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
IsEquiv (operation_curry A ss t)
  srapply isequiv_adjointify.
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
CurriedOperation A ss t -> FiniteOperation A ss t
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_curry A ss t o ?g == idmap
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
?g o operation_curry A ss t == idmap
  -
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
CurriedOperation A ss t -> FiniteOperation A ss t apply operation_uncurry.
  -
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_curry A ss t o operation_uncurry A ss t == idmap apply path_operation_uncurry_to_curry.
  -
H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n (Sort σ)
t: Sort σ
operation_uncurry A ss t o operation_curry A ss t == idmap apply path_operation_curry_to_cunurry.
Defined.

Definition equiv_operation_curry `{Funext} {σ} (A : Carriers σ)
  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
  : FiniteOperation A ss t <~> CurriedOperation A ss t
  := Build_Equiv _ _ (operation_curry A ss t) _.