代码拉取完成，页面将自动刷新
(**#+TITLE: cartierSolution3.v
Proph
https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution3.v
solves half of some question of Cartier which is how to program grammatical polymorph metafunctors-full-subcategory containing-equalizers generated by some views ( "complete" ) ...
The ends is to start from some generating/views data and then to add equalizers of morphisms ; but where are those equalizers ? Oneself could get them as metafunctors on this generating data, as long as oneself grammatically distinguishes whatever-is-interesting .
In contrast from the earlier grammatical presentation of pairing-projections (product), now the equalizer-objects do depend on the morphisms . BUT THIS DEPENDENCE NEED-NOT BE GRAMMATICAL ! This dependence could be expressed via the sense-decoding ( "Yoneda" ) of the grammatical morphisms .
The grammatical objects/morphisms are simultaneously-mutually presented with their sense-decoding ; this could be done via some common inductive-recursive presentation or alternatively by inferring the sense-decoding computation into extra indexes of the type-family of the object/morphisms .
The conversion-relation shall convert across two morphisms whose sense-decoding indexes are not syntactically/grammatically-the-same. But oneself does show that, by logical-deduction, these two sense-decoding are indeed propositionally equal ( "soundness lemma" ) .
Finally, some linear total/asymptotic grade is defined on the morphisms and the tactics-automated degradation lemma shows that each of the conversion indeed degrades the redex morphism .
For instant first impression , the conversion-relation constructor which says that the inclusion/restriction (projection) morphisms cancels the corestriction (pairing) morphism , is written as :
#+BEGIN_EXAMPLE
| Pairing_Project1 :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
forall Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0),
forall (Yoneda10_ff_eq :
forall A : obIndexer, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
forall ( _transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 )
( _transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 )
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0),
( ( ff o>CoMod zz )
: 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod Yoneda10_ff Yoneda10_zz )0 )
<~~ ( ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
o>CoMod ( ~_1 @ _transfL , _transfR o>CoMod zz ) )
: 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod (Yoneda10_Pairing Yoneda10_ff_eq)
(Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz) )0 )
#+END_EXAMPLE
KEYWORDS : 1337777.OOO ; COQ ; cut-elimination ; equalizers ; polymorph metafunctors-grammar ; modos
OUTLINE :
* Generating-views data
* Grammatical presentation of objects and morphisms , with sense-decoding as metafunctors and metatransformations
** Grammatical presentation of objects
** Grammatical presentation of morphisms
* Grammatical conversions of morphisms , which infer the same sense-decoding
** Grammatical conversions of morphisms
** Same sense-decoding for convertible morphisms
** Linear total/asymptotic grade and the degradation lemma
* Solution
** Solution morphisms without polymorphism
** Destruction of morphisms with inner-instantiation of object-indexes
* Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution
-----
EPILOGUE : Now there is enough data (for multiple masters-engineering) to confirm the presence of some MODOS grammar, which is some style of "substructural topos" ... where oneself could present grammatical polymorph views-data ( "sheaves" ) , grammatical polymorph generating-views ( "presentable category" ) , grammatical polymorph internal functors ( "internal category" ) , grammatical polymorph images ( "regular category" ) , grammatical polymorph unions ( "coherent category" ) ...
-----
BUY RECURSIVE T-SQUARE paypal.me/1337777 ; 微信支付 2796386464@qq.com ; eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777
**)
(**
* Generating-views data
The ends is to start from some generating data and then to add equalizers of morphisms ; but where are those equalizers ? Oneself could get them as metafunctors on this generating data, as long as oneself grammatically distinguishes whatever-is-interesting .
Here for simplicity, the generating/views data is some identity-functor (category) but could be as basic as only some graph .
#+BEGIN_SRC coq :exports both :results silent **)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
Require Omega.
Module EQUALIZERS.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Parameter obIndexer : Type.
Parameter morIndexer : obIndexer -> obIndexer -> Type.
Parameter polyIndexer : forall A A', morIndexer A' A -> forall A'', morIndexer A'' A' -> morIndexer A'' A .
Parameter unitIndexer : forall {A : obIndexer}, morIndexer A A.
Delimit Scope poly_scope with poly.
Open Scope poly.
Notation "''Indexer' (0 A' ~> A )0" :=
(@morIndexer A' A) (at level 0, format "''Indexer' (0 A' ~> A )0") : poly_scope.
Notation "a_ o>Indexer a'" :=
(@polyIndexer _ _ a' _ a_) (at level 40, a' at next level, left associativity) : poly_scope.
Axiom polyIndexer_morphism :
forall (A A' : obIndexer) (a' : 'Indexer(0 A' ~> A )0)
(A'' : obIndexer) (a_ : 'Indexer(0 A'' ~> A' )0),
forall B (b : 'Indexer(0 B ~> A'' )0),
b o>Indexer ( a_ o>Indexer a' ) = ( b o>Indexer a_ ) o>Indexer a' .
Axiom polyIndexer_unitIndexer :
forall (A A' : obIndexer) (a' : 'Indexer(0 A' ~> A )0),
a' = ( (@unitIndexer A') o>Indexer a' ) .
Axiom unitIndexer_polyIndexer :
forall (A : obIndexer), forall (A'' : obIndexer) (a_ : 'Indexer(0 A'' ~> A )0),
a_ = ( a_ o>Indexer (@unitIndexer A) ) .
(**#+END_SRC
* Grammatical presentation of objects and morphisms , with sense-decoding as metafunctors and metatransformations
In contrast from the earlier grammatical presentation of pairing-projections (product), now the equalizer-objects do depend on the morphisms . BUT THIS DEPENDENCE NEED-NOT BE GRAMMATICAL ! This dependence could be expressed via the sense-decoding ( "Yoneda" ) of the grammatical morphisms .
The sense-decoding of any object is some metafunctor . The sense-decoding of any morphism is some metatransformation . The grammatical objects are simultaneously-mutually presented with their sense-decoding ; this could be done via some common inductive-recursive presentation or alternatively by inferring the sense-decoding computation into extra indexes of the type-family of the objects . This same comment holds for the presentation of grammatical morphisms .
While the common choice would be to use the inductive-recursive presentation, it is true that the extra-indexes presentation enable the easy sharing of indexes among grammatical objects and grammatical morphisms ; therefore this extra-indexes presentation avoids the need for manipulating extra propositional-equalities which express these sharings .
** Grammatical presentation of objects
The elements of the metafunctor which is the sense-decoding of the equalizer-object is the well-known equalized-subcollection of the elements of the metafunctor which is the sense-decoding of the domain-object . The common definition in polymorph mathematics says that the particular-deduction of this second-component equalizing-property does not matter ( is unique ) ; therefore the COQ logic shall express this property and other common functional-extensionality properties, via some very-particular axioms for example .
#+BEGIN_SRC coq :exports both :results silent **)
Definition Yoneda01_functor (Yoneda00 : obIndexer -> Type)
(Yoneda01 : (forall A A' : obIndexer, 'Indexer(0 A' ~> A )0 -> Yoneda00 A -> Yoneda00 A')) : Prop :=
( (* binary/composing functoriality *)
( forall A A' (a : 'Indexer(0 A' ~> A)0) A'' (a' : 'Indexer(0 A'' ~> A')0) x,
Yoneda01 _ _ a' (Yoneda01 _ _ a x) = Yoneda01 _ _ (a' o>Indexer a) x ) /\
( (* empty/unit functoriality is held only in PolyYoneda00_Pairing *)
forall A x, x = Yoneda01 _ _ (@unitIndexer A) x ) ) .
Definition Yoneda10_natural
Yoneda00_F (Yoneda01_F : { Yoneda01 : _ | Yoneda01_functor Yoneda01 })
Yoneda00_G (Yoneda01_G : { Yoneda01 : _ | Yoneda01_functor Yoneda01 })
(Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A) : Prop :=
forall A A' (a : 'Indexer(0 A' ~> A )0) (f : Yoneda00_F A),
(proj1_sig Yoneda01_G) _ _ a (Yoneda10 A f) = Yoneda10 A' ((proj1_sig Yoneda01_F) _ _ a f) .
Axiom ax1_Yoneda10_natural
: forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G,
forall (Yoneda10_gg : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10}),
forall (Yoneda10_gg0 : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10}),
( forall A0, (proj1_sig Yoneda10_gg0 A0) =1 (proj1_sig Yoneda10_gg A0) ) ->
Yoneda10_gg0 = Yoneda10_gg .
Axiom ax2_Yoneda00_EqFunctor :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(transfL transfR : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf})
A (Pr := (fun f : Yoneda00_F A => proj1_sig transfL A f = proj1_sig transfR A f))
(f : Yoneda00_F A) (fP : Pr f) (g : Yoneda00_F A) (gP : Pr g),
f = g -> exist Pr f fP = exist Pr g gP .
Section Senses_obCoMod.
Lemma Yoneda00_View : forall (B : obIndexer), (obIndexer -> Type).
Proof. intros B. refine (fun A => 'Indexer(0 A ~> B )0 ). Defined.
Lemma Yoneda01_View : forall (B : obIndexer),
{Yoneda01 : ( forall A A' : obIndexer, 'Indexer(0 A' ~> A )0 -> (Yoneda00_View B) A -> (Yoneda00_View B) A' ) |
Yoneda01_functor Yoneda01} .
Proof.
intros. exists (fun A A' a x => a o>Indexer x).
abstract (split; [intros; exact: polyIndexer_morphism | intros; exact: polyIndexer_unitIndexer]).
Defined.
Lemma Yoneda00_EqFunctor :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(transfL transfR : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf}),
(obIndexer -> Type) .
Proof.
intros until 2. refine ((fun A => {f : Yoneda00_F A | proj1_sig transfL A f = proj1_sig transfR A f})).
Defined.
Lemma Yoneda01_EqFunctor :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(transfL transfR : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf}),
{ Yoneda01 : ( forall A A' : obIndexer, 'Indexer(0 A' ~> A )0 ->
Yoneda00_EqFunctor transfL transfR A ->
Yoneda00_EqFunctor transfL transfR A' ) |
Yoneda01_functor Yoneda01 }.
Proof.
unshelve eexists. intros A A' a f.
exists ((proj1_sig Yoneda01_F) _ _ a (proj1_sig f)).
abstract (simpl in *; rewrite -(proj2_sig transfL)
-(proj2_sig transfR) (proj2_sig f); reflexivity).
abstract (simpl in *; split; [ intros; apply: ax2_Yoneda00_EqFunctor;
apply: (proj1 (proj2_sig Yoneda01_F))
| move => A [x x_eq]; apply: ax2_Yoneda00_EqFunctor;
apply: (proj2 (proj2_sig Yoneda01_F)) ]).
Defined.
End Senses_obCoMod.
Inductive obCoMod : forall Yoneda00 : obIndexer -> Type,
{ Yoneda01 : ( forall A A' : obIndexer, 'Indexer(0 A' ~> A )0 -> Yoneda00 A -> Yoneda00 A' ) |
Yoneda01_functor Yoneda01 } -> Type :=
| View : forall B : obIndexer, @obCoMod (Yoneda00_View B) (Yoneda01_View B)
| EqFunctor : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall (transfL transfR : { transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf }),
@obCoMod (Yoneda00_EqFunctor transfL transfR) (Yoneda01_EqFunctor transfL transfR) .
(**#+END_SRC
** Grammatical presentation of morphisms
#+BEGIN_SRC coq :exports both :results silent **)
Section Senses_morCoMod.
Lemma Yoneda10_PolyCoMod :
forall Yoneda00_F1 Yoneda01_F1 Yoneda00_F2 Yoneda01_F2
(Yoneda10_ff_ : {Yoneda10 : ( forall A : obIndexer, Yoneda00_F1 A -> Yoneda00_F2 A ) |
Yoneda10_natural Yoneda01_F1 Yoneda01_F2 Yoneda10 })
Yoneda00_F2' Yoneda01_F2'
(Yoneda10_ff' : {Yoneda10 : ( forall A : obIndexer, Yoneda00_F2 A -> Yoneda00_F2' A ) |
Yoneda10_natural Yoneda01_F2 Yoneda01_F2' Yoneda10}),
{Yoneda10 : ( forall A : obIndexer, Yoneda00_F1 A -> Yoneda00_F2' A ) |
Yoneda10_natural Yoneda01_F1 Yoneda01_F2' Yoneda10}.
Proof.
intros. exists (fun A => (proj1_sig Yoneda10_ff') A \o (proj1_sig Yoneda10_ff_) A ).
abstract (intros; move; intros; simpl;
rewrite (proj2_sig Yoneda10_ff') (proj2_sig Yoneda10_ff_); reflexivity).
Defined.
Lemma Yoneda10_UnitCoMod :
forall Yoneda00_F Yoneda01_F,
{Yoneda10 : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_F A ) |
Yoneda10_natural Yoneda01_F Yoneda01_F Yoneda10 } .
Proof.
intros. exists (fun A => id).
abstract (intros; move; intros; reflexivity).
Defined.
Lemma Yoneda10_PolyYoneda00 :
forall Yoneda00_F Yoneda01_F (B : obIndexer) (f : Yoneda00_F B),
{Yoneda10 : ( forall A : obIndexer, Yoneda00_View B A -> Yoneda00_F A ) |
Yoneda10_natural (Yoneda01_View B) Yoneda01_F Yoneda10} .
Proof.
intros. exists (fun A b => proj1_sig Yoneda01_F _ _ b f) .
abstract (intros; move; intros; apply: (proj1 (proj2_sig Yoneda01_F))).
Defined.
Lemma Yoneda10_PolyTransf :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(transf : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf })
(A : obIndexer)
(Yoneda10_ff : {Yoneda10 : ( forall A0 : obIndexer, 'Indexer(0 A0 ~> A )0 -> Yoneda00_F A0 ) |
Yoneda10_natural (Yoneda01_View A) Yoneda01_F Yoneda10 }),
{Yoneda10 : ( forall A0 : obIndexer, 'Indexer(0 A0 ~> A )0 -> Yoneda00_G A0 ) |
Yoneda10_natural (Yoneda01_View A) Yoneda01_G Yoneda10 } .
Proof.
intros. exists (fun A' => (proj1_sig transf) A' \o (proj1_sig Yoneda10_ff) A' ).
abstract (intros; move; intros; simpl in *;
rewrite (proj2_sig transf) (proj2_sig Yoneda10_ff); reflexivity).
Defined.
Lemma Yoneda10_Project1 :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL Yoneda10_transfR : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf }),
forall Yoneda00_Z Yoneda01_Z,
forall Yoneda10_z : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_Z A ) |
Yoneda10_natural Yoneda01_F Yoneda01_Z transf },
{transf : ( forall A : obIndexer, (Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR) A ->
Yoneda00_Z A ) |
Yoneda10_natural (Yoneda01_EqFunctor Yoneda10_transfL Yoneda10_transfR) Yoneda01_Z transf } .
Proof.
intros. exists (fun A f => (proj1_sig Yoneda10_z A) ((proj1_sig f))).
abstract (intros; move; intros; rewrite (proj2_sig Yoneda10_z); reflexivity).
Defined.
Lemma Yoneda10_Pairing :
forall Yoneda00_L Yoneda01_L Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL : {Yoneda10 : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10 })
(Yoneda10_transfR : {Yoneda10 : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10 })
(Yoneda10_ff : {Yoneda10 : ( forall A : obIndexer, Yoneda00_L A -> Yoneda00_F A ) |
Yoneda10_natural Yoneda01_L Yoneda01_F Yoneda10 })
(Yoneda10_ff_eq : (forall A, (proj1_sig Yoneda10_transfL) A \o (proj1_sig Yoneda10_ff) A
=1 (proj1_sig Yoneda10_transfR) A \o (proj1_sig Yoneda10_ff) A)),
{Yoneda10 : ( forall A : obIndexer, Yoneda00_L A ->
(Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR) A ) |
Yoneda10_natural Yoneda01_L (Yoneda01_EqFunctor Yoneda10_transfL Yoneda10_transfR) Yoneda10 }.
Proof.
intros. unshelve eexists. intros A l.
exists (proj1_sig Yoneda10_ff A l).
abstract (exact: Yoneda10_ff_eq). intros; move; intros; simpl.
abstract (intros; move; intros; simpl;
apply: ax2_Yoneda00_EqFunctor; exact: (proj2_sig Yoneda10_ff)).
Defined.
End Senses_morCoMod.
(*
PolyYoneda00 : View A ~> F
PolyTransf : View A ~> G
Project1 : EqFunctor F G Yoneda10_transfL Yoneda10_transfR ~> Z
Pairing : L ~> EqFunctor F G Yoneda10_transfL Yoneda10_transfR
*)
Reserved Notation "''CoMod' (0 F' ~> F @ Yoneda10 )0" (at level 0, format "''CoMod' (0 F' ~> F @ Yoneda10 )0").
Inductive morCoMod : forall Yoneda00_F Yoneda01_F,
@obCoMod Yoneda00_F Yoneda01_F ->
forall Yoneda00_G Yoneda01_G,
@obCoMod Yoneda00_G Yoneda01_G ->
{ Yoneda10 : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10 } -> Type :=
| PolyCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_F' Yoneda01_F' (F' : @obCoMod Yoneda00_F' Yoneda01_F')
Yoneda10_ff' ,
'CoMod(0 F' ~> F @ Yoneda10_ff' )0 ->
forall Yoneda00_F'' Yoneda01_F'' (F'' : @obCoMod Yoneda00_F'' Yoneda01_F'')
Yoneda10_ff_ ,
'CoMod(0 F'' ~> F' @ Yoneda10_ff_ )0 ->
'CoMod(0 F'' ~> F @ Yoneda10_PolyCoMod Yoneda10_ff_ Yoneda10_ff' )0
| UnitCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
'CoMod(0 F ~> F @ Yoneda10_UnitCoMod Yoneda01_F )0
| PolyYoneda00 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
(A : obIndexer) (f : Yoneda00_F A),
'CoMod(0 View A ~> F @ Yoneda10_PolyYoneda00 Yoneda01_F f )0
| PolyTransf : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
(transf : {transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf})
(A : obIndexer) Yoneda10_ff ,
'CoMod(0 View A ~> F @ Yoneda10_ff )0 ->
'CoMod(0 View A ~> G @ Yoneda10_PolyTransf transf Yoneda10_ff )0
(* similar as inclusion , similar as restriction *)
| Project1 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL ,
'CoMod(0 F ~> G @ Yoneda10_transfL )0 ->
forall Yoneda10_transfR ,
'CoMod(0 F ~> G @ Yoneda10_transfR )0 ->
forall Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz,
'CoMod(0 F ~> Z @ Yoneda10_zz )0 ->
'CoMod(0 EqFunctor F G Yoneda10_transfL Yoneda10_transfR ~> Z @
Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz )0
(* similar as corestriction of codomain ;
similar as internalization-as-second-component of external equation *)
| Pairing : forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL,
'CoMod(0 F ~> G @ Yoneda10_transfL )0 ->
forall Yoneda10_transfR,
'CoMod(0 F ~> G @ Yoneda10_transfR )0 ->
forall Yoneda10_ff,
'CoMod(0 L ~> F @ Yoneda10_ff )0 ->
forall Yoneda10_ff_eq : forall A, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A,
'CoMod(0 L ~> EqFunctor F G Yoneda10_transfL Yoneda10_transfR @
Yoneda10_Pairing Yoneda10_ff_eq )0
where "''CoMod' (0 F' ~> F @ Yoneda10 )0" := (@morCoMod _ _ F' _ _ F Yoneda10) : poly_scope.
Notation "''CoMod' (0 F' ~> F )0" :=
(@morCoMod _ _ F' _ _ F _) (at level 0, only parsing, format "''CoMod' (0 F' ~> F )0") : poly_scope.
Notation "ff_ o>CoMod ff'" :=
(@PolyCoMod _ _ _ _ _ _ _ ff' _ _ _ _ ff_) (at level 40 , ff' at next level , left associativity) : poly_scope.
Notation "@ ''UnitCoMod' F" := (@UnitCoMod _ _ F) (at level 10, only parsing) : poly_scope.
Notation "''UnitCoMod'" := (@UnitCoMod _ _ _) (at level 0) : poly_scope.
Notation "''PolyYoneda00' F f" := (@PolyYoneda00 _ _ F _ f) (at level 10, F at next level, f at next level) : poly_scope.
Notation "ff o>Transf_ transf @ G" :=
(@PolyTransf _ _ _ _ _ G transf _ _ ff) (at level 3, transf at next level, G at level 0, left associativity) : poly_scope.
Notation "ff o>Transf_ transf" :=
(@PolyTransf _ _ _ _ _ _ transf _ _ ff) (at level 3, transf at next level) : poly_scope.
Notation "~_1 @ transfL , transfR o>CoMod zz" :=
(@Project1 _ _ _ _ _ _ _ transfL _ transfR _ _ _ _ zz) (at level 4, transfL at next level, transfR at next level , zz at level 4, right associativity) : poly_scope.
Notation "~_1 o>CoMod zz" :=
(@Project1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ zz) (at level 4, zz at level 4) : poly_scope.
Notation "<< ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ transfL _ transfR _ ff Yoneda10_ff_eq) (at level 4 , ff at level 40 , Yoneda10_ff_eq at level 9, transfL at level 40 , transfR at level 40) : poly_scope.
Notation "<< ff ,CoMod Yoneda10_ff_eq >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ _ _ _ _ ff Yoneda10_ff_eq) (at level 4 , ff at level 40 , Yoneda10_ff_eq at level 9) : poly_scope.
Notation "<< ff @ transfL , transfR >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ transfL _ transfR _ ff _) (at level 4 , ff at level 40 , transfL at level 40 , transfR at level 40) : poly_scope.
Notation "<< ff ,CoMod >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ _ _ _ _ ff _) (at level 4 , ff at level 40) : poly_scope.
(**#+END_SRC
* Grammatical conversions of morphisms , which infer the same sense-decoding
As common, the grammatical conversions are classified into the total/(multi-step) conversions , and the congruences conversions , and the atomics conversions which are used in the polymorphism/cut-elimination lemma , and the atomics conversions which are only for the wanted sense of equalizers-grammar , and the atomics conversions which are only for the confluence lemma .
In contrast, now the congruences enable also any conversion of each of the grammatical two-equalized-morphisms parameters, as long as the sense-decoding stays the same.
Also in contrast, because of the embedded extra-indexes in the type-family of the morphisms, the conversion-relation shall convert across two morphisms whose sense-decoding indexes are not syntactically/grammatically-the-same. But oneself does show that, by logical-deduction, these two sense-decoding are indeed propositionally equal ( "soundness lemma" ) .
It is "clear" that, using the polymorphism/cut-elimination lemma and the confluence lemma, oneself shall be able to deduce that the same-sense-decoding property across two morphisms infers grammatical-conversion across these two morphisms ( "completeness lemma" ) ...
Finally, some linear total/asymptotic grade is defined on the morphisms and the tactics-automated degradation lemma shows that each of the conversion indeed degrades the redex morphism .
** Grammatical conversions of morphisms
#+BEGIN_SRC coq :exports both :results silent **)
Section Senses_convCoMod.
Lemma Proj2_Pairing_morphism :
forall Yoneda00_L Yoneda01_L Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10}),
forall (Yoneda10_transfR : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10}),
forall (Yoneda10_ff : {Yoneda10 : forall A : obIndexer, Yoneda00_L A -> Yoneda00_F A |
Yoneda10_natural Yoneda01_L Yoneda01_F Yoneda10}),
forall Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A,
forall Yoneda00_L' Yoneda01_L',
forall (Yoneda10_ll : {Yoneda10 : forall A : obIndexer, Yoneda00_L' A -> Yoneda00_L A |
Yoneda10_natural Yoneda01_L' Yoneda01_L Yoneda10}),
forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o
proj1_sig (Yoneda10_PolyCoMod Yoneda10_ll Yoneda10_ff) A
=1 proj1_sig Yoneda10_transfR A \o
proj1_sig (Yoneda10_PolyCoMod Yoneda10_ll Yoneda10_ff) A .
Proof. intros. move. intro l. apply: Yoneda10_ff_eq. Defined.
Lemma Proj2_Pairing_PolyTransf :
forall (B : obIndexer) Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10})
(Yoneda10_transfR : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10})
(Yoneda10_ff : {Yoneda10 : forall A : obIndexer, Yoneda00_View B A -> Yoneda00_F A |
Yoneda10_natural (Yoneda01_View B) Yoneda01_F Yoneda10})
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR B.
Proof.
intros. exact: (exist _ (proj1_sig Yoneda10_ff _ (@unitIndexer B))
(Yoneda10_ff_eq B (@unitIndexer B))).
Defined.
Lemma Proj2_Project1_Proj2_Pairing :
forall Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10})
(Yoneda10_transfR : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10}),
forall A : obIndexer,
( proj1_sig Yoneda10_transfL A )
\o proj1_sig (Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR
(Yoneda10_UnitCoMod Yoneda01_F)) A
=1 proj1_sig Yoneda10_transfR A
\o proj1_sig (Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR
(Yoneda10_UnitCoMod Yoneda01_F)) A .
Proof.
intros. move. intros [f f_eq]. simpl. apply: f_eq.
Defined.
Lemma Proj2_PolyYoneda00_Pairing :
forall (A : obIndexer) Yoneda00_F Yoneda01_F Yoneda00_G Yoneda01_G
(Yoneda10_transfL : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10})
(Yoneda10_transfR : {Yoneda10 : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10})
(f : Yoneda00_F A)
(Yoneda10_ff_eq : forall A0 : obIndexer,
proj1_sig Yoneda10_transfL A0
\o proj1_sig (Yoneda10_PolyYoneda00 Yoneda01_F f) A0
=1 proj1_sig Yoneda10_transfR A0
\o proj1_sig (Yoneda10_PolyYoneda00 Yoneda01_F f) A0),
Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR A.
Proof.
intros A. intros until Yoneda10_transfR. intros f.
exists f .
rewrite [f](proj2 (proj2_sig Yoneda01_F)).
apply: (Yoneda10_ff_eq A (@unitIndexer A)).
Defined.
End Senses_convCoMod.
Reserved Notation "gg' <~~ gg" (at level 70).
Inductive convCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg ( gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
forall Yoneda10_gg0 ( gg0 : 'CoMod(0 F ~> G @ Yoneda10_gg0 )0 ), Prop :=
(* 1 - computational/total/asymptotic/reduction/(multi-step) *)
| convCoMod_Refl :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
gg <~~ gg
| convCoMod_Trans :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
forall Yoneda10_uTrans (uTrans : 'CoMod(0 F ~> G @ Yoneda10_uTrans )0 ),
( uTrans <~~ gg ) ->
forall Yoneda10_gg0 (gg0 : 'CoMod(0 F ~> G @ Yoneda10_gg0 )0 ),
( gg0 <~~ uTrans ) -> ( gg0 <~~ gg )
(* 2 - congruences
assumed functional-extensionality for transf , therefore no extra congruences ref transf *)
| PolyCoMod_cong_Pre :
forall Yoneda00_F Yoneda01_F' (F' : @obCoMod Yoneda00_F Yoneda01_F')
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda10_ff' (ff' : 'CoMod(0 F' ~> F @ Yoneda10_ff' )0)
Yoneda00_F' Yoneda01_F'' (F'' : @obCoMod Yoneda00_F' Yoneda01_F'')
Yoneda10_ff_ (ff_ : 'CoMod(0 F'' ~> F' @ Yoneda10_ff_ )0)
Yoneda10_ff_0 (ff_0 : 'CoMod(0 F'' ~> F' @ Yoneda10_ff_0 )0),
ff_0 <~~ ff_ -> ( ff_0 o>CoMod ff' ) <~~ ( ff_ o>CoMod ff' )
| PolyCoMod_cong_Post :
forall Yoneda00_F' Yoneda01_F' (F' : @obCoMod Yoneda00_F' Yoneda01_F')
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda10_ff' (ff' : 'CoMod(0 F' ~> F @ Yoneda10_ff' )0)
Yoneda00_F'' Yoneda01_F'' (F'' : @obCoMod Yoneda00_F'' Yoneda01_F'')
Yoneda10_ff_ (ff_ : 'CoMod(0 F'' ~> F' @ Yoneda10_ff_ )0)
Yoneda10_ff'0 (ff'0 : 'CoMod(0 F' ~> F @ Yoneda10_ff'0 )0),
ff'0 <~~ ff' -> ( ff_ o>CoMod ff'0 ) <~~ ( ff_ o>CoMod ff' )
| PolyTransf_cong :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
(transf : {transf : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G transf})
(A : obIndexer)
Yoneda10_ff (ff : 'CoMod(0 View A ~> F @ Yoneda10_ff )0)
Yoneda10_ff0 (ff0 : 'CoMod(0 View A ~> F @ Yoneda10_ff0 )0),
ff0 <~~ ff -> ( ff0 o>Transf_ transf @ G ) <~~ ( ff o>Transf_ transf @ G )
| Project1_cong :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0)
Yoneda10_zz0 (zz0 : 'CoMod(0 F ~> Z @ Yoneda10_zz0 )0),
zz0 <~~ zz ->
( ~_1 @ transfL , transfR o>CoMod zz0 ) <~~ ( ~_1 @ transfL , transfR o>CoMod zz )
| Project1_cong_transfL :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0)
(transfL0 : 'CoMod(0 F ~> G @ Yoneda10_transfL )0),
transfL0 <~~ transfL ->
( ~_1 @ transfL0 , transfR o>CoMod zz ) <~~ ( ~_1 @ transfL , transfR o>CoMod zz )
| Project1_cong_transfR :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0)
(transfR0 : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
transfR0 <~~ transfR ->
( ~_1 @ transfL , transfR0 o>CoMod zz ) <~~ ( ~_1 @ transfL , transfR o>CoMod zz )
| Pairing_cong :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A)
Yoneda10_ff0 (ff0 : 'CoMod(0 L ~> F @ Yoneda10_ff0 )0)
(Yoneda10_ff0_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff0 A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff0 A),
ff0 <~~ ff ->
( << ff0 ,CoMod Yoneda10_ff0_eq @ transfL , transfR >> )
<~~ ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
| Pairing_cong_transfL :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
forall (transfL0 : 'CoMod(0 F ~> G @ Yoneda10_transfL )0),
transfL0 <~~ transfL ->
( << ff ,CoMod Yoneda10_ff_eq @ transfL0 , transfR >> )
<~~ ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
| Pairing_cong_transfR :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
forall (transfR0 : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
transfR0 <~~ transfR ->
( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR0 >> )
<~~ ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
(* 3 - atomics *)
| UnitCoMod_PolyCoMod :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0),
gg <~~ ( gg o>CoMod ('UnitCoMod) )
| PolyCoMod_UnitCoMod :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0),
gg <~~ ( ('UnitCoMod) o>CoMod gg )
| PolyTransf_UnitCoMod :
forall (B : obIndexer)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
(transf : {transf : forall A : obIndexer, (Yoneda00_View B) A -> Yoneda00_G A |
Yoneda10_natural (Yoneda01_View B) Yoneda01_G transf}),
( PolyYoneda00 G (proj1_sig transf _ (@unitIndexer B)) )
<~~ ( (@'UnitCoMod (View B)) o>Transf_ transf @ G )
| PolyYoneda00_PolyYoneda00 :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
(A : obIndexer) (f : Yoneda00_F A) A' (a : Yoneda00_View A A'),
( PolyYoneda00 F (proj1_sig Yoneda01_F A A' a f) )
<~~ ( (PolyYoneda00 (View A) a) o>CoMod (PolyYoneda00 F f) )
| PolyTransf_morphism :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
(transf : {transf : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G transf})
(A : obIndexer)
Yoneda10_ff (ff : 'CoMod(0 View A ~> F @ Yoneda10_ff )0),
forall A' Yoneda10_aa (aa : 'CoMod(0 View A' ~> View A @ Yoneda10_aa )0),
( (aa o>CoMod ff) o>Transf_ transf @ G )
<~~ ( aa o>CoMod (ff o>Transf_ transf @ G) )
| PolyYoneda00_Project1 :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0),
forall (B : obIndexer) (f : Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR B),
( (PolyYoneda00 F (proj1_sig f)) o>CoMod zz )
<~~ ( (PolyYoneda00 (EqFunctor F G Yoneda10_transfL Yoneda10_transfR) f)
o>CoMod ( ~_1 @ transfL , transfR o>CoMod zz ) )
| Pairing_morphism :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A)
Yoneda00_L' Yoneda01_L' (L' : @obCoMod Yoneda00_L' Yoneda01_L')
Yoneda10_ll (ll : 'CoMod(0 L' ~> L @ Yoneda10_ll )0),
( << ll o>CoMod ff
,CoMod (Proj2_Pairing_morphism Yoneda10_ff_eq Yoneda10_ll)
@ transfL , transfR >> )
<~~ ( ll o>CoMod << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
| PolyYoneda00_PolyTransf :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
(transf : {transf : forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A |
Yoneda10_natural Yoneda01_F Yoneda01_G transf})
(A : obIndexer),
forall (f : Yoneda00_F A),
( PolyYoneda00 G (proj1_sig transf _ f) )
<~~ ( (PolyYoneda00 F f) o>Transf_ transf @ G )
| Pairing_PolyTransf :
forall (B : obIndexer) Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 View B ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A)
Yoneda00_H Yoneda01_H (H : @obCoMod Yoneda00_H Yoneda01_H)
(transf : {transf : ( forall A, Yoneda00_EqFunctor Yoneda10_transfL Yoneda10_transfR A ->
Yoneda00_H A ) |
Yoneda10_natural (Yoneda01_EqFunctor Yoneda10_transfL Yoneda10_transfR)
Yoneda01_H transf}),
(PolyYoneda00 H (proj1_sig transf _ (Proj2_Pairing_PolyTransf Yoneda10_ff_eq) ))
<~~ ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> o>Transf_ transf @ H )
| Project1_morphism :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0),
forall Yoneda00_Y Yoneda01_Y (Y : @obCoMod Yoneda00_Y Yoneda01_Y)
Yoneda10_yy (yy : 'CoMod(0 Z ~> Y @ Yoneda10_yy )0),
( ~_1 @ transfL , transfR o>CoMod (zz o>CoMod yy) )
<~~ ( ( ~_1 @ transfL , transfR o>CoMod zz ) o>CoMod yy )
| Pairing_Project1 :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
forall Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0),
forall (Yoneda10_ff_eq :
forall A : obIndexer, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
forall ( _transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 )
( _transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 )
Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0),
( ( ff o>CoMod zz )
: 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod Yoneda10_ff Yoneda10_zz )0 )
<~~ ( ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
o>CoMod ( ~_1 @ _transfL , _transfR o>CoMod zz ) )
: 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod (Yoneda10_Pairing Yoneda10_ff_eq)
(Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz) )0 )
(* for sense *)
| PolyYoneda00_Pairing :
forall (A : obIndexer) Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
forall (f : Yoneda00_F A),
forall Yoneda10_ff_eq : forall A0 : obIndexer,
proj1_sig Yoneda10_transfL A0 \o proj1_sig (Yoneda10_PolyYoneda00 Yoneda01_F f) A0
=1 proj1_sig Yoneda10_transfR A0 \o proj1_sig (Yoneda10_PolyYoneda00 Yoneda01_F f) A0,
( PolyYoneda00 (EqFunctor F G Yoneda10_transfL Yoneda10_transfR)
(Proj2_PolyYoneda00_Pairing Yoneda10_ff_eq) (* exist _ f _ *) )
<~~ ( << (PolyYoneda00 F f) ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
(* for sense *)
| Project1_Proj2_Pairing :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
forall ( _transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
( _transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
(*ALT: more general , already knowing the existence :
forall Proj2_Project1_Proj2_Pairing, *)
( @'UnitCoMod (EqFunctor F G Yoneda10_transfL Yoneda10_transfR) )
<~~ ( << ( ~_1 @ transfL , transfR o>CoMod 'UnitCoMod )
,CoMod (@Proj2_Project1_Proj2_Pairing _ _ _ _ Yoneda10_transfL Yoneda10_transfR)
@ _transfL , _transfR >> )
(* for confluence *)
| Project1_Pairing :
forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0)
Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0)
(Yoneda10_ff_eq : forall A, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
forall Yoneda00_H Yoneda01_H (H : @obCoMod Yoneda00_H Yoneda01_H)
Yoneda10_transfL' (transfL' : 'CoMod(0 L ~> H @ Yoneda10_transfL' )0)
Yoneda10_transfR' (transfR' : 'CoMod(0 L ~> H @ Yoneda10_transfR' )0),
( << ( ~_1 @ transfL' , transfR' o>CoMod ff )
,CoMod (Proj2_Pairing_morphism Yoneda10_ff_eq (Yoneda10_Project1 Yoneda10_transfL' Yoneda10_transfR' ( Yoneda10_UnitCoMod _ ))) @ transfL , transfR >> )
<~~ ( ~_1 @ transfL' , transfR' o>CoMod ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) )
where "gg' <~~ gg" := (@convCoMod _ _ _ _ _ _ _ gg _ gg').
Hint Constructors convCoMod.
(**#+END_SRC
** Same sense-decoding for convertible morphisms
#+BEGIN_SRC coq :exports both :results silent **)
Lemma convCoMod_sense
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
forall Yoneda10_gg0 (gg0 : 'CoMod(0 F ~> G @ Yoneda10_gg0 )0 ),
gg0 <~~ gg -> forall A0, (proj1_sig Yoneda10_gg0 A0) =1 (proj1_sig Yoneda10_gg A0).
Proof.
intros until gg0. intros conv_gg.
elim : Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G
Yoneda10_gg gg Yoneda10_gg0 gg0 / conv_gg .
- (* convCoMod_Refl *) intros. move. intros f. reflexivity.
- (* convCoMod_Trans *) intros until 1. intros gg_eq . intros until 1. intros uTrans_eq.
intros. move. intros f. rewrite -gg_eq -uTrans_eq . reflexivity.
- (* PolyCoMod_cong_Pre *) intros until 2. intros ff__eq . intros. move. intros f''.
rewrite /Yoneda10_PolyCoMod /= . rewrite -ff__eq. reflexivity.
- (* PolyCoMod_cong_Post *) intros until 2. intros ff'_eq . intros. move. intros f''.
rewrite /Yoneda10_PolyCoMod /= . rewrite -ff'_eq. reflexivity.
- (* PolyTransf_cong *) intros until 2. intros ff_eq . intros. move. intros a.
simpl. (* rewrite /Yoneda10_PolyTransf /= . *) rewrite -ff_eq. reflexivity.
- (* Project1_cong *) intros until 3. intros zz_eq . intros. move. intros f.
simpl. (* rewrite /Yoneda10_Project1 /= . *) rewrite -zz_eq. reflexivity.
- (* Project1_cong_transfL *) intros until 3. intros zz_eq . intros. move. intros f.
simpl. (* rewrite /Yoneda10_Project1 /= . *) reflexivity.
- (* Project1_cong_transfR *) intros until 3. intros zz_eq . intros. move. intros f.
simpl. (* rewrite /Yoneda10_Project1 /= . *) reflexivity.
- (* Pairing_cong *) intros until 3. intros ff_eq . intros. move. intros l.
simpl. (* rewrite /Yoneda10_Pairing /= . *)
apply: ax2_Yoneda00_EqFunctor. rewrite -ff_eq. reflexivity.
- (* Pairing_cong_transfL *) intros until 3. intros ff_eq . intros. move. intros l.
simpl. (* rewrite /Yoneda10_Pairing /= . *) reflexivity.
- (* Pairing_cong_transfR *) intros until 3. intros ff_eq . intros. move. intros l.
simpl. (* rewrite /Yoneda10_Pairing /= . *) reflexivity.
- (* UnitCoMod_PolyCoMod *) intros. move. intros f.
simpl. reflexivity.
- (* PolyCoMod_UnitCoMod *) intros. move. intros f.
simpl. reflexivity.
- (* PolyTransf_UnitCoMod *) intros. move. intros b.
simpl. rewrite [LHS](proj2_sig transf). simpl.
congr 1 (proj1_sig transf _) . rewrite -unitIndexer_polyIndexer ; reflexivity .
- (* PolyYoneda00_PolyYoneda00 *) intros. move. intros a'.
simpl. exact: (proj1 (proj2_sig Yoneda01_F)).
- (* PolyTransf_morphism *) intros. move. intros a'. reflexivity.
- (* PolyYoneda00_Project1 *) intros. move. intros b. reflexivity.
- (* Pairing_morphism *) intros. move. intros l'.
simpl. apply: ax2_Yoneda00_EqFunctor. reflexivity.
- (* PolyYoneda00_PolyTransf *) intros. move. intros a. simpl.
exact: (proj2_sig transf).
- (* Pairing_PolyTransf *) intros. move. intros b. cbn -[Yoneda10_Pairing].
rewrite [LHS](proj2_sig transf). simpl.
congr 1 (proj1_sig transf _) . apply: ax2_Yoneda00_EqFunctor.
rewrite [LHS](proj2_sig Yoneda10_ff). simpl.
rewrite -unitIndexer_polyIndexer . reflexivity.
- (* Project1_morphism *) intros. move. intros f. reflexivity.
- (* Pairing_Project1 *) intros. move. intros l. reflexivity.
- (* PolyYoneda00_Pairing *) intros. move. intros a.
simpl. apply: ax2_Yoneda00_EqFunctor. reflexivity.
- (* Project1_Proj2_Pairing *) intros. move. intros [f f_eq].
simpl. apply: ax2_Yoneda00_EqFunctor. reflexivity.
- (* Project1_Pairing *) intros. move. intros [l l_eq].
simpl. apply: ax2_Yoneda00_EqFunctor. reflexivity.
Qed.
Lemma convCoMod_sense'
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
forall Yoneda10_gg0 (gg0 : 'CoMod(0 F ~> G @ Yoneda10_gg0 )0 ),
gg0 <~~ gg -> Yoneda10_gg0 = Yoneda10_gg .
Proof. intros. apply: ax1_Yoneda10_natural. apply: convCoMod_sense. eassumption. Qed.
(**#+END_SRC
** Linear total/asymptotic grade and the degradation lemma
#+BEGIN_SRC coq :exports both :results silent **)
Fixpoint grade Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ) {struct gg} : nat .
Proof.
case : Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_gg / gg .
- intros ? ? F ? ? F' ? ff' ? ? F'' ? ff_ .
exact: ( (S (grade _ _ _ _ _ _ _ ff' + grade _ _ _ _ _ _ _ ff_)%coq_nat ) +
(S (grade _ _ _ _ _ _ _ ff' + grade _ _ _ _ _ _ _ ff_)%coq_nat ) )%coq_nat .
- intros. exact: (S O).
- intros. exact: (S O).
- intros ? ? F ? ? G transf A ? ff .
exact: (S (grade _ _ _ _ _ _ _ ff)).
- intros ? ? F ? ? G ? transfL ? transfR ? ? Z ? zz .
exact: (S ( ( (grade _ _ _ _ _ _ _ transfL) + (grade _ _ _ _ _ _ _ transfR) )%coq_nat + (grade _ _ _ _ _ _ _ zz) )%coq_nat).
- intros ? ? L ? ? F ? ? G ? transfL ? transfR ? ff Yoneda10_ff_eq .
exact: (S ( ( (grade _ _ _ _ _ _ _ transfL) + (grade _ _ _ _ _ _ _ transfR) )%coq_nat + (grade _ _ _ _ _ _ _ ff) )%coq_nat).
Defined.
Lemma grade_gt0 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
((S O) <= (grade gg))%coq_nat.
Proof.
move => Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_gg gg .
apply/leP; case : gg; simpl; auto.
Qed.
Ltac tac_grade_gt0 :=
match goal with
| [ gg1 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg2 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg3 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg4 : 'CoMod(0 _ ~> _ @ _ )0 |- _ ] =>
move : (@grade_gt0 _ _ _ _ _ _ _ gg1) (@grade_gt0 _ _ _ _ _ _ _ gg2)
(@grade_gt0 _ _ _ _ _ _ _ gg3)
(@grade_gt0 _ _ _ _ _ _ _ gg4)
| [ gg1 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg2 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg3 : 'CoMod(0 _ ~> _ @ _ )0 |- _ ] =>
move : (@grade_gt0 _ _ _ _ _ _ _ gg1) (@grade_gt0 _ _ _ _ _ _ _ gg2)
(@grade_gt0 _ _ _ _ _ _ _ gg3)
| [ gg1 : 'CoMod(0 _ ~> _ @ _ )0 ,
gg2 : 'CoMod(0 _ ~> _ @ _ )0 |- _ ] =>
move : (@grade_gt0 _ _ _ _ _ _ _ gg1) (@grade_gt0 _ _ _ _ _ _ _ gg2)
| [ gg1 : 'CoMod(0 _ ~> _ @ _ )0 |- _ ] =>
move : (@grade_gt0 _ _ _ _ _ _ _ gg1)
end.
Lemma degrade
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 )
Yoneda10_ggDeg (ggDeg : 'CoMod(0 F ~> G @ Yoneda10_ggDeg )0 ),
ggDeg <~~ gg -> (* without convCoMod_Refl : ( grade ggDeg < grade gg )%coq_nat *)
( grade ggDeg <= grade gg )%coq_nat .
Proof.
intros until ggDeg. intros red_gg.
elim : Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_gg gg Yoneda10_ggDeg ggDeg / red_gg ;
try solve [ simpl; intros; abstract intuition Omega.omega ].
Qed.
Ltac tac_degrade H_grade :=
repeat match goal with
| [ Hred : ( _ <~~ _ ) |- _ ] =>
move : (degrade Hred) ; clear Hred
end;
move: H_grade; simpl; clear; intros;
try tac_grade_gt0; intros; Omega.omega.
(**#+END_SRC
* Solution
As common, the purely-grammatical polymorphism/cut constructor is not part of the solution .
In contrast, there is one additional half-grammar half-sense cut constructor which embeds any sense natural-transformation (function) into the grammar as some morphism ( in operational form , knowing that the generators/views are dense generators ... ) . Therefore to eliminate this cut is same as to accumulate the effects/applications of this natural-transformation function onto any embedded sense elements (of the metafunctors) .
** Solution morphisms without polymorphism
#+BEGIN_SRC coq :exports both :results silent **)
Module Sol.
Section Section1.
Delimit Scope sol_scope with sol.
(*
PolyYoneda00 : View A ~> F
Project1 : EqFunctor F G Yoneda10_transfL Yoneda10_transfR ~> Z
Pairing : L ~> EqFunctor F G Yoneda10_transfL Yoneda10_transfR
*)
Inductive morCoMod : forall Yoneda00_F Yoneda01_F,
@obCoMod Yoneda00_F Yoneda01_F ->
forall Yoneda00_G Yoneda01_G,
@obCoMod Yoneda00_G Yoneda01_G ->
{ Yoneda10 : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G Yoneda10 } -> Type :=
| UnitCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
'CoMod(0 F ~> F @ Yoneda10_UnitCoMod Yoneda01_F )0
| PolyYoneda00 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
(A : obIndexer) (f : Yoneda00_F A),
'CoMod(0 View A ~> F @ Yoneda10_PolyYoneda00 Yoneda01_F f )0
(* similar as inclusion , similar as restriction *)
| Project1 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL ,
'CoMod(0 F ~> G @ Yoneda10_transfL )0 ->
forall Yoneda10_transfR ,
'CoMod(0 F ~> G @ Yoneda10_transfR )0 ->
forall Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz,
'CoMod(0 F ~> Z @ Yoneda10_zz )0 ->
'CoMod(0 EqFunctor F G Yoneda10_transfL Yoneda10_transfR ~> Z @
Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz )0
(* similar as corestriction of codomain ;
similar as internalization-as-second-component of external equation *)
| Pairing : forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL,
'CoMod(0 F ~> G @ Yoneda10_transfL )0 ->
forall Yoneda10_transfR,
'CoMod(0 F ~> G @ Yoneda10_transfR )0 ->
forall Yoneda10_ff,
'CoMod(0 L ~> F @ Yoneda10_ff )0 ->
forall Yoneda10_ff_eq : forall A, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A,
'CoMod(0 L ~> EqFunctor F G Yoneda10_transfL Yoneda10_transfR @
Yoneda10_Pairing Yoneda10_ff_eq )0
where "''CoMod' (0 F' ~> F @ Yoneda10 )0" := (@morCoMod _ _ F' _ _ F Yoneda10) : sol_scope.
End Section1.
Module Import Ex_Notations.
Delimit Scope sol_scope with sol.
Notation "''CoMod' (0 F' ~> F @ Yoneda10 )0" := (@morCoMod _ _ F' _ _ F Yoneda10) : sol_scope.
Notation "''CoMod' (0 F' ~> F )0" := (@morCoMod _ _ F' _ _ F _) (at level 0, only parsing, format "''CoMod' (0 F' ~> F )0") : sol_scope.
Notation "@ ''UnitCoMod' F" := (@UnitCoMod _ _ F) (at level 10, only parsing) : sol_scope.
Notation "''UnitCoMod'" := (@UnitCoMod _ _ _) (at level 0) : sol_scope.
Notation "''PolyYoneda00' F f" := (@PolyYoneda00 _ _ F _ f) (at level 10, F at next level, f at next level) : sol_scope.
Notation "~_1 @ transfL , transfR o>CoMod zz" :=
(@Project1 _ _ _ _ _ _ _ transfL _ transfR _ _ _ _ zz) (at level 4, transfL at next level, transfR at next level , zz at level 4, right associativity) : sol_scope.
Notation "~_1 o>CoMod zz" :=
(@Project1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ zz) (at level 4, zz at level 4) : sol_scope.
Notation "<< ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ transfL _ transfR _ ff Yoneda10_ff_eq) (at level 4 , ff at level 40 , Yoneda10_ff_eq at level 9, transfL at level 40 , transfR at level 40) : sol_scope.
Notation "<< ff ,CoMod Yoneda10_ff_eq >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ _ _ _ _ ff Yoneda10_ff_eq) (at level 4 , ff at level 40 , Yoneda10_ff_eq at level 9) : sol_scope.
Notation "<< ff @ transfL , transfR >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ transfL _ transfR _ ff _) (at level 4 , ff at level 40 , transfL at level 40 , transfR at level 40) : sol_scope.
Notation "<< ff ,CoMod >>" :=
(@Pairing _ _ _ _ _ _ _ _ _ _ _ _ _ _ ff _) (at level 4 , ff at level 40) : sol_scope.
End Ex_Notations.
Definition toCoMod :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 %sol ),
'CoMod(0 F ~> G @ Yoneda10_gg )0 .
Proof.
(move => Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_gg gg);
elim : Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_gg / gg =>
[ ? ? F
| ? ? F A f
| ? ? F ? ? G ? transfL transfLSol ? transfR transfRSol ? ? Z ? zz zzSol
| ? ? L ? ? F ? ? G ? transfL transfLSol ? transfR transfRSol ? ff ffSol Yoneda10_ff_eq ];
[ apply: (@'UnitCoMod F)
| apply: ( 'PolyYoneda00 F f )
| apply: ( ~_1 @ transfLSol , transfRSol o>CoMod zzSol)
| apply: ( << ffSol ,CoMod Yoneda10_ff_eq @ transfLSol , transfRSol >> )].
Defined.
(**#+END_SRC
** Destruction of morphisms with inner-instantiation of object-indexes
Regardless the extra-indexes in the type-families , oneself easily still-gets the common dependent-destruction of morphisms with inner-instantiation of object-indexes
#+BEGIN_SRC coq :exports both :results silent **)
Module Destruct_domView.
(*
PolyYoneda00 : View A ~> F
Project1 : EqFunctor F G Yoneda10_transfL Yoneda10_transfR ~> Z
Pairing : L ~> EqFunctor F G Yoneda10_transfL Yoneda10_transfR
*)
Inductive morCoMod_domView
: forall (B : obIndexer), forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F ),
forall Yoneda10_ff, 'CoMod(0 (View B) ~> F @ Yoneda10_ff )0 %sol -> Type :=
| UnitCoMod : forall B : obIndexer,
morCoMod_domView ( ( @'UnitCoMod (View B) )%sol )
| PolyYoneda00 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
(A : obIndexer) (f : Yoneda00_F A),
morCoMod_domView ( ( 'PolyYoneda00 F f )%sol )
| Pairing : forall (B : obIndexer) Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 %sol )
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 %sol ),
forall Yoneda10_ff (ff : 'CoMod(0 (View B) ~> F @ Yoneda10_ff )0 %sol),
forall Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A,
morCoMod_domView ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )%sol ) .
Lemma morCoMod_domViewP
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 %sol ),
ltac:( destruct F; [ | intros; refine (unit : Type) ];
refine (morCoMod_domView gg) ).
Proof.
intros. case: _ _ F _ _ G Yoneda10_gg / gg.
- destruct F; [ | intros; exact: tt ].
constructor 1.
- constructor 2.
- intros; exact: tt.
- destruct L; [ | intros; exact: tt ].
constructor 3.
Defined.
End Destruct_domView.
Module Destruct_domEqFunctor.
Inductive morCoMod_domEqFunctor
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F ),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G ),
forall (transfL transfR : { transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf }),
forall Yoneda00_H Yoneda01_H (H : @obCoMod Yoneda00_H Yoneda01_H ),
forall Yoneda10_hh, 'CoMod(0 (EqFunctor F G transfL transfR) ~> H @ Yoneda10_hh )0 %sol -> Type :=
| UnitCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F ),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G ),
forall (transfL transfR : { transf : ( forall A : obIndexer, Yoneda00_F A -> Yoneda00_G A ) |
Yoneda10_natural Yoneda01_F Yoneda01_G transf }),
morCoMod_domEqFunctor ( @'UnitCoMod (EqFunctor F G transfL transfR) )%sol
| Project1 : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 %sol),
forall Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 %sol),
forall Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0 %sol),
morCoMod_domEqFunctor ( ~_1 @ transfL , transfR o>CoMod zz )%sol
| Pairing : forall Yoneda00_F' Yoneda01_F' (F' : @obCoMod Yoneda00_F' Yoneda01_F' )
Yoneda00_G' Yoneda01_G' (G' : @obCoMod Yoneda00_G' Yoneda01_G' )
(transfL' transfR' : { transf : ( forall A : obIndexer, Yoneda00_F' A -> Yoneda00_G' A ) |
Yoneda10_natural Yoneda01_F' Yoneda01_G' transf })
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 %sol )
Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 %sol )
Yoneda10_ff (ff : 'CoMod(0 (EqFunctor F' G' transfL' transfR') ~> F @ Yoneda10_ff )0 %sol )
(Yoneda10_ff_eq : forall A : obIndexer,
proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A
=1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A),
morCoMod_domEqFunctor ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )%sol .
Lemma morCoMod_domEqFunctorP
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
forall Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
forall Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 %sol ),
ltac:( destruct F; [ intros; refine (unit : Type) | ];
refine (morCoMod_domEqFunctor gg) ).
Proof.
intros. case: _ _ F _ _ G Yoneda10_gg / gg.
- destruct F; [ intros; exact: tt | ].
constructor 1.
- intros; exact: tt.
- constructor 2.
- destruct L; [ intros; exact: tt | ].
constructor 3.
Defined.
End Destruct_domEqFunctor.
End Sol.
(**#+END_SRC
* Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution
As common, this resolution is by some non-structurally recursive function .
In contrast, this resolution also computes the sense-decoding index of the resolved morphism, this index is inferred as metavariable from the actual resolved morphism via the [eexists] tactic. The technical progress of this resolution does require the earlier lemma that convertible morphisms do have the sense-decoding indexes.
This COQ program and deduction is mostly-automated ; but memo that COQ lacks inductive-recursive presentations and memo that here the automation-tactics use only logical eauto-resolution because COQ lacks some more-efficient heterogeneous-rewriting tactics, because the conversion-relation do convert across two morphisms whose sense-decoding indexes are not syntactically/grammatically-the-same.
#+BEGIN_SRC coq :exports both :results silent **)
Module Resolve.
Import Sol.Ex_Notations.
Ltac tac_reduce := simpl in *; (intuition (try subst; eauto 9)).
Fixpoint solveCoMod len {struct len} :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G)
Yoneda10_gg (gg : 'CoMod(0 F ~> G @ Yoneda10_gg )0 ),
forall grade_gg : (grade gg <= len)%coq_nat,
{ Yoneda10_ggSol : _ & { ggSol : 'CoMod(0 F ~> G @ Yoneda10_ggSol )0 %sol
| (Sol.toCoMod ggSol) <~~ gg } }.
Proof.
case : len => [ | len ].
(* len is O *)
- ( move => ? ? F ? ? G ? gg grade_gg ); exfalso; abstract tac_degrade grade_gg.
(* len is (S len) *)
- move => ? ? F ? ? G Yoneda10_gg gg; case : _ _ F _ _ G Yoneda10_gg / gg =>
[ Yoneda00_F Yoneda01_F F Yoneda00_F' Yoneda01_F' F'
Yoneda10_ff' ff' Yoneda00_F'' Yoneda01_F'' F''
Yoneda10_ff_ ff_ (* ff_ o>CoMod ff' *)
| Yoneda00_F Yoneda01_F F (* @'UnitCoMod F *)
| Yoneda00_F Yoneda01_F F A f (* PolyYoneda00 F f *)
| Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G
transf A Yoneda10_ff ff (* ff o>Transf_ transf @ G *)
| Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G Yoneda10_transfL transfL
Yoneda10_transfR transfR Yoneda00_Z Yoneda01_Z Z Yoneda10_zz zz
(* ~_1 @ transfL , transfR o>CoMod zz *)
| Yoneda00_L Yoneda01_L L Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G
Yoneda10_transfL transfL Yoneda10_transfR transfR
Yoneda10_ff ff Yoneda10_ff_eq
(* << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> *)
] grade_gg .
(* gg is ff_ o>CoMod ff' *)
+ all: cycle 1.
(* gg is @'UnitCoMod F *)
+ eexists. exists (@'UnitCoMod F)%sol. apply: convCoMod_Refl.
(* gg is PolyYoneda00 F f *)
+ eexists. exists ('PolyYoneda00 F f)%sol. apply: convCoMod_Refl.
(* gg is ff o>Transf_ transf @ G *)
+ case : (solveCoMod len _ _ _ _ _ _ _ ff)
=> [ | Yoneda10_ffSol [ffSol ffSol_prop] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' ffSol_prop) => ffSol_prop_eq; subst.
clear - solveCoMod grade_gg ffSol_prop.
move: (Sol.Destruct_domView.morCoMod_domViewP ffSol) => ffSol_domViewP.
destruct ffSol_domViewP as
[ B (* @'UnitCoMod (View B) *)
| Yoneda00_F Yoneda01_F F A f (* PolyYoneda00 F f *)
| B Yoneda00_F Yoneda01_F F _Yoneda00_G _Yoneda01_G _G Yoneda10_transfL transfL
Yoneda10_transfR transfR _Yoneda10_ff _ff _Yoneda10_ff_eq
(* << _ff ,CoMod _Yoneda10_ff_eq @ transfL , transfR >> *)
] .
* eexists. exists ( 'PolyYoneda00 G (proj1_sig transf _ (@unitIndexer B)) )%sol.
clear -ffSol_prop.
simpl in *; eapply convCoMod_Trans with
(uTrans := ('UnitCoMod) o>Transf_ transf ); abstract tac_reduce.
* eexists. exists ( 'PolyYoneda00 G (proj1_sig transf _ f) )%sol.
clear -ffSol_prop.
simpl in *; eapply convCoMod_Trans with
(uTrans := (PolyYoneda00 F f) o>Transf_ transf ); abstract tac_reduce.
* eexists. exists ( 'PolyYoneda00 _ (proj1_sig transf _ (Proj2_Pairing_PolyTransf _Yoneda10_ff_eq) ) )%sol.
clear -ffSol_prop.
simpl in *; eapply convCoMod_Trans with
(uTrans := ( << Sol.toCoMod _ff ,CoMod _Yoneda10_ff_eq @ Sol.toCoMod transfL , Sol.toCoMod transfR >> ) o>Transf_ transf ); abstract tac_reduce.
(* gg is ~_1 @ transfL , transfR o>CoMod zz *)
+ case: (solveCoMod len _ _ _ _ _ _ _ transfL)
=> [ | Yoneda10_transfLSol [ transfLSol transfLSol_prop ] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' transfLSol_prop) => transfLSol_prop_eq; subst.
case: (solveCoMod len _ _ _ _ _ _ _ transfR)
=> [ | Yoneda10_transfRSol [ transfRSol transfRSol_prop ] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' transfRSol_prop) => transfRSol_prop_eq; subst.
case: (solveCoMod len _ _ _ _ _ _ _ zz) => [ | Yoneda10_zzSol [ zzSol zzSol_prop ] ]; first by abstract tac_degrade grade_gg.
eexists. exists ( ~_1 @ transfLSol , transfRSol o>CoMod zzSol )%sol.
clear - transfLSol_prop transfRSol_prop zzSol_prop. abstract tac_reduce.
(* gg is << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> *)
+ case: (solveCoMod len _ _ _ _ _ _ _ transfL)
=> [ | Yoneda10_transfLSol [ transfLSol transfLSol_prop ] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' transfLSol_prop) => transfLSol_prop_eq; subst.
case: (solveCoMod len _ _ _ _ _ _ _ transfR)
=> [ | Yoneda10_transfRSol [ transfRSol transfRSol_prop ] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' transfRSol_prop) => transfRSol_prop_eq; subst.
move: (solveCoMod len _ _ _ _ _ _ _ ff)
=> [ | Yoneda10_ffSol [ffSol ffSol_prop] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' ffSol_prop) => ffSol_prop_eq; subst.
eexists. exists ( << ffSol ,CoMod Yoneda10_ff_eq @ transfLSol , transfRSol >> )%sol.
clear - transfLSol_prop transfRSol_prop ffSol_prop. abstract tac_reduce.
(* gg is ff_ o>CoMod ff' *)
+ move: (solveCoMod len _ _ _ _ _ _ _ ff_)
=> [ | Yoneda10_ff_Sol [ff_Sol ff_Sol_prop] ];
first by abstract tac_degrade grade_gg.
move: (solveCoMod len _ _ _ _ _ _ _ ff')
=> [ | Yoneda10_ff'Sol [ff'Sol ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) *)
destruct ff_Sol as
[ _Yoneda00_F _Yoneda01_F _F (* @'UnitCoMod _F %sol *)
| _Yoneda00_F _Yoneda01_F _F A f (* 'PolyYoneda00 _F f *)
| _Yoneda00_F _Yoneda01_F _F Yoneda00_G Yoneda01_G G Yoneda10_transfL transfL
Yoneda10_transfR transfR Yoneda00_Z Yoneda01_Z Z Yoneda10_zz zz
(* ~_1 @ transfL , transfR o>CoMod zz %sol *)
| Yoneda00_L Yoneda01_L L _Yoneda00_F _Yoneda01_F _F
Yoneda00_G Yoneda01_G G Yoneda10_transfL transfL Yoneda10_transfR transfR
Yoneda10_ff ff Yoneda10_ff_eq
(* << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> %sol *)
] .
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ((@'UnitCoMod _F) o>CoMod ff'Sol) *)
* eexists. exists (ff'Sol).
clear -ff_Sol_prop ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := ('UnitCoMod) o>CoMod (ff')); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ('UnitCoMod) o>CoMod (Sol.toCoMod ff'Sol)); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ff'Sol) *)
* { destruct ff'Sol as
[ Yoneda00_F Yoneda01_F F (* @'UnitCoMod F %sol *)
| Yoneda00_F Yoneda01_F F _A _f (* 'PolyYoneda00 F _f *)
| Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G
Yoneda10_transfL transfL Yoneda10_transfR transfR
Yoneda00_Z Yoneda01_Z Z Yoneda10_zz zz
(* ~_1 @ transfL , transfR o>CoMod zz %sol *)
| Yoneda00_L Yoneda01_L L _Yoneda00_F _Yoneda01_F _F Yoneda00_G Yoneda01_G G
Yoneda10_transfL transfL Yoneda10_transfR transfR
Yoneda10_ff ff Yoneda10_ff_eq
(* << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> %sol *)
] .
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod (@'UnitCoMod F)) *)
- eexists. exists ( 'PolyYoneda00 _ f ) %sol .
clear -ff_Sol_prop ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := ( ff_) o>CoMod ('UnitCoMod)); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ('PolyYoneda00 F _f)) *)
- eexists. exists ( 'PolyYoneda00 F (proj1_sig Yoneda01_F _ _ f _f) ) %sol .
clear -ff_Sol_prop ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := (PolyYoneda00 _ f) o>CoMod (ff')); first (by eauto);
eapply convCoMod_Trans with
(uTrans := (PolyYoneda00 _ f) o>CoMod (PolyYoneda00 _ _f)); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod (~_1 @ transfL , transfR o>CoMod zz)) *)
- move: (solveCoMod len _ _ _ _ _ _ _ ( (PolyYoneda00 _ (proj1_sig f)) o>CoMod (Sol.toCoMod zz)))
=> [ | Yoneda10_ff_Sol_o_ff'Sol [ff_Sol_o_ff'Sol ff_Sol_o_ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
eexists. exists ( ff_Sol_o_ff'Sol ) .
clear -ff_Sol_prop ff'Sol_prop ff_Sol_o_ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := (PolyYoneda00 _ f) o>CoMod (ff')); first (by eauto);
eapply convCoMod_Trans with
(uTrans := (PolyYoneda00 _ f) o>CoMod (~_1 @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) o>CoMod (Sol.toCoMod zz))); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( (PolyYoneda00 _ (proj1_sig f)) o>CoMod (Sol.toCoMod zz))); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod ff'Sol) , is (('PolyYoneda00 _F f) o>CoMod (<< ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >>)) *)
- move: (solveCoMod len _ _ _ _ _ _ _ ( << (PolyYoneda00 _ f) o>CoMod (Sol.toCoMod ff) ,CoMod (Proj2_Pairing_morphism Yoneda10_ff_eq (Yoneda10_PolyYoneda00 _ f)) @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ))
=> [ | Yoneda10_ff_Sol_o_ff'Sol [ff_Sol_o_ff'Sol ff_Sol_o_ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
eexists. exists ( ff_Sol_o_ff'Sol ) .
clear -ff_Sol_prop ff'Sol_prop ff_Sol_o_ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with (uTrans := (PolyYoneda00 _ f) o>CoMod (ff')); first (by eauto);
eapply convCoMod_Trans with (uTrans := (PolyYoneda00 _ f) o>CoMod ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> )); first (by eauto);
eapply convCoMod_Trans with (uTrans := ( << (PolyYoneda00 _ f) o>CoMod (Sol.toCoMod ff) ,CoMod (Proj2_Pairing_morphism Yoneda10_ff_eq (Yoneda10_PolyYoneda00 _ f)) @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> )); by eauto).
}
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ((~_1 @ transfL , transfR o>CoMod zz) o>CoMod ff'Sol) *)
* move: (solveCoMod len _ _ _ _ _ _ _ ( (Sol.toCoMod zz) o>CoMod (Sol.toCoMod ff'Sol) ))
=> [ | Yoneda10_ff_Sol_o_ff'Sol [ff_Sol_o_ff'Sol ff_Sol_o_ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
eexists. exists ( ~_1 @ transfL , transfR o>CoMod ff_Sol_o_ff'Sol )%sol .
clear -ff_Sol_prop ff'Sol_prop ff_Sol_o_ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := ( ~_1 @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) o>CoMod (Sol.toCoMod zz) ) o>CoMod ff'); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( ~_1 @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) o>CoMod (Sol.toCoMod zz) ) o>CoMod (Sol.toCoMod ff'Sol)); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( ~_1 @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) o>CoMod ( (Sol.toCoMod zz) o>CoMod (Sol.toCoMod ff'Sol) ) )); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) o>CoMod ff'Sol ) *)
* { move: (Sol.Destruct_domEqFunctor.morCoMod_domEqFunctorP ff'Sol) => ff'Sol_domEqFunctorP.
destruct ff'Sol_domEqFunctorP as
[ Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G _transfL _transfR
(* @'UnitCoMod (EqFunctor F G _transfL _transfR) *)
| Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G _Yoneda10_transfL _transfL
_Yoneda10_transfR _transfR Yoneda00_Z Yoneda01_Z Z Yoneda10_zz zz
(* ~_1 @ _transfL , _transfR o>CoMod zz *)
| Yoneda00_F' Yoneda01_F' F' Yoneda00_G' Yoneda01_G' G' transfL' transfR'
Yoneda00_F Yoneda01_F F Yoneda00_G Yoneda01_G G _Yoneda10_transfL
_transfL _Yoneda10_transfR _transfR _Yoneda10_ff _ff _Yoneda10_ff_eq
(* << _ff ,CoMod _Yoneda10_ff_eq @ _transfL , _transfR >> *)
] .
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) o>CoMod (@'UnitCoMod (EqFunctor F G _transfL _transfR) ) *)
- eexists. exists ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) %sol .
clear -ff_Sol_prop ff'Sol_prop.
abstract (simpl in *; eapply convCoMod_Trans with
(uTrans := ( ff_ ) o>CoMod ('UnitCoMod)); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) o>CoMod ( ~_1 @ _transfL , _transfR o>CoMod zz ) *)
- move: (solveCoMod len _ _ _ _ _ _ _ ( (Sol.toCoMod ff) o>CoMod (Sol.toCoMod zz) ))
=> [ | Yoneda10_ff_Sol_o_ff'Sol [ff_Sol_o_ff'Sol ff_Sol_o_ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
eexists. exists ( ff_Sol_o_ff'Sol )%sol .
clear -ff_Sol_prop ff'Sol_prop ff_Sol_o_ff'Sol_prop.
(simpl in *; eapply convCoMod_Trans with
(uTrans := ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod ff'); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod ( ~_1 @ (Sol.toCoMod _transfL) , (Sol.toCoMod _transfR) o>CoMod (Sol.toCoMod zz))); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( (Sol.toCoMod ff) o>CoMod (Sol.toCoMod zz) ) ); by eauto).
(* gg is (ff_ o>CoMod ff') , to (ff_Sol o>CoMod ff'Sol) , is ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) o>CoMod ( << _ff ,CoMod _Yoneda10_ff_eq @ _transfL , _transfR >> ) *)
- move: (solveCoMod len _ _ _ _ _ _ _ ( ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod (Sol.toCoMod _ff) ))
=> [ | Yoneda10_ff_Sol_o_ff'Sol [ff_Sol_o_ff'Sol ff_Sol_o_ff'Sol_prop] ];
first by abstract tac_degrade grade_gg.
move : (convCoMod_sense' ff_Sol_o_ff'Sol_prop) => ff_Sol_o_ff'Sol_prop_eq; subst.
pose HeqSol := (Proj2_Pairing_morphism _Yoneda10_ff_eq (Yoneda10_Pairing Yoneda10_ff_eq)).
eexists. exists ( << ff_Sol_o_ff'Sol ,CoMod HeqSol @ _transfL , _transfR >> ) %sol .
clear -ff_Sol_prop ff'Sol_prop ff_Sol_o_ff'Sol_prop.
(simpl in *; eapply convCoMod_Trans with
(uTrans := ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod ff'); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod ( << (Sol.toCoMod _ff) ,CoMod _Yoneda10_ff_eq @ (Sol.toCoMod _transfL) , (Sol.toCoMod _transfR) >> ) ); first (by eauto);
eapply convCoMod_Trans with
(uTrans := ( << ( ( << (Sol.toCoMod ff) ,CoMod Yoneda10_ff_eq @ (Sol.toCoMod transfL) , (Sol.toCoMod transfR) >> ) o>CoMod (Sol.toCoMod _ff) ) ,CoMod HeqSol @ (Sol.toCoMod _transfL) , (Sol.toCoMod _transfR) >> ) ); by eauto).
}
Defined.
End Resolve.
End EQUALIZERS.
(**#+END_SRC
Voila. **)
此处可能存在不合适展示的内容，页面不予展示。您可通过相关编辑功能自查并修改。
如您确认内容无涉及 不当用语 / 纯广告导流 / 暴力 / 低俗色情 / 侵权 / 盗版 / 虚假 / 无价值内容或违法国家有关法律法规的内容，可点击提交进行申诉，我们将尽快为您处理。
马建仓 AI 助手
