Remove redundant structures for finite powers

1 files changed, 5 insertions, 8 deletions

diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index ca148e2..09f94f0 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -10,7 +10,7 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
 (* Any eqType, choiceType, countType and finType structures on rT extend to   *)
 (* {ffun aT -> rT} as Leibnitz equality and extensional equalities coincide.  *)
 (*     (T ^ n)%type is notation for {ffun 'I_n -> T}, which is isomorphic     *)
-(*                     ot n.-tuple T.                                         *)
+(*                     to n.-tuple T.                                         *)
 (*  For f : {ffun aT -> rT}, we define                                        *)
 (*              f x == the image of x under f (f coerces to a CiC function)   *)
 (*         fgraph f == the graph of f, i.e., the #|aT|.-tuple rT of the       *)
@@ -52,13 +52,13 @@ End Def.
 
 Notation "{ 'ffun' fT }" := (finfun_of (Phant fT))
   (at level 0, format "{ 'ffun'  '[hv' fT ']' }") : type_scope.
-Definition finexp_domFinType n := ordinal_finType n.
-Notation "T ^ n" := (@finfun_of (finexp_domFinType n) T (Phant _)) : type_scope.
+Definition exp_finIndexType n := ordinal_finType n.
+Notation "T ^ n" := (@finfun_of (exp_finIndexType n) T (Phant _)) : type_scope.
 
-Notation Local fun_of_fin_def :=
+Local Notation fun_of_fin_def :=
   (fun aT rT f x => tnth (@fgraph aT rT f) (enum_rank x)).
 
-Notation Local finfun_def := (fun aT rT f => @Finfun aT rT (codom_tuple f)).
+Local Notation finfun_def := (fun aT rT f => @Finfun aT rT (codom_tuple f)).
 
 Module Type FunFinfunSig.
 Parameter fun_of_fin : forall aT rT, finfun_type aT rT -> aT -> rT.
@@ -212,7 +212,6 @@ by move=> x Ax; apply: f_fam; apply/imageP; exists x.
 Qed.
 
 End EqTheory.
-Canonical exp_eqType (T : eqType) n := [eqType of T ^ n].
 
 Implicit Arguments supportP [aT rT y D g].
 Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))).
@@ -224,7 +223,6 @@ Canonical finfun_choiceType aT rT :=
   Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
 Canonical finfun_of_choiceType (aT : finType) (rT : choiceType) :=
   Eval hnf in [choiceType of {ffun aT -> rT}].
-Canonical exp_choiceType (T : choiceType) n := [choiceType of T ^ n].
 
 Definition finfun_countMixin aT (rT : countType) :=
   [countMixin of finfun_type aT rT by <:].
@@ -301,5 +299,4 @@ Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.
 Proof. by rewrite -card_ffun_on; apply/esym/eq_card=> f; apply/forallP. Qed.
 
 End FinTheory.
-Canonical exp_finType (T : finType) n := [finType of T ^ n].