-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcartierSolution7.v
2246 lines (1904 loc) · 122 KB
/
cartierSolution7.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** # #
#+TITLE: cartierSolution7.v
Proph
https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution7.v
https://github.com/1337777/cartier/blob/master/cartierSolution7.v.pdf
solves half of some question of Cartier which is how to program grammatical polymorph generated-functor-along-reindexing ( "Kan extension" ) ...
SHORT ::
ERRATA : the (modified) colimits half is erased here and will be presented only later after cartierSolution8.v ... « generated modified colimits » ( « modos » ) .
The ends is to do start with some given generating-functor from some given reindexer-graph into some given generator-graph and then to generate some other extended functor from some given extended indexer-graph into some extension of the given generator-graph ; but where are those outputs of the generated-functor at the indexes ? Oneself could get them as metafunctors over this generator-graph , as long as oneself grammatically-distinguishes whatever-is-interesting .
Memo that the sense of this generated-functor ( « colimits » ) really-is the colimit(-simultaneously) of multiple diagrams , instead of the multiple colimits of each diagram ( "pointwise" ) (I.3.7.2) ... Moreover memo that here the generator-graph is some non-quantified outer/global parameter , instead of some innerly-quantified local argument which is carried around by all the grammatical constructors , in some « polygeneration » (functorial) form , as for some presentation of grammatical right-adjunction (I.3.7.6) ... Elsewhere memo that the generated-functor is similar as some existential-quantification functor ( left adjoint to some preimage functor of the generating-functor ) , therefore oneself may now think of adding logical-connectives to form some external-logic of modos and to attempt polymorph (relative-)quantifier-elimination ...
Now the conversion-relation shall convert across two morphisms whose sense-decoding datatype-indexes/arguments are not syntactically/grammatically-the-same . But oneself does show that , by logical-deduction , these two sense-decodings 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 . But to facilitate the COQ automatic-arithmetic during the degradation lemma , here oneself assumes some finiteness-property on the graph of reindexer elements of each index along the reindexing-functor and also assumes some other finiteness-property on the indexer-graph . Clearly this ongoing COQ program and deduction will still-proceed when those things are confined less than any regular cardinal .
For instant first impression , the sense-decoding ( "Yoneda" ) of the generated-functor-along-reindexing , is written as :
#+BEGIN_EXAMPLE
Definition Yoneda00_Generated (I : obIndexer) (G : obGenerator) :=
{ R : { R : obReIndexer & 'Indexer( ReIndexing0 R |- I ) }
& 'Generator( G ~> Generating0 (projT1 R) ) }.
Axiom Yoneda00_Generated_quotient :
forall (I : obIndexer) (G : obGenerator),
forall (R S : obReIndexer) (rs : 'ReIndexer( R |- S ))
(si : 'Indexer( ReIndexing0 S |- I ))
(gr : 'Generator( G ~> Generating0 R )),
( existT _ (existT _ S si) (gr o>Generator Generating1 rs) )
= ( existT _ (existT _ R (ReIndexing1 rs o>Indexer si)) gr
: Yoneda00_Generated I G ).
#+END_EXAMPLE
KEYWORDS :: 1337777.OOO ; COQ ; cut-elimination ; polymorph generated-functor-along-reindexing ; polymorph metafunctors-grammar ; modos
OUTLINE ::
* Indexer metalogic , generating-views data
+ Indexer metalogic
+ Generating-views data
* Grammatical presentation of objects
+ Sense-decodings of the objects
+ Grammar of the objects , which carry the sense-decodings
* Grammatical presentation of morphisms
+ Sense-decodings of the morphisms
+ Grammar of the morphisms , which carry the sense-decodings
* Solution morphisms
+ Solution morphisms without polymorphism
+ Destruction of morphisms with inner-instantiation of object-indexes
* 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
* Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution
-----
HINT :: free master-engineering ; program this grammatical polymorph viewed-metafunctor-along-views-data ( "sheafification" ) :
#+BEGIN_EXAMPLE
| PolyElement :
Transformations( ( S : SubViewOfGeneratingView G ) ~> F )
-> Transformations( G ~> ViewedMetaFunctor F )
#+END_EXAMPLE
-----
BUY MOM RECURSIVE T-SQUARE :: paypal.me/1337777 [email protected] ; 微信支付 [email protected] ; eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777
-----
* Indexer metalogic , generating-views data
The ends is to start with some given generating-functor from some given reindexer-graph into some given generator-graph and then to generate some other extended functor from some given extended indexer-graph into some extension of the given generator-graph ; but where are those outputs of the generated-functor at the indexes ? Oneself could get them as metafunctors over this generator-graph , as long as oneself grammatically-distinguishes whatever-is-interesting .
Memo that the sense of this generated-functor ( « colimits » ) really-is the colimit(-simultaneously) of multiple diagrams , instead of the multiple colimits of each diagram ( "pointwise" ) ... This is because , in this ongoing COQ program , the input object [(I : obIndexer)] is always innerly-quantified ( inner/local argument instead of outer/global parameter ) . Therefore , if oneself wants to change this into some outer-quantification , then oneself will get , for multiple outer-parameters [(I : obIndexer)] , the grammatical colimit of the diagram (over the graph of the reindexer elements of [I] along the reindexing-functor) determined by [I] (I.3.7.2) .
Moreover memo that , in this ongoing COQ program , the generator-graph is some non-quantified outer/global parameter , instead of some innerly-quantified local argument which is carried around by all the grammatical constructors , in some « polygeneration » (functorial) form , as for some presentation of right adjunction . Therefore , if oneself wants to change this into some polygeneration inner-quantification , then oneself will get some grammatical (right) adjoint/coreflection (in the polygeneration formulation) (I.3.7.6) .
** Indexer metalogic
As common , some reindexing-functor [Parameter ReIndexing0 : obReIndexer -> obIndexer] is given from some reindexer graph to some indexer graph .
In contrast , to facilitate the COQ automatic-arithmetic during the degradation lemma , here oneself shall present the predicate [Inductive is_MorIndexer12_ (I : obIndexer) : forall R : obReIndexer, 'Indexer( ReIndexing0 R |- I ) -> Type] such to force/assume [Axiom is_MorIndexer12_allP] the finiteness of this graph [{ R : obReIndexer & 'Indexer( ReIndexing0 R |- (I : obIndexer) ) }] of common-interest ( « graph of reindexer elements of some index [I] along the reindexing-functor » , in other words : « the preimage of some index [I] along the reindexing-functor » ) ; also some other finiteness is forced/assumed [Axiom is_ObIndexer12_allP] on the indexes of the indexer graph [obIndexer] . Clearly this ongoing COQ program and deduction will still-proceed when those things are confined less than any regular cardinal .
#+BEGIN_SRC coq :exports both :results silent # # **)
From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
Require Psatz.
Module GENERATEDFUNCTOR.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Delimit Scope poly_scope with poly.
Open Scope poly.
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.
Notation "''Indexer' ( A' |- A )" :=
(@morIndexer A' A) (at level 0, format "''Indexer' ( A' |- A )") : poly_scope.
Notation "_@ A'' o>Indexer a'" := (@polyIndexer _ _ a' A'')
(at level 40, A'' at next level, left associativity,
format "_@ A'' o>Indexer a'") : 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( A' |- A ))
(A'' : obIndexer) (a_ : 'Indexer( A'' |- A' )),
forall B (b : 'Indexer( B |- A'' )),
b o>Indexer ( a_ o>Indexer a' ) = ( b o>Indexer a_ ) o>Indexer a' .
Axiom polyIndexer_unitIndexer :
forall (A A' : obIndexer) (a' : 'Indexer( A' |- A )),
a' = ( (@unitIndexer A') o>Indexer a' ) .
Axiom unitIndexer_polyIndexer :
forall (A : obIndexer), forall (A'' : obIndexer) (a_ : 'Indexer( A'' |- A )),
a_ = ( a_ o>Indexer (@unitIndexer A) ) .
Parameter obReIndexer : Type.
Parameter morReIndexer : obReIndexer -> obReIndexer -> Type.
Parameter polyReIndexer :
forall A A', morReIndexer A' A -> forall A'', morReIndexer A'' A' -> morReIndexer A'' A .
Parameter unitReIndexer : forall {A : obReIndexer}, morReIndexer A A.
Notation "''ReIndexer' ( A' |- A )" := (@morReIndexer A' A)
(at level 0, format "''ReIndexer' ( A' |- A )") : poly_scope.
Notation "_@ A'' o>ReIndexer a'" := (@polyReIndexer _ _ a' A'')
(at level 40, A'' at next level, left associativity,
format "_@ A'' o>ReIndexer a'") : poly_scope.
Notation "a_ o>ReIndexer a'" := (@polyReIndexer _ _ a' _ a_)
(at level 40, a' at next level, left associativity) : poly_scope.
Axiom polyReIndexer_morphism :
forall (A A' : obReIndexer) (a' : 'ReIndexer( A' |- A ))
(A'' : obReIndexer) (a_ : 'ReIndexer( A'' |- A' )),
forall B (b : 'ReIndexer( B |- A'' )),
b o>ReIndexer ( a_ o>ReIndexer a' ) = ( b o>ReIndexer a_ ) o>ReIndexer a' .
Axiom polyReIndexer_unitReIndexer :
forall (A A' : obReIndexer) (a' : 'ReIndexer( A' |- A )),
a' = ( (@unitReIndexer A') o>ReIndexer a' ) .
Axiom unitReIndexer_polyReIndexer :
forall (A : obReIndexer), forall (A'' : obReIndexer) (a_ : 'ReIndexer( A'' |- A )),
a_ = ( a_ o>ReIndexer (@unitReIndexer A) ) .
Parameter ReIndexing0 : obReIndexer -> obIndexer.
Parameter ReIndexing1 : forall A A' : obReIndexer,
'ReIndexer( A |- A' ) -> 'Indexer( ReIndexing0 A |- ReIndexing0 A') .
Axiom ReIndexing_morphism :
forall (A A' : obReIndexer) (a' : 'ReIndexer( A' |- A ))
(A'' : obReIndexer) (a_ : 'ReIndexer( A'' |- A' )),
ReIndexing1 ( a_ o>ReIndexer a' ) = ( ReIndexing1 a_ ) o>Indexer ( ReIndexing1 a' ).
Axiom ReIndexing_unitReIndexer :
forall (A : obReIndexer),
(@unitIndexer (ReIndexing0 A)) = ( ReIndexing1 (@unitReIndexer A) ) .
Parameter ObReIndexer1_ : obIndexer -> obReIndexer.
Parameter ObReIndexer2_ : obIndexer -> obReIndexer.
Parameter MorIndexer1_ :
forall I : obIndexer, 'Indexer( ReIndexing0 (ObReIndexer1_ I) |- I ).
Parameter MorIndexer2_ :
forall I : obIndexer, 'Indexer( ReIndexing0 (ObReIndexer2_ I) |- I ).
Inductive is_MorIndexer12_ (I : obIndexer) :
forall R : obReIndexer, 'Indexer( ReIndexing0 R |- I ) -> Type :=
| Is_MorIndexer12_MorIndexer1_ : is_MorIndexer12_ (MorIndexer1_ I)
| Is_MorIndexer12_MorIndexer2_ : is_MorIndexer12_ (MorIndexer2_ I) .
Axiom is_MorIndexer12_allP : forall (I : obIndexer),
forall (R : obReIndexer) (ri : 'Indexer( ReIndexing0 R |- I )), is_MorIndexer12_ ri.
Parameter ObIndexer1 : obIndexer.
Parameter ObIndexer2 : obIndexer.
Inductive is_ObIndexer12 : obIndexer -> Type :=
| Is_ObIndexer12_ObIndexer1 : is_ObIndexer12 (ObIndexer1)
| Is_ObIndexer12_ObIndexer2 : is_ObIndexer12 (ObIndexer2) .
Axiom is_ObIndexer12_allP : forall (I : obIndexer), is_ObIndexer12 I.
(** # #
#+END_SRC
** Generating-views data
As common , some generating functor [Parameter Generating0 : obReIndexer -> obGenerator] is given from some reindexer graph to some generator graph . Each output of the generated-functor at some index is some grammatically-distinguished ( "new" ) metafunctor over this generator graph .
#+BEGIN_SRC coq :exports both :results silent # # **)
Parameter obGenerator : Type.
Parameter morGenerator : obGenerator -> obGenerator -> Type.
Parameter polyGenerator :
forall A A', morGenerator A' A -> forall A'', morGenerator A'' A' -> morGenerator A'' A .
Parameter unitGenerator : forall {A : obGenerator}, morGenerator A A.
Notation "''Generator' ( A' ~> A )" := (@morGenerator A' A)
(at level 0, format "''Generator' ( A' ~> A )") : poly_scope.
Notation "_@ A'' o>Generator a'" := (@polyGenerator _ _ a' A'')
(at level 40, A'' at next level, left associativity,
format "_@ A'' o>Generator a'") : poly_scope.
Notation "a_ o>Generator a'" := (@polyGenerator _ _ a' _ a_)
(at level 40, a' at next level, left associativity) : poly_scope.
Axiom polyGenerator_morphism :
forall (A A' : obGenerator) (a' : 'Generator( A' ~> A ))
(A'' : obGenerator) (a_ : 'Generator( A'' ~> A' )),
forall B (b : 'Generator( B ~> A'' )),
b o>Generator ( a_ o>Generator a' ) = ( b o>Generator a_ ) o>Generator a' .
Axiom polyGenerator_unitGenerator :
forall (A A' : obGenerator) (a' : 'Generator( A' ~> A )),
a' = ( (@unitGenerator A') o>Generator a' ) .
Axiom unitGenerator_polyGenerator :
forall (A : obGenerator), forall (A'' : obGenerator) (a_ : 'Generator( A'' ~> A )),
a_ = ( a_ o>Generator (@unitGenerator A) ) .
Parameter Generating0 : obReIndexer -> obGenerator.
Parameter Generating1 : forall A A' : obReIndexer,
'ReIndexer( A |- A' ) -> 'Generator( Generating0 A ~> Generating0 A') .
Axiom Generating_morphism :
forall (A A' : obReIndexer) (a' : 'ReIndexer( A' |- A ))
(A'' : obReIndexer) (a_ : 'ReIndexer( A'' |- A' )),
Generating1 ( a_ o>ReIndexer a' ) = ( Generating1 a_ ) o>Generator (Generating1 a').
Axiom Generating_unitReIndexer :
forall (A : obReIndexer),
(@unitGenerator (Generating0 A)) = ( Generating1 (@unitReIndexer A) ) .
(** # #
#+END_SRC
* Grammatical presentation of objects
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 .
Memo that these sense-decodings may be held for two ends : (1) to express the cocone logical-condition on any input cocone data as held by the reflector-constructor ( "universality-morphism" , copairing ) ; (2) to express the dependence of the output limit-object on the morphisms contained in some given input diagram . In the ongoing COQ program , the description (2) will not be necessary because the morphisms contained in the input diagrams are touched indirectly and uniformly (essentially-fixed) .
** Sense-decodings of the objects
The elements at some generator [G] of the metafunctor over the generator-graph which is the sense-decoding of the output of the generated-functor at some index [I] is : the reindexer elements [R] of this index [I] along the reindexing-functor which are also above this generator [G] along the generating-functor ; modulo some polyarrowing in the choice of the reindex .
#+BEGIN_EXAMPLE
Definition Yoneda00_Generated (I : obIndexer) (G : obGenerator) :=
{ R : { R : obReIndexer & 'Indexer( ReIndexing0 R |- I ) }
& 'Generator( G ~> Generating0 (projT1 R) ) }.
#+END_EXAMPLE
Memo that in the common formulation , if the reindexing-functor is flat and the generator-graph is locally presentable , then oneself will get this ongoing formulation ; but in reality oneself may start as in this ongoing formulation where it is relaxed (less-requirements) that the universality/limitativeness property of this construction holds simultaneously (inner-quantification) at all the indexes . Moreover memo that in the case that the generator-graph is [Set] of sets , this presentation will give the common definition .
Elsewhere : oneself may see the graph [{ R : obReIndexer & 'Indexer( ReIndexing0 R |- (I : obIndexer) ) }] of the reindexer elements of [I] along the reindexing-functor as some subset/predicate over the whole reindexer-graph , and see the output of the generated-functor at some index [Yoneda00_Generated (I : obIndexer)] as some predicate over the generator-graph . Then the generated-functor is similar as some existential-quantification functor ( left adjoint to some preimage functor of the generating-functor ) , oneself may now think of adding logical-connectives to form some external-logic of modos and to attempt polymorph (relative-)quantifier-elimination ...
#+BEGIN_SRC coq :exports both :results silent # # **)
Definition Yoneda01_functor (Yoneda00 : obGenerator -> Type)
(Yoneda01 : forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00 G -> Yoneda00 G') : Prop :=
( (* binary/composing functoriality *)
( forall G G' (g : 'Generator( G' ~> G)) G'' (g' : 'Generator( G'' ~> G')) x,
Yoneda01 _ _ g' (Yoneda01 _ _ g x) = Yoneda01 _ _ (g' o>Generator g) x ) /\
( (* empty/unit functoriality is held only in PolyElement_Pairing *)
forall G x, x = Yoneda01 _ _ (@unitGenerator G) x ) ) .
Definition Yoneda10_natural
Yoneda00_F (Yoneda01_F : { Yoneda01 : _ | Yoneda01_functor Yoneda01 })
Yoneda00_E (Yoneda01_E : { Yoneda01 : _ | Yoneda01_functor Yoneda01 })
(Yoneda10 : forall G : obGenerator, Yoneda00_F G -> Yoneda00_E G) : Prop :=
forall G G' (g : 'Generator( G' ~> G )) (f : Yoneda00_F G),
(proj1_sig Yoneda01_E) _ _ g (Yoneda10 G f)
= Yoneda10 G' ((proj1_sig Yoneda01_F) _ _ g f) .
Notation "<< R ; i ; g >>" := (existT _ (existT _ R i) g)
(at level 0, format "<< R ; i ; g >>").
Section Senses_obCoMod.
Lemma Yoneda00_View_Generating0 : forall (R : obReIndexer), (obGenerator -> Type).
Proof. intros R. refine (fun A => 'Generator( A ~> Generating0 R ) ). Defined.
Lemma Yoneda01_View_Generating0 : forall (R : obReIndexer),
{Yoneda01 : ( forall A A' : obGenerator,
'Generator( A' ~> A ) -> (Yoneda00_View_Generating0 R) A -> (Yoneda00_View_Generating0 R) A' ) |
Yoneda01_functor Yoneda01} .
Proof.
intros. exists (fun A A' a x => a o>Generator x).
abstract (split; [intros; exact: polyGenerator_morphism
| intros; exact: polyGenerator_unitGenerator]).
Defined.
Definition Yoneda00_Generated (I : obIndexer) (G : obGenerator) :=
{ R : { R : obReIndexer & 'Indexer( ReIndexing0 R |- I ) }
& 'Generator( G ~> Generating0 (projT1 R) ) }.
Axiom Yoneda00_Generated_quotient :
forall (I : obIndexer) (G : obGenerator),
forall (R S : obReIndexer) (rs : 'ReIndexer( R |- S ))
(si : 'Indexer( ReIndexing0 S |- I ))
(gr : 'Generator( G ~> Generating0 R )),
( existT _ ( existT _ S (si) ) (gr o>Generator (Generating1 rs)) )
= ( existT _ ( existT _ R ((ReIndexing1 rs) o>Indexer si) ) (gr)
: Yoneda00_Generated I G ).
Lemma Yoneda01_Generated :
forall (I : obIndexer),
{ Yoneda01 : ( forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Generated I G -> Yoneda00_Generated I G' ) |
Yoneda01_functor Yoneda01 }.
Proof.
unshelve eexists.
- intros G G' g ii.
refine (existT _ (existT _ (projT1 (projT1 ii)) (projT2 (projT1 ii)))
(g o>Generator (projT2 ii))) .
- abstract (split; [ intros; rewrite -polyGenerator_morphism; reflexivity
| intros G ii;
rewrite -polyGenerator_unitGenerator;
destruct ii as [[? ?] ?]; reflexivity ]) .
Defined.
Lemma Yoneda01_Generated_PolyIndexer :
forall (I : obIndexer) (J : obIndexer) (i : 'Indexer( I |- J )),
{Yoneda10 : forall G : obGenerator, Yoneda00_Generated I G -> Yoneda00_Generated J G |
Yoneda10_natural (Yoneda01_Generated I) (Yoneda01_Generated J) Yoneda10} .
intros. unshelve eexists.
refine (fun G gi => existT _ (existT _ (projT1 (projT1 gi))
((projT2 (projT1 gi)) o>Indexer i))
(projT2 gi) ) .
abstract(intros; move; reflexivity).
Defined.
End Senses_obCoMod.
(** # #
#+END_SRC
** Grammar of the objects, which carry the sense-decodings
As common , the [View] constructor is the (covariant) Yoneda-embedding ( therefore [View G] is some contravariant metafunctor ) .
In contrast , the polymorphism/cut-elimination resolution will require the destruction of some morphism which is constrained by the structure of its domain/codomain objects . Therefore it is necessary , to grammatically-distinguish those singleton objects which in-reality came from some indexing/family of many objects ; for example , the output-object of the generated-functor at some index is such object which shall be grammatically distinguished . Now this grammatically-distinguishing is done by using two mutually-inductive datatypes ; more-precisely the datatype for indexed/family objects [obCoMod_indexed] is nested ( non-recursively , for grammatically-remembering-only ... ) within the datatype for singleton objects [obCoMod] .
Moreover in contrast , during the above destruction , oneself wants some additional data to be instantiated/shared , beyond the domain/codomain objects : ( the sense-decoding [Yoneda01_Generated_PolyIndexer] of ) the indexer-arrow (functorial-)actions across the indexed/family objects . Therefore oneself shall make the grammatical presentation of the indexed/family objects carry this additional data via some extra type-index/argument .
#+BEGIN_SRC coq :exports both :results silent # # **)
Inductive obCoMod : forall Yoneda00 : obGenerator -> Type,
{ Yoneda01 : ( forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00 G -> Yoneda00 G' ) |
Yoneda01_functor Yoneda01 } -> Type :=
| AtIndexOb : forall (Yoneda00_F_ : obIndexer -> _) (Yoneda01_F_ : forall I : obIndexer, _)
(Yoneda01_F_Poly : forall I J : obIndexer, 'Indexer( I |- J ) -> _),
(@obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly) ->
forall I : obIndexer, @obCoMod (Yoneda00_F_(I)) (Yoneda01_F_(I))
| View_Generating0 : forall R : obReIndexer, @obCoMod (Yoneda00_View_Generating0 R) (Yoneda01_View_Generating0 R)
with obCoMod_indexed (**memo: non-recursive **) :
forall Yoneda00_ : obIndexer -> obGenerator -> Type,
forall Yoneda01_ : (forall I : obIndexer, { Yoneda01 : ( forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_ I G -> Yoneda00_ I G' ) |
Yoneda01_functor Yoneda01 }),
forall Yoneda01_Poly : (forall I J : obIndexer, 'Indexer( I |- J ) ->
{Yoneda10_Poly_i : forall G : obGenerator, Yoneda00_ I G -> Yoneda00_ J G |
Yoneda10_natural (Yoneda01_ I) (Yoneda01_ J) Yoneda10_Poly_i}), Type :=
| ObCoMod_indexed : forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly,
(forall I : obIndexer, @obCoMod (Yoneda00_F_(I)) (Yoneda01_F_(I))) ->
@obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
| Generated : @obCoMod_indexed Yoneda00_Generated Yoneda01_Generated
Yoneda01_Generated_PolyIndexer .
(** # #
#+END_SRC
* Grammatical presentation of morphisms
** Sense-decodings of the morphisms
The sense-decoding of any morphism is some metatransformation . Memo that these sense-decodings will be held in the constructor [Reflector] to express the cocone logical-condition on any input cocone data as held by the output reflector-constructor ( "universality-morphism" , copairing ) .
Memo that the quotient relation [Yoneda00_Generated_quotient] on the elements of the generated-functor at some index at some generator will be used only once to show the lemma [Yoneda10_CoUnitGenerated_form_morphismReIndexer_morphismIndexer] that the counit ( section/injection ) of the generated-functor is polyarrowing across the indexer and is polyarrowing across the reindexer .
#+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 : obGenerator, Yoneda00_F1 A -> Yoneda00_F2 A |
Yoneda10_natural Yoneda01_F1 Yoneda01_F2 Yoneda10 })
Yoneda00_F2' Yoneda01_F2'
(Yoneda10_ff' : {Yoneda10 : forall A : obGenerator, Yoneda00_F2 A -> Yoneda00_F2' A |
Yoneda10_natural Yoneda01_F2 Yoneda01_F2' Yoneda10}),
{Yoneda10 : ( forall A : obGenerator, 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 : obGenerator, 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_View_Generating1 : forall ( R R' : obReIndexer)
(r : 'ReIndexer( R' |- R )),
{Yoneda10
: forall G : obGenerator,
Yoneda00_View_Generating0 R' G -> Yoneda00_View_Generating0 R G |
Yoneda10_natural (Yoneda01_View_Generating0 R')
(Yoneda01_View_Generating0 R) Yoneda10} .
Proof.
intros. unshelve eexists. intros G.
refine ( _@ G o>Generator (Generating1 r) ) .
abstract (intros; move; simpl; intros; exact: polyGenerator_morphism).
Defined.
Lemma Yoneda10_CoUnitGenerated :
forall (I : obIndexer), forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{ Yoneda10 : forall G : obGenerator, Yoneda00_View_Generating0 R G -> Yoneda00_Generated (I) G |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_Generated I) Yoneda10}.
Proof.
intros. unshelve eexists.
refine (fun G ff => sval (Yoneda01_Generated_PolyIndexer i) G
(existT _ (existT _ R (@unitIndexer (ReIndexing0 R)))
( (* (proj1_sig Yoneda10_rr) G *) ff))).
abstract (intros; move; intros; reflexivity).
Defined.
Lemma Yoneda10_Reflector :
forall (Yoneda00_F_ : obIndexer -> _)
(Yoneda01_F_ : forall I : obIndexer, _)
(Yoneda10_ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{Yoneda10_ff_i : _ |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_F_(I)) Yoneda10_ff_i}),
forall (I : obIndexer),
{Yoneda10 : forall G : obGenerator, Yoneda00_Generated I G -> Yoneda00_F_ I G |
Yoneda10_natural (Yoneda01_Generated I) (Yoneda01_F_ I) Yoneda10} .
Proof.
intros. unshelve eexists.
- intros G ii. refine (sval (Yoneda10_ff_ _ _
(projT2 (projT1 ii))) G (projT2 ii)) .
- abstract (intros G G' g ii;
rewrite [in LHS](proj2_sig (Yoneda10_ff_ _ _ _ )); reflexivity).
Defined.
Definition Yoneda10_functorIndexer (Yoneda00_F_ : obIndexer -> _)
(Yoneda01_F_ : forall I : obIndexer, _)
(Yoneda01_F_Poly : forall I J : obIndexer, 'Indexer( I |- J ) ->
{Yoneda01_F_Poly_i : forall G : obGenerator, Yoneda00_F_ I G -> Yoneda00_F_ J G |
Yoneda10_natural (Yoneda01_F_ I) (Yoneda01_F_ J) Yoneda01_F_Poly_i})
:= ( forall (I J : obIndexer) (i : 'Indexer( I |- J ))
(K : obIndexer) (j : 'Indexer( J |- K )),
forall (G : obGenerator),
sval (Yoneda01_F_Poly J K j) G \o sval (Yoneda01_F_Poly I J i) G
=1 sval (Yoneda01_F_Poly I K (i o>Indexer j)) G ) /\
( forall (I : obIndexer),
forall (G : obGenerator),
id =1 sval (Yoneda01_F_Poly I I (@unitIndexer I)) G ) .
Section Section1.
Variables (Yoneda00_F_ : obIndexer -> _)
(Yoneda01_F_ : forall I : obIndexer, _)
(Yoneda01_F_Poly : forall I J : obIndexer, 'Indexer( I |- J ) ->
{Yoneda01_F_Poly_i : forall G : obGenerator, Yoneda00_F_ I G -> Yoneda00_F_ J G |
Yoneda10_natural (Yoneda01_F_ I) (Yoneda01_F_ J) Yoneda01_F_Poly_i})
(Yoneda10_ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{Yoneda10_ff_i : forall G : obGenerator,
Yoneda00_View_Generating0 R G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_F_(I)) Yoneda10_ff_i}).
Definition Yoneda10_morphismReIndexer_morphismIndexer :=
forall (I : obIndexer),
forall (R : obReIndexer) (ri : 'Indexer( ReIndexing0 R |- I )),
forall (S : obReIndexer) (sr : 'ReIndexer( S |- R )),
forall (J : obIndexer) (ij : 'Indexer( I |- J )),
forall (G : obGenerator),
( sval (Yoneda10_ff_ ((ReIndexing1 sr o>Indexer ri) o>Indexer ij)) G )
=1 (sval (Yoneda01_F_Poly ij) G \o
(sval (Yoneda10_ff_ ri) G \o
sval (Yoneda10_View_Generating1 sr) G)).
(**Definition Yoneda10_morphismReIndexer_morphismIndexer :=
forall (I : obIndexer),
forall (R : obReIndexer) (ri : 'Indexer( ReIndexing0 R |- I )),
forall (S : obReIndexer) (sr : 'ReIndexer( S |- R )),
forall (J : obIndexer) (ij : 'Indexer( I |- J )),
forall (G : obGenerator),
( sval (Yoneda10_ff_ ((ReIndexing1 sr o>Indexer ri) o>Indexer ij)) G )
=1 (sval (Yoneda01_F_Poly ij) G \o
(sval (Yoneda10_ff_ ri) G \o
sval (Yoneda10_PolyElement (Yoneda01_View (Generating0 R)) (Generating1 sr)) G)). **)
Definition Yoneda10_morphismIndexerOnly
:= ( forall (I : obIndexer),
forall (R : obReIndexer) (ri : 'Indexer( ReIndexing0 R |- I )),
forall (J : obIndexer) (ij : 'Indexer( I |- J )),
forall (G : obGenerator),
( sval (Yoneda10_ff_ (ri o>Indexer ij)) G )
=1 ( sval (Yoneda01_F_Poly ij) G \o
(sval (Yoneda10_ff_ ri) G) )) .
Lemma Yoneda10_morphismReIndexer_morphismIndexer_to_Yoneda10_morphismIndexerOnly :
Yoneda10_morphismReIndexer_morphismIndexer
-> Yoneda10_morphismIndexerOnly .
Proof.
intros H. move. intros. move. intros x.
move => /(_ I R ri _ (unitReIndexer) J ij G) in H.
rewrite -ReIndexing_unitReIndexer in H.
rewrite -polyIndexer_unitIndexer in H.
rewrite /= -Generating_unitReIndexer in H.
move => /(_ x) in H. rewrite /= -unitGenerator_polyGenerator in H.
exact: H.
Qed.
Definition Yoneda10_naturalIndexer
(Yoneda00_E_ : obIndexer -> _)
(Yoneda01_E_ : forall I : obIndexer, _)
(Yoneda01_E_Poly : forall I J : obIndexer, 'Indexer( I |- J ) ->
{Yoneda01_E_Poly_i : forall G : obGenerator, Yoneda00_E_ I G -> Yoneda00_E_ J G |
Yoneda10_natural (Yoneda01_E_ I) (Yoneda01_E_ J) Yoneda01_E_Poly_i})
(Yoneda10_ee_ : forall I : obIndexer, {Yoneda10_ee_I : forall G : obGenerator,
Yoneda00_F_(I) G -> Yoneda00_E_(I) G |
Yoneda10_natural (Yoneda01_F_(I)) (Yoneda01_E_(I)) Yoneda10_ee_I})
:= forall (I J : obIndexer) (ij : 'Indexer( I |- J )),
forall (G : obGenerator),
( sval (Yoneda10_ee_ J) G \o
sval (Yoneda01_F_Poly ij) G )
=1 ( sval (Yoneda01_E_Poly _ _ ij) G \o
(sval (Yoneda10_ee_ I) G )) .
End Section1.
Lemma Yoneda10_Reflector_naturalIndexer_ALT :
forall (Yoneda00_F_ : obIndexer -> _)
(Yoneda01_F_ : forall I : obIndexer, _)
(Yoneda01_F_Poly : forall I J : obIndexer, 'Indexer( I |- J ) ->
{Yoneda01_F_Poly_i : forall G : obGenerator, Yoneda00_F_ I G -> Yoneda00_F_ J G |
Yoneda10_natural (Yoneda01_F_ I) (Yoneda01_F_ J) Yoneda01_F_Poly_i})
(Yoneda10_ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{Yoneda10_ff_i : forall G : obGenerator,
Yoneda00_View_Generating0 R G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_F_(I)) Yoneda10_ff_i}),
forall (Yoneda10_ff_morphismReIndexer_morphismIndexer :
Yoneda10_morphismReIndexer_morphismIndexer Yoneda01_F_Poly Yoneda10_ff_),
Yoneda10_naturalIndexer Yoneda01_Generated_PolyIndexer Yoneda01_F_Poly
(Yoneda10_Reflector Yoneda10_ff_).
Proof.
intros. rewrite /Yoneda10_naturalIndexer.
intros; move. intros i.
apply: (Yoneda10_morphismReIndexer_morphismIndexer_to_Yoneda10_morphismIndexerOnly
Yoneda10_ff_morphismReIndexer_morphismIndexer).
Qed.
End Senses_morCoMod.
(** # #
#+END_SRC
** Grammar of the morphisms , which carry the sense-decodings
ERRATA : the (modified) colimits half is erased here and will be presented only later after cartierSolution8.v ... « generated modified colimits » ( « modos » ) .
As common , the [PolyElement] constructor inputs some element of any functor and changes its format and outputs some generator-morphisms-(functorial-)action ( "Yoneda" ) . Also the [PolyTransf] constructor inputs some (sense) transformation of elements across two metafunctors and changes its format and outputs some (grammatical) transformation of generator-morphisms-(functorial-)actions ( "Yoneda" ) . Memo that both cut-constructors [PolyCoMod] and [PolyTransf] shall be erased/eliminated .
As common , the [CoUnitGenerated] constructor is the counit ( section/injection ) obtained from seeing the generated-functor functor as left adjoint of the precomposition-by-the-reindexing-functor functor . But there are 3 contrasts : (1) this counit ( which commonly-is some family-over-the-reindexer of morphisms ) is polyarrowing in the indexer along the reindexing-functor ; (2) this constructor is presented in the polymorphic formulation , and therefore accumulates some pre-composed morphism-argument ; (3) this constructor is grammatically-distinguished from the [PolyElement] constructor , instead of being defined via the [PolyElement] constructor .
As common , the [Reflector] constructor expresses the universality/limitativeness ( "universality-morphism" , copairing ) of the above adjunction . In contrast , this universality/limitativeness is relaxed (less-requirements) for multiple diagrams simultaneously , instead of the multiple universalities/limitativenesses of each diagram ( "pointwise" ) . Indeed , in this ongoing COQ program , the input object [(I : obIndexer)] is always innerly-quantified ( inner/local argument instead of outer/global parameter ) .
Moreover in contrast , to express the grammatical conversion-relation [Reflector_morphism] that the [Reflector] constructor is polymorphic , it is necessary to grammatically-distinguish those singleton morphisms which in-reality came from some indexing/family of many morphisms ; for example , the input-morphism of this polymorphism conversion-relation is such morphism which shall be grammatically distinguished , also the output-morphism of the reflector-constructor at some index is such morphism which shall be grammatically distinguished . Now this grammatically-distinguishing is done by using two mutually-inductive datatypes ; more-precisely the datatype for indexed/family morphisms [morCoMod_indexed] is nested ( non-recursively , for grammatically-remembering-only ... ) within the datatype for singleton morphisms [morCoMod] .
#+BEGIN_SRC coq :exports both :results silent # # **)
Reserved Notation "''CoMod' ( E ~> F @ Yoneda10 )"
(at level 0, format "''CoMod' ( E ~> F @ Yoneda10 )").
Reserved Notation "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )"
(at level 0, format "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )").
Inductive morCoMod : forall Yoneda00_E Yoneda01_E,
@obCoMod Yoneda00_E Yoneda01_E ->
forall Yoneda00_F Yoneda01_F,
@obCoMod Yoneda00_F Yoneda01_F ->
{ Yoneda10 : ( forall G : obGenerator, Yoneda00_E G -> Yoneda00_F G ) |
Yoneda10_natural Yoneda01_E Yoneda01_F Yoneda10 } -> Type :=
(** ----outer-structural (solution) morphisms---- **)
| AtIndexMor : forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly),
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly),
forall (Yoneda10_ff_ : forall I : obIndexer, _ ),
'CoMod_( E_ ~> F_ @ Yoneda10_ff_ ) ->
forall (I : obIndexer), 'CoMod( AtIndexOb E_(I) ~> AtIndexOb F_(I) @ Yoneda10_ff_(I) )
(** -----cuts to be eliminated----- **)
| 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( F' ~> F @ Yoneda10_ff' ) ->
forall Yoneda00_F'' Yoneda01_F'' (F'' : @obCoMod Yoneda00_F'' Yoneda01_F''),
forall Yoneda10_ff_ , 'CoMod( F'' ~> F' @ Yoneda10_ff_ ) ->
'CoMod( F'' ~> F @ Yoneda10_PolyCoMod Yoneda10_ff_ Yoneda10_ff' )
(** ----solution morphisms---- **)
| UnitCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
'CoMod( F ~> F @ Yoneda10_UnitCoMod Yoneda01_F )
| View_Generating1 : forall (R R' : obReIndexer) (r : 'ReIndexer( R' |- R )),
'CoMod( View_Generating0 R' ~> View_Generating0 R @ Yoneda10_View_Generating1 r )
| CoUnitGenerated : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
'CoMod( View_Generating0 R ~> AtIndexOb Generated(I) @ Yoneda10_CoUnitGenerated i )
where "''CoMod' ( F' ~> F @ Yoneda10 )" :=
(@morCoMod _ _ F' _ _ F Yoneda10) : poly_scope
with morCoMod_indexed (**memo: non-recursive **)
: forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly,
@obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly ->
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly,
@obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly ->
(forall I : obIndexer, { Yoneda10 : forall G : obGenerator,
Yoneda00_E_(I) G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_E_(I)) (Yoneda01_F_(I)) Yoneda10 }) -> Type :=
(** ----outer-structural (solution) morphisms---- **)
| MorCoMod_indexed :
forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly),
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly),
forall (Yoneda10_ff_ : forall I : obIndexer, _ ),
(forall (I : obIndexer),
'CoMod( AtIndexOb E_(I) ~> AtIndexOb F_(I) @ Yoneda10_ff_(I) )) ->
'CoMod_( E_ ~> F_ @ Yoneda10_ff_ )
(** ----solution morphisms---- **)
| Reflector :
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
(Yoneda10_ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{Yoneda10_ff_i : forall G : obGenerator,
Yoneda00_View_Generating0 R G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_F_(I)) Yoneda10_ff_i})
(ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
'CoMod( View_Generating0 R ~> AtIndexOb F_(I) @ (Yoneda10_ff_(I)(R)(i)) ))
(**memo: Yoneda01_F_Poly_functorIndexer and Yoneda10_ff_morphismReIndexerOnly not used in to show convCoMod_sense **)
(Yoneda01_F_Poly_functorIndexer : Yoneda10_functorIndexer Yoneda01_F_Poly)
(Yoneda10_ff_morphismReIndexer_morphismIndexer :
Yoneda10_morphismReIndexer_morphismIndexer Yoneda01_F_Poly Yoneda10_ff_),
'CoMod_( Generated ~> F_ @ Yoneda10_Reflector Yoneda10_ff_ )
where "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )"
:= (@morCoMod_indexed _ _ _ E_ _ _ _ F_ Yoneda10_) : poly_scope .
Notation "''CoMod' ( F' ~> F )" := (@morCoMod _ _ F' _ _ F _)
(at level 0, only parsing, format "''CoMod' ( F' ~> F )") : poly_scope.
Notation "''CoMod_' ( E_ ~> F_ )" := (@morCoMod_indexed _ _ _ E_ _ _ _ F_ _)
(at level 0, format "''CoMod_' ( E_ ~> F_ )") : poly_scope.
Notation "''AtIndexMor' ff_ I" := (@AtIndexMor _ _ _ _ _ _ _ _ _ ff_ I)
(at level 10, ff_ at next level, I at next level) : 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 "''View_Generating1' r" := (@View_Generating1 _ _ r)
(at level 10, r at next level) : poly_scope.
Notation "'CoUnitGenerated @ i" := (@CoUnitGenerated _ _ i)
(at level 10, i at next level) : poly_scope.
Notation "''MorCoMod_indexed' ff_" := (@MorCoMod_indexed _ _ _ _ _ _ _ _ _ ff_)
(at level 10, ff_ at next level) : poly_scope.
Notation "[[ ff_ @ Yoneda01_F_Poly_functorIndexer , Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_" :=
(@Reflector _ _ _ _ _ ff_ Yoneda01_F_Poly_functorIndexer
Yoneda10_ff_morphismReIndexer_morphismIndexer)
(at level 4, Yoneda01_F_Poly_functorIndexer at next level,
Yoneda10_ff_morphismReIndexer_morphismIndexer at next level,
format "[[ ff_ @ Yoneda01_F_Poly_functorIndexer , Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_" ) : poly_scope.
Notation "[[ ff_ ]]_" := (@Reflector _ _ _ _ _ ff_ _ _ )
(at level 4, format "[[ ff_ ]]_" ) : poly_scope.
Scheme morCoMod_morCoMod_indexed_ind := Induction for morCoMod Sort Prop
with morCoMod_indexed_morCoMod_ind := Induction for morCoMod_indexed Sort Prop.
Combined Scheme morCoMod_morCoMod_indexed_mutind from
morCoMod_morCoMod_indexed_ind, morCoMod_indexed_morCoMod_ind.
Scheme morCoMod_morCoMod_indexed_rect := Induction for morCoMod Sort Type
with morCoMod_indexed_morCoMod_rect := Induction for morCoMod_indexed Sort Type.
Definition morCoMod_morCoMod_indexed_mutrect P P0 a b c d e f g :=
pair (@morCoMod_morCoMod_indexed_rect P P0 a b c d e f g)
(@morCoMod_indexed_morCoMod_rect P P0 a b c d e f g).
(** # #
#+END_SRC
* Solution morphisms
As common, the purely-grammatical polymorphism cut-constructor [PolyCoMod] is not part of the solution terminology .
In contrast, there is one additional cut-constructor [PolyTransf] which inputs some (sense) transformation of elements across two metafunctors and changes its format and outputs some (grammatical) transformation of generator-morphisms-(functorial-)actions ( "Yoneda" ) . Memo that both cut-constructors [PolyCoMod] and [PolyTransf] shall be erased/eliminated .
** Solution morphisms without polymorphism
#+BEGIN_SRC coq :exports both :results silent # # **)
Module Sol.
Section Section1.
Delimit Scope sol_scope with sol.
Inductive morCoMod : forall Yoneda00_E Yoneda01_E,
@obCoMod Yoneda00_E Yoneda01_E ->
forall Yoneda00_F Yoneda01_F,
@obCoMod Yoneda00_F Yoneda01_F ->
{ Yoneda10 : ( forall G : obGenerator, Yoneda00_E G -> Yoneda00_F G ) |
Yoneda10_natural Yoneda01_E Yoneda01_F Yoneda10 } -> Type :=
| AtIndexMor : forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly),
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly),
forall (Yoneda10_ff_ : forall I : obIndexer, _),
'CoMod_( E_ ~> F_ @ Yoneda10_ff_ ) -> forall (I : obIndexer),
'CoMod( AtIndexOb E_(I) ~> AtIndexOb F_(I) @ (Yoneda10_ff_(I)) )
| UnitCoMod : forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
'CoMod( F ~> F @ Yoneda10_UnitCoMod Yoneda01_F )
| View_Generating1 : forall (R R' : obReIndexer) (r : 'ReIndexer( R' |- R )),
'CoMod( View_Generating0 R' ~> View_Generating0 R @ Yoneda10_View_Generating1 r )
| CoUnitGenerated : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
'CoMod( View_Generating0 R ~> AtIndexOb Generated(I) @ Yoneda10_CoUnitGenerated i )
where "''CoMod' ( F' ~> F @ Yoneda10 )" :=
(@morCoMod _ _ F' _ _ F Yoneda10) : sol_scope
with morCoMod_indexed
: forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly,
@obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly ->
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly,
@obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly ->
(forall I : obIndexer, { Yoneda10 : forall G : obGenerator,
Yoneda00_E_(I) G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_E_(I)) (Yoneda01_F_(I)) Yoneda10 }) -> Type :=
| MorCoMod_indexed :
forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly),
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly),
forall (Yoneda10_ff_ : forall I : obIndexer, _ ),
(forall (I : obIndexer),
'CoMod( AtIndexOb E_(I) ~> AtIndexOb F_(I) @ (Yoneda10_ff_(I)) ) ) ->
'CoMod_( E_ ~> F_ @ Yoneda10_ff_ )
| Reflector :
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
(Yoneda10_ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
{Yoneda10_ff_i : forall G : obGenerator,
Yoneda00_View_Generating0 R G -> Yoneda00_F_(I) G |
Yoneda10_natural (Yoneda01_View_Generating0 R) (Yoneda01_F_(I)) Yoneda10_ff_i})
(ff_ : forall (I : obIndexer),
forall (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
'CoMod( View_Generating0 R ~> AtIndexOb F_(I) @ (Yoneda10_ff_ _ _ (i)) ))
(Yoneda01_F_Poly_functorIndexer : Yoneda10_functorIndexer Yoneda01_F_Poly)
(Yoneda10_ff_morphismReIndexer_morphismIndexer :
Yoneda10_morphismReIndexer_morphismIndexer Yoneda01_F_Poly Yoneda10_ff_),
'CoMod_( Generated ~> F_ @ Yoneda10_Reflector Yoneda10_ff_ )
where "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )" :=
(@morCoMod_indexed _ _ _ E_ _ _ _ F_ Yoneda10_) : sol_scope .
End Section1.
Module Export Ex_Notations.
Delimit Scope sol_scope with sol.
Notation "''CoMod' ( F' ~> F @ Yoneda10 )" := (@morCoMod _ _ F' _ _ F Yoneda10)
(at level 0, format "''CoMod' ( F' ~> F @ Yoneda10 )") : sol_scope.
Notation "''CoMod' ( F' ~> F )" := (@morCoMod _ _ F' _ _ F _)
(at level 0, only parsing, format "''CoMod' ( F' ~> F )") : sol_scope.
Notation "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )" :=
(@morCoMod_indexed _ _ _ E_ _ _ _ F_ Yoneda10_)
(at level 0, format "''CoMod_' ( E_ ~> F_ @ Yoneda10_ )") : sol_scope.
Notation "''CoMod_' ( E_ ~> F_ )" := (@morCoMod_indexed _ _ _ E_ _ _ _ F_ _)
(at level 0, format "''CoMod_' ( E_ ~> F_ )") : sol_scope.
Notation "''AtIndexMor' ff_ I" := (@AtIndexMor _ _ _ _ _ _ _ _ _ ff_ I)
(at level 10, ff_ at next level, I at next level) : sol_scope.
Notation "@ ''UnitCoMod' F" := (@UnitCoMod _ _ F)
(at level 10, only parsing) : sol_scope.
Notation "''UnitCoMod'" := (@UnitCoMod _ _ _) (at level 0) : sol_scope.
Notation "''View_Generating1' r" := (@View_Generating1 _ _ r)
(at level 10, r at next level) : sol_scope.
Notation "'CoUnitGenerated @ i" := (@CoUnitGenerated _ _ i)
(at level 10, i at next level) : sol_scope.
Notation "''MorCoMod_indexed' ff_" := (@MorCoMod_indexed _ _ _ _ _ _ _ _ _ ff_)
(at level 10, ff_ at next level) : sol_scope.
Notation "[[ ff_ @ Yoneda01_F_Poly_functorIndexer , Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_" :=
(@Reflector _ _ _ _ _ ff_ Yoneda01_F_Poly_functorIndexer
Yoneda10_ff_morphismReIndexer_morphismIndexer)
(at level 4, Yoneda01_F_Poly_functorIndexer at next level,
Yoneda10_ff_morphismReIndexer_morphismIndexer at next level,
format "[[ ff_ @ Yoneda01_F_Poly_functorIndexer , Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_" ) : sol_scope.
Notation "[[ ff_ ]]_" := (@Reflector _ _ _ _ _ ff_ _ _ )
(at level 4, format "[[ ff_ ]]_" ) : sol_scope.
End Ex_Notations.
Scheme morCoMod_morCoMod_indexed_ind := Induction for morCoMod Sort Prop
with morCoMod_indexed_morCoMod_ind := Induction for morCoMod_indexed Sort Prop.
Combined Scheme morCoMod_morCoMod_indexed_mutind from
morCoMod_morCoMod_indexed_ind, morCoMod_indexed_morCoMod_ind.
Scheme morCoMod_morCoMod_indexed_rect := Induction for morCoMod Sort Type
with morCoMod_indexed_morCoMod_rect := Induction for morCoMod_indexed Sort Type.
Definition morCoMod_morCoMod_indexed_mutrect P P0 a b c d e f :=
pair (@morCoMod_morCoMod_indexed_rect P P0 a b c d e f)
(@morCoMod_indexed_morCoMod_rect P P0 a b c d e f).
Definition toPolyMor_mut :
(forall Yoneda00_E Yoneda01_E (E : @obCoMod Yoneda00_E Yoneda01_E)
Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
Yoneda10_ff (ff : 'CoMod( E ~> F @ Yoneda10_ff ) %sol ),
'CoMod( E ~> F @ Yoneda10_ff ) %poly ) *
( forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly)
Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
Yoneda10_ff_ (ff_ : 'CoMod_( E_ ~> F_ @ Yoneda10_ff_ ) %sol ),
'CoMod_( E_ ~> F_ @ Yoneda10_ff_ ) %poly ) .
Proof.
apply morCoMod_morCoMod_indexed_mutrect.
- (* AtIndexMor *) intros ? ? ? ? ? ? ? ? ? ff_ IHff_ I .
exact: ('AtIndexMor IHff_ I)%poly.
- (* UnitCoMod *) intros ? ? F .
exact: ( @'UnitCoMod F ) %poly.
- (* View_Generating1 *) intros ? ? r.
exact: ( 'View_Generating1 r)%poly.
- (* CoUnitGenerated *) intros ? ? i.
exact: ( 'CoUnitGenerated @ i )%poly.
- (* MorCoMod_indexed *) intros ? ? ? ? ? ? ? ? ? ff_ IHff_ .
exact: ( 'MorCoMod_indexed (fun I : obIndexer => IHff_(I)) )%poly.
- (* Reflector *) intros ? ? ? F_ ? ff_ IHff_ Yoneda01_F_Poly_functorIndexer
Yoneda10_ff_morphismReIndexer_morphismIndexer.
exact: ( [[ ( fun (I : obIndexer)
(R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )) =>
(IHff_ I R i) ) @ Yoneda01_F_Poly_functorIndexer ,
Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_ )%poly.
Defined.
Definition toPolyMor := fst toPolyMor_mut.
Definition toPolyMor_indexed := snd toPolyMor_mut.
Arguments toPolyMor : simpl nomatch.
Arguments toPolyMor_indexed : simpl nomatch.
Lemma toPolyMor_mut_AtIndexMor :
forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly)
Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
Yoneda10_ff_ (ff_ : 'CoMod_( E_ ~> F_ @ Yoneda10_ff_ )%sol),
forall I : obIndexer,
toPolyMor (AtIndexMor ff_ I) = ('AtIndexMor (toPolyMor_indexed ff_) I)%poly.
Proof. reflexivity. Qed.
Lemma toPolyMor_mut_UnitCoMod :
forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F),
toPolyMor (@'UnitCoMod F)%sol = (@'UnitCoMod F)%poly.
Proof. reflexivity. Qed.
Lemma toPolyMor_mut_View_Generating1 :
forall (R R' : obReIndexer) (r : 'ReIndexer( R' |- R )),
toPolyMor ('View_Generating1 @ r)%sol = ('View_Generating1 @ r)%poly.
Proof. reflexivity. Qed.
Lemma toPolyMor_mut_CoUnitGenerated :
forall (I : obIndexer) (R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
toPolyMor ('CoUnitGenerated @ i)%sol = ('CoUnitGenerated @ i)%poly.
Proof. reflexivity. Qed.
Lemma toPolyMor_mut_MorCoMod_indexed :
forall Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly
(E_ : @obCoMod_indexed Yoneda00_E_ Yoneda01_E_ Yoneda01_E_Poly)
Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
Yoneda10_ff_ (ff_: (forall I : obIndexer,
'CoMod( AtIndexOb E_ I ~> AtIndexOb F_ I @ Yoneda10_ff_ I )%sol)),
toPolyMor_indexed ('MorCoMod_indexed ff_ )%sol
= ( 'MorCoMod_indexed (fun I : obIndexer => toPolyMor (ff_(I))) )%poly.
Proof. reflexivity. Qed.
Lemma toPolyMor_mut_Reflector :
forall Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly
(F_ : @obCoMod_indexed Yoneda00_F_ Yoneda01_F_ Yoneda01_F_Poly)
Yoneda10_ff_ (ff_ : (forall (I : obIndexer)
(R : obReIndexer) (i : 'Indexer( ReIndexing0 R |- I )),
'CoMod( View_Generating0 R ~> AtIndexOb F_ I @ Yoneda10_ff_ I R i )%sol))
(Yoneda01_F_Poly_functorIndexer : Yoneda10_functorIndexer Yoneda01_F_Poly)
(Yoneda10_ff_morphismReIndexer_morphismIndexer :
Yoneda10_morphismReIndexer_morphismIndexer Yoneda01_F_Poly Yoneda10_ff_),
toPolyMor_indexed ([[ ff_ @ Yoneda01_F_Poly_functorIndexer ,
Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_ )%sol
= ( [[ ( fun (I : obIndexer) (R : obReIndexer)
(i : 'Indexer( ReIndexing0 R |- I )) => toPolyMor (ff_(I)(R)(i)) )
@ Yoneda01_F_Poly_functorIndexer ,
Yoneda10_ff_morphismReIndexer_morphismIndexer ]]_ )%poly.
Proof. reflexivity. Qed.
Definition toPolyMor_mut_rewrite :=
(toPolyMor_mut_AtIndexMor, toPolyMor_mut_UnitCoMod, toPolyMor_mut_View_Generating1,
toPolyMor_mut_CoUnitGenerated, toPolyMor_mut_MorCoMod_indexed,
toPolyMor_mut_Reflector).
(** # #
#+END_SRC
** Destruction of morphisms with inner-instantiation of object-indexes
As common , the polymorphism/cut-elimination resolution will require the destruction of some morphism which is constrained by the structure of its domain/codomain objects . In contrast , during the above destruction , oneself wants some additional data to be instantiated/shared , beyond the domain/codomain objects : ( the sense-decoding [Yoneda01_Generated_PolyIndexer] of ) the indexer-arrow (functorial-)actions across the indexed/family objects .
Regardless the (nested) mutually-inductive presentation of the datatypes and regardless the extra-indexes in the datatype-families , oneself easily still-gets the common dependent-destruction of morphisms with inner-instantiation of object-indexes .
Moreover some contrast is during the polymorphism/cut-elimination resolution . In the earlier COQ programs for limits , it was better to start by general-destructing the prefix-argument [f_] of the composition [(f_ o>CoMod f')] and then to constrained-destruct the postfix-parameter [f'] such to use the general-polymorphism of the projection (unit of adjunction) and the instantiated-polymorphism of the pairing ; the alternative would use the instantiated-polymorphism of the projection and general-polymorphism of the pairing . In this ongoing COQ program for colimits , it is better to start by general-destructing the postfix-parameter [f'] of the composition [(f_ o>CoMod f')] and then to constrained-destruct the prefix-argument [f_] such to use the general-polymorphism of the counit ( section/injection ) and the instantiated-polymorphism of the reflector ( copairing ) ; the alternative would be the same but with more case-analyses .
#+BEGIN_SRC coq :exports both :results silent # # **)
Module Destruct_codomViewGenerating.
Inductive morCoMod_codomViewGenerating
: forall Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F ),
forall (R : obReIndexer), forall Yoneda10_ff,
'CoMod( F ~> (View_Generating0 R) @ Yoneda10_ff ) %sol -> Type :=
| UnitCoMod : forall R : obReIndexer,
morCoMod_codomViewGenerating ( ( @'UnitCoMod (View_Generating0 R) )%sol )
| View_Generating1 : forall (R R' : obReIndexer) (r : 'ReIndexer( R' |- R )),
morCoMod_codomViewGenerating ( ( 'View_Generating1 r ) %sol ).
Lemma morCoMod_codomViewGeneratingP
: 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( F ~> G @ Yoneda10_gg ) %sol ),
ltac:( destruct G; [ refine (unit : Type) | ];
refine (morCoMod_codomViewGenerating gg) ).
Proof.
intros. case: _ _ F _ _ G Yoneda10_gg / gg.
- intros; exact: tt.
- destruct F; [intros; exact: tt | ].
constructor 1.
- constructor 2.