Operation.v

(** 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.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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 (not_lt_n_n _ 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 (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 i : Fin n, A (ss i)),
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 (ss : FinSeq n (Sort σ)) (N : n > 0) (a : forall i : Fin n, A (ss i)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
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 (n : nat) (i : Fin n) =>
   forall (ss : Fin n -> Sort σ) (N : n > 0),
   A (fshead' n N ss) ->
   (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
   A (ss i))
  (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
     (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
     (_ : forall i : Fin (pred n'.+1),
          A (fstail' n'.+1 ss i)) => x)
  (fun (n' : nat) (i' : Fin n')
     (_ : forall (ss : Fin n' -> Sort σ) (N : n' > 0),
          A (fshead' n' N ss) ->
          (forall i : Fin (pred n'),
           A (fstail' n' ss i)) -> A (ss i'))
     (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N ss))
     (xs : forall i : Fin (pred n'.+1),
           A (fstail' n'.+1 ss 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 compute_fin_ind_fin_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 (ss : FinSeq n (Sort σ)) (N : n > 0) (a : forall i : Fin n, A (ss i)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
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 (ss : FinSeq n (Sort σ)) (N : n > 0) (a : forall i : Fin n, A (ss i)),
cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i
ss: FinSeq n.+1 (Sort σ)
N: n.+1 > 0
a: forall i : Fin n.+1, A (ss i)
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall (ss : Fin n -> Sort σ) (N : n > 0),
   A (fshead' n N ss) ->
   (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
   A (ss i))
  (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
     (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
     (_ : forall i : Fin (pred n'.+1),
          A (fstail' n'.+1 ss i)) => x)
  (fun (n' : nat) (i' : Fin n')
     (_ : forall (ss : Fin n' -> Sort σ) (N : n' > 0),
          A (fshead' n' N ss) ->
          (forall i : Fin (pred n'),
           A (fstail' n' ss i)) -> A (ss i'))
     (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N ss))
     (xs : forall i : Fin (pred n'.+1),
           A (fstail' n'.+1 ss i)) => 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 compute_fin_ind_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 i : Fin n.+1, A (ss i)
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 (ss : FinSeq n (Sort σ)) (a : FiniteOperation A ss t),
operation_uncurry A ss t (operation_curry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : FiniteOperation A ss t),
operation_uncurry A ss t (operation_curry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : FiniteOperation A ss t),
operation_uncurry A ss t (operation_curry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : FiniteOperation A ss t),
operation_uncurry A ss t (operation_curry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : FiniteOperation A ss t),
operation_uncurry A ss t (operation_curry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (n : nat) (i : Fin n) =>
         forall (ss : Fin n -> Sort σ) (N : n > 0),
         A (fshead' n N ss) ->
         (forall i0 : Fin (pred n),
          A (fstail' n ss i0)) -> A (ss i))
        (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
           (z : n'.+1 > 0)
           (x : A (fshead' n'.+1 z ss))
           (_ : forall i : Fin (pred n'.+1),
                A (fstail' n'.+1 ss i)) => x)
        (fun (n' : nat) (i' : Fin n')
           (_ : forall (ss : Fin n' -> Sort σ)
                (N : n' > 0),
                A (fshead' n' N ss) ->
                (forall i : Fin (pred n'),
                 A (fstail' n' ss i)) -> A (ss i'))
           (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
           (_ : A (fshead' n'.+1 N ss))
           (xs : forall i : Fin (pred n'.+1),
                 A (fstail' n'.+1 ss i)) => xs i')
        fin_zero ss (leq_S_n' 0 n (leq_0_n n)) x a'))
  (fun x0 : Fin n =>
   fin_ind
     (fun (n : nat) (i : Fin n) =>
      forall (ss : Fin n -> Sort σ) (N : n > 0),
      A (fshead' n N ss) ->
      (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
      A (ss i))
     (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
        (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
        (_ : forall i : Fin (pred n'.+1),
             A (fstail' n'.+1 ss i)) => x)
     (fun (n' : nat) (i' : Fin n')
        (_ : forall (ss : Fin n' -> Sort σ)
             (N : n' > 0),
             A (fshead' n' N ss) ->
             (forall i : Fin (pred n'),
              A (fstail' n' ss i)) -> A (ss i'))
        (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
        (_ : A (fshead' n'.+1 N ss))
        (xs : forall i : Fin (pred n'.+1),
              A (fstail' n'.+1 ss i)) => xs i')
     (fsucc x0) ss (leq_S_n' 0 n (leq_0_n n)) x a') =
operation_uncurry A (fstail ss) t (a x) a'
  rewrite compute_fin_ind_fin_zero.H: Funext
σ: Signature
A: Carriers σ
n: nat
ss: FinSeq n.+1 (Sort σ)
t: Sort σ
a: CurriedOperation A ss t
IHn: forall (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (n : nat) (i : Fin n) =>
      forall (ss : Fin n -> Sort σ) (N : n > 0),
      A (fshead' n N ss) ->
      (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
      A (ss i))
     (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
        (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
        (_ : forall i : Fin (pred n'.+1),
             A (fstail' n'.+1 ss i)) => x)
     (fun (n' : nat) (i' : Fin n')
        (_ : forall (ss : Fin n' -> Sort σ)
             (N : n' > 0),
             A (fshead' n' N ss) ->
             (forall i : Fin (pred n'),
              A (fstail' n' ss i)) -> A (ss i'))
        (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
        (_ : A (fshead' n'.+1 N ss))
        (xs : forall i : Fin (pred n'.+1),
              A (fstail' n'.+1 ss i)) => xs i')
     (fsucc x0) ss (leq_S_n' 0 n (leq_0_n 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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (n : nat) (i : Fin n) =>
    forall (ss : Fin n -> Sort σ) (N : n > 0),
    A (fshead' n N ss) ->
    (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
    A (ss i))
   (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
      (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
      (_ : forall i : Fin (pred n'.+1),
           A (fstail' n'.+1 ss i)) => x)
   (fun (n' : nat) (i' : Fin n')
      (_ : forall (ss : Fin n' -> Sort σ)
           (N : n' > 0),
           A (fshead' n' N ss) ->
           (forall i : Fin (pred n'),
            A (fstail' n' ss i)) -> A (ss i'))
      (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
      (_ : A (fshead' n'.+1 N ss))
      (xs : forall i : Fin (pred n'.+1),
            A (fstail' n'.+1 ss i)) => xs i')
   (fsucc x0) ss (leq_S_n' 0 n (leq_0_n 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 (ss : FinSeq n (Sort σ)) (a : CurriedOperation A ss t),
operation_curry A ss t (operation_uncurry A ss t a) = a
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 (n : nat) (i : Fin n) =>
   forall (ss : Fin n -> Sort σ) (N : n > 0),
   A (fshead' n N ss) ->
   (forall i0 : Fin (pred n), A (fstail' n ss i0)) ->
   A (ss i))
  (fun (n' : nat) (ss : Fin n'.+1 -> Sort σ)
     (z : n'.+1 > 0) (x : A (fshead' n'.+1 z ss))
     (_ : forall i : Fin (pred n'.+1),
          A (fstail' n'.+1 ss i)) => x)
  (fun (n' : nat) (i' : Fin n')
     (_ : forall (ss : Fin n' -> Sort σ) (N : n' > 0),
          A (fshead' n' N ss) ->
          (forall i : Fin (pred n'),
           A (fstail' n' ss i)) -> A (ss i'))
     (ss : Fin n'.+1 -> Sort σ) (N : n'.+1 > 0)
     (_ : A (fshead' n'.+1 N ss))
     (xs : forall i : Fin (pred n'.+1),
           A (fstail' n'.+1 ss i)) => xs i')
  (fsucc i') ss (leq_S_n' 0 n (leq_0_n n)) x a' =
a' i'
  now rewrite compute_fin_ind_fsucc.
Qed.

Global 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) _.