Use functor arguments instead of subfunctor instances.

Make the normal functor arguments of type Set -> Set of
Distinct_Sub_Functor explicit and make the Sub_Functor
instance arguments implicit instead.

Arith.v

@@ -373,7 +373,7 @@ Section Arith.
 
   (* Add case. *)
 
-  Context {Dis_VI_Bot : Distinct_Sub_Functor _ Sub_NatValue_V Sub_BotValue_V}.
+  Context {Dis_VI_Bot : Distinct_Sub_Functor NatValue BotValue V}.
 
   (* Inversion principles for natural number SubValues. *)
   Definition SV_invertVI_P (i : SubValue_i V) :=
@@ -399,7 +399,7 @@ Section Arith.
     (WF_V' : WF_Functor V' V sub_V'_V),
     (forall (i : SubValue_i V) (H : SV' SV_invertVI_P i),
       exists v', proj1_sig (sv_a _ i) = inject v') ->
-    Distinct_Sub_Functor _ Sub_NatValue_V sub_V'_V ->
+    Distinct_Sub_Functor NatValue V' V ->
     iPAlgebra SV_invertVI_Name SV_invertVI_P SV'.
   Proof.
     econstructor; intros.

Arith_Lambda.v

@@ -66,13 +66,13 @@ Section Lambda_Arith.
   Variable WFV : (WFValue_i D V -> Prop) -> WFValue_i D V -> Prop.
   Context {funWFV : iFunctor WFV}.
 
-  Context {Dis_VI_Clos : Distinct_Sub_Functor Fun_V Sub_NatValue_V Sub_ClosValue_V}.
+  Context {Dis_VI_Clos : Distinct_Sub_Functor NatValue (ClosValue E) V}.
   Context {WF_Sub_ClosValue_V : WF_Functor (ClosValue E) V Sub_ClosValue_V}.
   Context {WF_Sub_NatValue_V : WF_Functor NatValue V Sub_NatValue_V}.
 
   Context {Sub_WFV_VI_WFV : Sub_iFunctor (WFValue_VI D V) WFV}.
   Context {Sub_WFV_Bot_WFV : Sub_iFunctor (WFValue_Bot D V) WFV}.
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_LType_D Sub_AType_D}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor LType AType D}.
 
   Context {Typeof_E : forall T, FAlgebra TypeofName T (typeofR D) (E (typeofR D))}.
   Context {WF_typeof_E : forall T, @WF_FAlgebra TypeofName T _ _ _

Bool.v

@@ -355,7 +355,7 @@ Section Bool.
   Context {SV : (SubValue_i V -> Prop) -> SubValue_i V -> Prop}.
   Context {Sub_SV_refl_SV : Sub_iFunctor (SubValue_refl V) SV}.
 
-  Context {Dis_VB_Bot : Distinct_Sub_Functor _ Sub_BoolValue_V Sub_BotValue_V}.
+  Context {Dis_VB_Bot : Distinct_Sub_Functor BoolValue BotValue V}.
 
   (* Inversion principles for natural number SubValues. *)
   Definition SV_invertVB_P (i : SubValue_i V) :=
@@ -381,7 +381,7 @@ Section Bool.
     (WF_V' : WF_Functor V' V sub_V'_V),
     (forall (i : SubValue_i V) (H : SV' SV_invertVB_P i),
       exists v', proj1_sig (sv_a _ i) = inject v') ->
-    Distinct_Sub_Functor _ Sub_BoolValue_V sub_V'_V ->
+    Distinct_Sub_Functor BoolValue V' V ->
     iPAlgebra SV_invertVB_Name SV_invertVB_P SV'.
   Proof.
     econstructor; intros.

Bool_Lambda.v

@@ -79,9 +79,9 @@ Section PLambda_Arith.
 
   Context {Sub_WFV_VB_WFV : Sub_iFunctor (WFValue_VB D V) WFV}.
   Context {Sub_WFV_Bot_WFV : Sub_iFunctor (WFValue_Bot D V) WFV}.
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_LType_D Sub_BType_D}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor LType BType D}.
 
-  Context {Dis_VB_Clos : Distinct_Sub_Functor Fun_V Sub_BoolValue_V Sub_ClosValue_V}.
+  Context {Dis_VB_Clos : Distinct_Sub_Functor BoolValue (ClosValue E) V}.
   Context {WF_Sub_ClosValue_V : WF_Functor (ClosValue E) V Sub_ClosValue_V}.
   Context {WF_Sub_BoolValue_V : WF_Functor BoolValue V Sub_BoolValue_V}.
 

Functors.v

@@ -494,10 +494,10 @@ Section Folds.
     reflexivity.
   Qed.
 
-  Class Distinct_Sub_Functor {F G H : Set -> Set}
-    (Fun_H : Functor H)
-    (sub_F_H : F :<: H)
-    (sub_G_H : G :<: H)
+  Class Distinct_Sub_Functor (F G H : Set -> Set)
+    {Fun_H : Functor H}
+    {sub_F_H : F :<: H}
+    {sub_G_H : G :<: H}
     : Set :=
     { inj_discriminate :
         forall A f g,
@@ -512,7 +512,7 @@ Section Folds.
     (sub_F_G : F :<: G)
     (sub_H_I : H :<: I)
     :
-    @Distinct_Sub_Functor F H (G :+: I) _ _ _.
+    Distinct_Sub_Functor F H (G :+: I).
   Proof.
     econstructor; intros.
     unfold not; simpl; unfold id; intros.
@@ -526,7 +526,7 @@ Section Folds.
     (sub_F_G : F :<: G)
     (sub_H_I : H :<: I)
     :
-    @Distinct_Sub_Functor F H (I :+: G) _ _ _.
+    Distinct_Sub_Functor F H (I :+: G).
   Proof.
     econstructor; intros.
     unfold not; simpl; unfold id; intros.
@@ -539,9 +539,9 @@ Section Folds.
     (Fun_I : Functor I)
     (sub_F_G : F :<: G)
     (sub_H_G : H :<: G)
-    (Dist_inl : @Distinct_Sub_Functor F H G Fun_G sub_F_G sub_H_G)
+    (Dist_inl : Distinct_Sub_Functor F H G)
     :
-    @Distinct_Sub_Functor F H (G :+: I) _ _ _.
+    Distinct_Sub_Functor F H (G :+: I).
   Proof.
     econstructor; intros.
     unfold not; intros.
@@ -555,9 +555,9 @@ Section Folds.
     (Fun_I : Functor I)
     (sub_F_G : F :<: G)
     (sub_H_G : H :<: G)
-    (Dist_inl : @Distinct_Sub_Functor F H G Fun_G sub_F_G sub_H_G)
+    (Dist_inl : Distinct_Sub_Functor F H G)
     :
-    @Distinct_Sub_Functor F H (I :+: G) _ _ _.
+    Distinct_Sub_Functor F H (I :+: G).
   Proof.
     econstructor; intros.
     unfold not; intros.
@@ -573,7 +573,7 @@ Section Folds.
     {sub_G_H : G :<: H}
     {WF_F : WF_Functor _ _ sub_F_H}
     {WF_G : WF_Functor _ _ sub_G_H},
-    Distinct_Sub_Functor Fun_H sub_F_H sub_G_H ->
+    Distinct_Sub_Functor F G H ->
     forall f g, inject (subGF := sub_F_H) f <> inject (subGF := sub_G_H) g.
   Proof.
     unfold inject; simpl; intros.

Lambda.v

@@ -545,7 +545,7 @@ Section Lambda.
 
   (* App case. *)
 
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_ClosValue_V Sub_BotValue_V}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor ClosValue BotValue V}.
   Context {iFun_SV : iFunctor SV}.
 
   Global Instance SV_proj1_b_Clos :

NatCase.v

@@ -186,7 +186,7 @@ Section NatCase.
     iPAlgebra SV_invertVI_Name (SV_invertVI_P V) SV}.
   Context {SV_invertVI'_SV :
     iPAlgebra SV_invertVI'_Name (SV_invertVI'_P V) SV}.
-  Context {Dis_VI_Bot : Distinct_Sub_Functor _ Sub_NatValue_V Sub_BotValue_V}.
+  Context {Dis_VI_Bot : Distinct_Sub_Functor NatValue BotValue V}.
   Context {SV_invertBot_SV :
     iPAlgebra SV_invertBot_Name (SV_invertBot_P V) SV}.