-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcartierSolution9.v
5721 lines (5100 loc) · 408 KB
/
cartierSolution9.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: cartierSolution9.v
Proph
https://gitlab.com/1337777/cartier/blob/master/cartierSolution9.v
solves half of some question of CARTIER which is how to program « parametrization modos » ( "parametrized form" , "dependent type" , "fibration with internal products" ) ...
ERRATA :: this also solves cartierSolution8.v where the continuity-property was "confused" .
SHORT ::
(1.) The ends is « QOC » : to program the « form-morphisms » parametrized-over the « parametrizator-arrows » ( "fibration" ) , which are generated by some « generating » parametrization-functor , such that this programming enables the computational-logical introductions-eliminations constructors and the cut/pullback-elimination/admissibility lemmas when in the presence of the grammatical « product/pi-objects » or the grammatical « substitution-objects » or the grammatical « colimit/sum/sigma/viewingfunctor-objects » ; and to do this programming coherently/continuously for the viewing-data/topology sense-decodings .
(2.) Commonly , the "lambda calculus" has the « cancellation » computation [ ( ( application s ) <o ( abstraction f ) ) := substitution ( f , s ) ] , where [ f ] is some function and [ s ] is some element ; but now in contrast the input function [ f ] (transformation function from representable/generator functor into the product-object/functor) shall be viewed as parametrized-over the given/fixed context-projection function (which defines the product-object) whose input section [ s ] is some now-function which parametrizes its corresponding application function [ application s ] and also parametrizes the output function [ substitution ( f , s ) ] of the substitution operation .
(3.) In other words , given any grammatical form-morphism [ f ] of [ |- ( E ~> F ) ] parametrized-over the parametrizator-arrow ( "span" ) [ project <o> subst ] , whose sensible-decoding is some « formatted » function [ project* E |- subst* F ] across the « formats » ( "pullbacks" ) from [ project* E ] to [ subst* F ] parametrized-over the (elements of the) parametrizator-object (metafunctor over the generator-morphology not the generating-parametrizator-morphology) [ P ] , oneself shall :
(3.1.) introduce some grammatical product/pi-object ( really « pi-substitution » ) with « inner-parametrizing/pairing/tupling/abstraction/remembering » ( reparametrized ) morphism [ |- ( E ~> PI_project SUBST_subst F ) ] which is polymorph-laxly-cancelled by the ( « selection/application/forgetting » ) morphism [ |- ( PI_project SUBST_subst F ~> F ) ] corresponding to some section arrow [ section ] of the [ project ] arrow ,
(3.2.) or introduce some grammatical substitution-object with « remembering » morphism [ |- ( E ~> SUBST_subst F ) ] which is polymorph-(tightly-)cancelled by the « forgetting » morphism [ |- ( SUBST_subst F ~> F ) ] of the substitution-object , for the instances when the [ project ] arrow is identity ,
(3.3.) and do such coherently/continuously for the viewing-data/topology sense-decodings which are internalized ( when finite-compact or finite-dimensional or finite-generated ) via the elimination of the (parametrized-and-modified) grammatical colimiting/sum/sigma/viewingfunctor-objects ( parametrized-and-modified rephrasing of « each functor is the sum/colimit of its elements » ) : [ X ; (p : P X) ; (e : E X (project p)) |- F X (subst p) ] ,
(3.4.) where the grammar definition/lemma and the cut/pullback-elimination/admissibility lemma/definition ( and the decidability of unification/convertibility , and the commutation of format/substitution along pi-substitution , and the analogue between "localization of fibration" and « programming locally after non-empty global contexts » , and the intended "cartesian" properties , and the non-necessity of "discrete-fibration" properties , and the limit-exactness/preservation of the viewed-functor construction which is used to add/express such things as « viewed-substitution » or « viewed-pi-substitution » ) are interdependently-discovered by many refinements after many attempts .
(4.) Another angle of view :
#+BEGIN_EXAMPLE
E ---------------------- f ----------------------> F
| |
. PI_project SUBST_subst F ---- application _ ---> .
| | |
. . .
| | |
. . .
| v |
v ------- section -------> v
E_ <----- project ------- P ------- subst -------> F_
#+END_EXAMPLE
(5.) Memo that this polymorph presentation of the pi-substitution objects has pre-substitution by any accumulator parametrizator-morphism built-in grammatically , therefore this infers the commutation of format/substitution along pi-substitution : [ t* PI_p SUBST_s (grammatically via parametrizator-object) <-> PI_p SUBST_(t o> s) (grammatically via form-object) ] .
(6.) Memo that any parametrizator-morphism ( "span" ) [ l <o> r ] may be viewed as some function [ r ] whose domain has been reindexed by the function [ l ] , and the composition of two parametrizator-morphisms ( "spans" ) is similar as some « polymorph pullback » ; therefore the grammatical cut-elimination/admissibility for such parametrizator-morphisms is in fact similar as some « polymorph-pullback-elimination/admissibility » which says that the pullback process among parametrizator-morphisms shall be structured/grammatical and not-merely exist in the sense .
(7.) Moreover memo that the form-morphisms parametrized-over the parametrizator-morphisms are defined « mutually inductively » with the parametrizator-morphisms , which says that , in adddition of doing « selection/application/forgetting » ( "lifting-as-identity" ) from any parametrizator-morphism upto the selection/application/forgetting-morphism of the pi/substitution-object , moreover oneself may do « formatting » ( "context extension" by any form-morphism , beyond the common "context extension" by own lifting ) from any form-morphism downto some parametrizator-morphism .
Regardless , any generating parametrization-functor which is « sense-discrete » ( "discrete-fibration" with only selection/application/forgetting-morphisms , which are really "lifting-as-identity" ) would be simpler because then only « nested-mutual induction » is required by the absence ( non-necessity ) of this formatting constructor ( "context extension" by any form-morphism ) .
Regardless , any generating parametrization-functor which is (constructively) « full functor » would be simpler because then any element of some parametrizator-object (element of metafunctor over the generator-morphology not the generating-parametrizator-morphology) has some fixed-chosen extension as polyelement (metatransformation) .
(8.) In summary , the final expressivity shall allow these two things ( II.8.5.5 ) : (1) mutual induction of form-morphisms with parametrizator-morphisms via the presence of the « formatting » constructor , (2) programming locally after « non-empty global contexts » . For (1) , therefore some grammatical pullback-elimination/admissibility for the form-morphisms shall also be necessary , in particular the "fibre-completeness" of the generating parametrization-functor shall be necessary . For (2) , the mathematician counter-part of this engineer-programmer "feature" is named « localization of fibration at some object of the base » . Regardless , everything can always be compiled back to the empty global context ( II.8.5.9 ) ...
(9.) Memo that this presentation of the pi/substitution-objects is « cartesian » only when the domain of the inner-parametrizing/pairing/tupling/abstraction/remembering-morphism is some generator (representable-functor) . This ( intended , as in the lambda calculus ) limitation can be erased in the case when the generating parametrization-functor is « sense-discrete » , where the parametrizator-morphisms are nested within the form-morphisms and are therefore priorly decidable .
(10.) Finally , memo that the grammatical colimiting/sum/sigma/viewing-functor-objects assume some finiteness properties ( such as finite-compactness or finite-dimensionality or finite-generated ) onto the viewing-data/topology sense-decodings which they internalize . And these viewing-functor-objects are similar as generators ( representable-functors ) but to be used for functors which are already viewed-functors ( "sheaf" ) . Therefore , and knowning that the viewed-functor construction is exact and commutes with limits , oneself may add/express such things as « viewed-substitution » or « viewed-pi-substitution » , as long as the codomain is already some viewed-functor and the domain for the « cartesian » property is now some viewing-functor .
Regardless , eventually the product/pi-objects shall assume similar finiteness properties , in the style of the « compacted-point » technique ( "compact-open topology for the compactly-continuous mappings , which gives compactly-uniform convergence" ( II.7.4.10 ) ... « compacted-parameters compacted-arguments viewing-data for the compacted-viewing-continuous morphisms » ? ) .
(11.) For instant first impression , the conversion/computation-relation constructor which says that the « forgetting » morphism of the substitution-object polymorph-cancels the « remembering » morphism corresponding to any form-morphism , is written as :
#+BEGIN_EXAMPLE
| Remember_Forget : forall Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F
Yoneda01_Param_F Yoneda10_FormParam_F (F : obCoMod Yoneda10_FormParam_F)
(Param_F : obCoMod_Param Yoneda01_Param_F) Yoneda00_Param_SubstF
Yoneda01_Param_SubstF (Param_SubstF : obCoMod_Param Yoneda01_Param_SubstF)
Yoneda10_Param_Forget (param_Forget :
'CoMod_( Param_SubstF ~> Param_F @_ Yoneda10_Param_Forget ))
(L : obGenerator) Yoneda10_Param_ll Yoneda10_Form_ll
(ll : 'CoMod( View L ~> F @_ Yoneda10_Param_ll @^ Yoneda10_Form_ll ))
Yoneda10_Param_ll_ , (* ... *)
( ll o>CoMod ee )
<~~ ( << ll @_ Heq_param = Yoneda10_Param_ll_ , Heq_subst_0 = param_Forget_0 >>
: 'CoMod ( View L ~> _ @_ _ @^ _ ) )
o>CoMod ( ( 'Forget @_ Heq_subst = param_Forget o>CoMod ee )
: 'CoMod( Subst F Param_F Param_SubstF Yoneda10_Param_Forget' ~> E @_ _ @^ _ ) )
#+END_EXAMPLE
KEYWORDS :: OOO1337777 ; COQ ; QOC ; MODOS
OUTLINE ::
* Generating parametrization-functor metalogic
+ Generating parameters
+ Generating parametrized-forms
* Grammatical presentation of objects
+ Sense-decodings of the objects
+ Finiteness of the viewing-elements of some viewing-functor
+ 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
* 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 morphisms
+ Solution morphisms without polymorphism
+ Destruction of morphisms with inner-instantiation of object-indexes
* Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution
HINT :: do cartierSolution10.v cartierSolution11.v
-----
* Generating parametrization-functor metalogic
** Generating parameters
In contrast , there are two generating morphologies . Firstly , the "base" generating morphology is named « generating parametrizator morphology » ; its objects are named « parametrizator-index » and its morphisms are named « parametrizator-arrow » . This generating morphology will generate the « parametrizator-objects » ( or simply , « parameter » ) and « parametrizator-morphisms » inside the « parametrizator morphology » . Secondly , the "total space" generating morphology is named « generator morphology » and generates the « forms morphology » , and will be presented in the next section .
Moreover in contrast , the sense-decodings ( "Yoneda" ) of the things/codes in both these generated grammar will be (meta-)functors [Yoneda01_functor] or natural transformations [Yoneda10_natural] over the « generator morphology » not the « generating parametrizator morphology » .
#+BEGIN_SRC coq :exports both :results silent # # **)
Require Import ssreflect ssrfun ssrbool.
Require Lia.
Module PARAMETRIZATION.
Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive.
Set Primitive Projections.
Declare Scope poly_scope. Delimit Scope poly_scope with poly. Open Scope poly.
Parameter obParametrizator : Type.
Parameter morParametrizator : obParametrizator -> obParametrizator -> Type.
Parameter polyParametrizator :
forall A A', morParametrizator A' A -> forall A'', morParametrizator A'' A' -> morParametrizator A'' A .
Parameter unitParametrizator : forall {A : obParametrizator}, morParametrizator A A.
Notation "''Parametrizator' ( A' ~> A )" := (@morParametrizator A' A) (at level 0) : poly_scope.
Notation "_@ A'' o>Parametrizator a'" := (@polyParametrizator _ _ a' A'')
(at level 40, A'' , a' at next level, left associativity) : poly_scope.
Notation "a_ o>Parametrizator a'" := (@polyParametrizator _ _ a' _ a_)
(at level 40, a' at next level) : poly_scope.
Axiom polyParametrizator_morphism :
forall (A A' : obParametrizator) (a' : 'Parametrizator( A' ~> A ))
(A'' : obParametrizator) (a_ : 'Parametrizator( A'' ~> A' )),
forall B (b : 'Parametrizator( B ~> A'' )),
b o>Parametrizator ( a_ o>Parametrizator a' ) = ( b o>Parametrizator a_ ) o>Parametrizator a' .
Axiom polyParametrizator_unitParametrizator :
forall (A A' : obParametrizator) (a' : 'Parametrizator( A' ~> A )),
a' = ( (@unitParametrizator A') o>Parametrizator a' ) .
Axiom unitParametrizator_polyParametrizator :
forall (A : obParametrizator), forall (A'' : obParametrizator) (a_ : 'Parametrizator( A'' ~> A )),
a_ = ( a_ o>Parametrizator (@unitParametrizator A) ) .
(** # #
#+END_SRC
** Generating parametrized-forms
Moreover , the "total space" generating morphology is named « generator morphology » ; its objects are named « generator-index » and its morphisms are named « generator-arrow » . This generating-morphology will generate « parametrized-objects » and « parametrized-morphisms » , which together are named « parametrized-forms » , inside the « forms morphology » .
Finally , some "fibration" « generating parametrization functor » from the « generator morphology » to the « generating parametrizator morphology » is presented . This generating parametrization functor is not assumed to be « full functor » . But as shall be discovered later , some assumption of generating parametrization-functor which is « full functor » would be simpler because then any element of some parametrizator-object (element of metafunctor over the generator-morphology not the generating-parametrizator-morphology) has some fixed-chosen extension as polyelement (metatransformation) .
#+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'' , a' at next level, left associativity) : poly_scope.
Notation "a_ o>Generator a'" := (@polyGenerator _ _ a' _ a_)
(at level 40, a' at next level) : 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 Parameter0 : obGenerator -> obParametrizator.
Parameter Parameter1 : forall A A' : obGenerator,
'Generator( A ~> A' ) -> 'Parametrizator( Parameter0 A ~> Parameter0 A') .
Axiom Parameter_morphism :
forall (A A' : obGenerator) (a' : 'Generator( A' ~> A ))
(A'' : obGenerator) (a_ : 'Generator( A'' ~> A' )),
Parameter1 ( a_ o>Generator a' ) = ( Parameter1 a_ ) o>Parametrizator (Parameter1 a').
Axiom Parameter_unitGenerator :
forall (A : obGenerator),
(@unitParametrizator (Parameter0 A)) = ( Parameter1 (@unitGenerator A) ) .
(**TODO: make use of this NOOP head constant [Element_data] everywhere ;
in particular , would be useful to match hypotheses such as
[ param : Element_data Yoneda00_Param_F G ] in tactics such as [tac_param_all] **)
Definition Element_data (Yoneda00 : obGenerator -> Type) (G : obGenerator) : Type
:= (Yoneda00 G).
Definition Yoneda01_action (Yoneda00 : obGenerator -> Type)
(Yoneda01 : forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00 G -> Yoneda00 G')
G G' (g : 'Generator( G' ~> G)) (x : Yoneda00 G)
:= (Yoneda01 G G' g x).
Notation "g o>Generator_ [ Yoneda01 ] x" := (@Yoneda01_action _ Yoneda01 _ _ g x)
(at level 40, x at next level) : poly_scope.
Notation "g o>Generator_ x" := (@Yoneda01_action _ _ _ _ g x)
(at level 40, x at next level) : poly_scope.
Definition Yoneda01_functor (Yoneda00 : obGenerator -> Type)
(Yoneda01 : forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00 G -> Yoneda00 G') : Prop :=
( forall G G' (g : 'Generator( G' ~> G)) G'' (g' : 'Generator( G'' ~> G')) x,
g' o>Generator_[Yoneda01] (g o>Generator_[Yoneda01] x)
= (g' o>Generator g) o>Generator_[Yoneda01] x ) /\
( forall G x, x = (@unitGenerator G) o>Generator_[Yoneda01] x ) .
Definition Yoneda01_data (Yoneda00 : obGenerator -> Type)
:= { Yoneda01 : ( forall G G' : obGenerator, 'Generator( G' ~> G ) -> Yoneda00 G -> Yoneda00 G' ) |
Yoneda01_functor Yoneda01 }.
Definition Yoneda10_natural
Yoneda00_F (Yoneda01_F : Yoneda01_data Yoneda00_F)
Yoneda00_E (Yoneda01_E : Yoneda01_data Yoneda00_E)
(Yoneda10 : forall G : obGenerator, Yoneda00_F G -> Yoneda00_E G) : Prop :=
forall G G' (g : 'Generator( G' ~> G )) (f : Yoneda00_F G),
g o>Generator_[sval Yoneda01_E] (Yoneda10 G f)
= Yoneda10 G' (g o>Generator_[sval Yoneda01_F] f) .
Definition Yoneda10_data
Yoneda00_F (Yoneda01_F : Yoneda01_data Yoneda00_F)
Yoneda00_E (Yoneda01_E : Yoneda01_data Yoneda00_E)
:= { Yoneda10 : ( forall G : obGenerator, Yoneda00_F G -> Yoneda00_E G ) |
Yoneda10_natural Yoneda01_F Yoneda01_E Yoneda10 } .
(** # #
#+END_SRC
* Grammatical presentation of objects
As common , the sense-decoding of any form-object is some metafunctor over the « generator » morphology ( [obGenerator] ) ; the sense-decoding of any form-morphism is some metatransformation over the « generator » morphology . In contrast , the sense-decoding of any parametrizator-object is some metafunctor over the « generator » morphology ( not the parametrizator-morphology /!\ ) ; the sense-decoding of any parametrizator-morphism is some metatransformation over the « generator » morphology ( not the parametrizator morphology /!\ ) .
And 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 .
Memo that these sense-decodings may be held for two ends : (1) to express the logical-properties which are carried-as-arguments by the many morphisms constructors ; (2) to express the dependence of the output limit-object ( pi-substitution-object ) on the parametrizator-morphisms contained in some given input diagram ( here the object [Subst] ) .
Moreover, the form-objects and the parametrizator-objects are presented mutually-inductively . Both the form-morphology and the parametrizator-morphology have their own viewing-data and (modified-)colimiting(-structure) ( [ViewingFunctor_default] , [ViewedFunctor_default] , [ViewedFunctor1_default] , [UnitViewedFunctor_default] , [PolyElement_default] , [PolyTransf_default] , and similarly [ViewingFunctor_Param_default] ... ) , which are interdependent . For now , oneself assumes that this viewing-data is the default-viewing data , and therefore only the critical skeleton of the grammar is shown ...
Moreover , the form-morphology has the substitution-object ( [Subst] ) , which depends on some fixed-given substitution morphism via its "Yoneda" sense-decoding .
And the parametrizator-morphology has the « formatting » constructor ( [Format] , [Formatting] ) , which does « formatting » ( "context extension" by any form-morphism , beyond the common "context extension" by own lifting ) from some form-morphism downto some parametrizator-arrow . This [Format] parametrizator-index (parameter) really is the common "pullback" ; this will become clearer later in the case of « pi-substitution » objects ...
Again , memo that the form-objects and the parametrizator-objects are presented mutually-inductively . This mutual-induction is not nested-mutual-induction because of the presence of the [Format] constructor ; also later oneself shall discover that the grammatical-reduction (oriented conversion) of form-morphisms would not infer the reduction of their carried parametrizator-morphisms codes , but only does infer the same sense-decodings ( which is solution conversion , which is priorly decidable in the case of discrete fibrations ) . Therefore , for non-discrete fibrations , the « sharing » between the inductive-type-families of the form-morphology and the parametrizator-morphology is (should and must) via the "Yoneda" sense-decodings not-via grammatical-codes ; in contrast to the earlier [cartierSolution6.v] for non-contextual ( "1-weighted" ) 2-fold ( "2-higher" ) pairing-projections ( "product" ) , where the "1-level" codes are nested/carried by the "2-level" codes ... Regardless , in some alternative refined presentation , the inductive-type-family for the form-morphisms shall be able to carry the parametrizator-objects codes .
Memo that clearly it can be shown that all the operations can be extended (well-defined) along the quotienting axioms ( for now only [Yoneda00_Form_Subst_quotientLogical] ) .
** Sense-decodings of the objects
#+BEGIN_SRC coq :exports both :results silent # # **)
Module Export Senses_obCoMod.
Notation "''exists' x ..." := (exist _ x _) (at level 10, x at next level) : poly_scope.
Notation "[< data | ... >]" := (exist (fun data : _ => sval _ _ data = _ ) data _) (at level 0) : poly_scope.
Lemma Yoneda00_View : forall (G : obGenerator), (obGenerator -> Type).
Proof. intros G. refine (fun H => 'Generator( H ~> G ) ). Defined.
Lemma Yoneda01_View : forall (G : obGenerator),
{Yoneda01 : ( forall H H' : obGenerator,
'Generator( H' ~> H ) -> (Yoneda00_View G) H -> (Yoneda00_View G) H' ) |
Yoneda01_functor Yoneda01} .
Proof.
intros. unshelve eexists.
- intros H H' h. refine (fun g => h o>Generator g).
- abstract (split; [intros; exact: polyGenerator_morphism
| intros; exact: polyGenerator_unitGenerator]).
Defined.
Lemma Yoneda00_Param_View : forall (P : obParametrizator), (obGenerator -> Type).
Proof. intros P. refine (fun Q => 'Parametrizator( Parameter0 Q ~> P ) ). Defined.
Lemma Yoneda01_Param_View : forall (P : obParametrizator),
{Yoneda01 : ( forall Q Q' : obGenerator,
'Generator( Q' ~> Q ) -> (Yoneda00_Param_View P) Q -> (Yoneda00_Param_View P) Q' ) |
Yoneda01_functor Yoneda01} .
Proof.
intros. unshelve eexists.
- intros Q Q' q. refine (fun p => (Parameter1 q) o>Parametrizator p).
- abstract (split; [ intros; rewrite /Yoneda01_action /= ; rewrite polyParametrizator_morphism Parameter_morphism; reflexivity
| intros; rewrite /Yoneda01_action /= ; rewrite -Parameter_unitGenerator; exact: polyParametrizator_unitParametrizator ]) .
Defined.
Lemma Yoneda10_FormParam_View : forall G : obGenerator ,
{ Yoneda10 : ( forall H : obGenerator, Yoneda00_View G H -> Yoneda00_Param_View (Parameter0 G) H ) |
Yoneda10_natural (Yoneda01_View G) (Yoneda01_Param_View (Parameter0 G)) Yoneda10 } .
Proof.
intros G. unshelve eexists.
- intros H. refine (@Parameter1 H G).
- abstract(move; intros; symmetry; exact: Parameter_morphism).
Defined.
Section Yoneda00_AtParam_.
Variables (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F).
Definition Yoneda00_AtParam_
(G : obGenerator) (param : Yoneda00_Param_F G)
:= {form : Yoneda00_Form_F G | sval Yoneda10_FormParam_F G form = param} .
Definition Yoneda01_AtParam_action
(Yoneda01_AtParam : ( forall G (param : Yoneda00_Param_F G) (G' : obGenerator) (g : 'Generator( G' ~> G )),
Yoneda00_AtParam_ param -> Yoneda00_AtParam_ (g o>Generator_[sval Yoneda01_Param_F] param) ))
G (param : Yoneda00_Param_F G) (G' : obGenerator) (g : 'Generator( G' ~> G )) (form : Yoneda00_AtParam_ param)
:= (Yoneda01_AtParam G param G' g form).
End Yoneda00_AtParam_.
Notation "''Generator' ( G' ~> G @_ param )" :=
(@Yoneda00_AtParam_ _ _ _ _ (Yoneda10_FormParam_View G) G' param) (at level 0) : poly_scope.
Definition polyGenerator_AtParam : forall G (G' : obGenerator) (g' : 'Generator( G' ~> G )), forall (G'' : obGenerator) param' , 'Generator( G'' ~> G' @_ param' ) -> 'Generator( G'' ~> G @_ (param' o>Parametrizator (Parameter1 g')) ) .
Proof.
intros G G' g' G'' param' g_; unshelve eexists. refine (sval g_ o>Generator g').
- abstract (simpl; rewrite Parameter_morphism;
rewrite [Parameter1 (sval g_)](proj2_sig g_); reflexivity).
Defined.
Definition unitGenerator_AtParam : forall {G : obGenerator} , 'Generator( G ~> G @_ unitParametrizator ) .
Proof.
intros. exists (@unitGenerator G).
abstract (simpl; symmetry; exact: Parameter_unitGenerator).
Defined.
Notation "gp_ o>GeneratorAtParam g'" :=
(@polyGenerator_AtParam _ _ g' _ _ gp_) (at level 40, g' at next level) : poly_scope.
Notation "g o>GeneratorAtParam_ [ Yoneda01_AtParam ] form" :=
(@Yoneda01_AtParam_action _ _ _ _ _ Yoneda01_AtParam _ _ _ g form)
(at level 40, form at next level) : poly_scope.
Notation "g o>GeneratorAtParam_ form" :=
(@Yoneda01_AtParam_action _ _ _ _ _ _ _ _ _ g form)
(at level 40, form at next level) : poly_scope.
Section Yoneda01_AtParam_.
Variables (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F).
Definition Yoneda01_AtParam_functor
(Yoneda01_AtParam : ( forall G (param : Yoneda00_Param_F G) (G' : obGenerator) (g : 'Generator( G' ~> G )),
Yoneda00_AtParam_ Yoneda10_FormParam_F param -> Yoneda00_AtParam_ Yoneda10_FormParam_F (g o>Generator_[sval Yoneda01_Param_F] param) )): Prop :=
( forall G param G' (g : 'Generator( G' ~> G)) G'' (g' : 'Generator( G'' ~> G')) (form : Yoneda00_AtParam_ Yoneda10_FormParam_F param),
sval (g' o>GeneratorAtParam_[Yoneda01_AtParam] (g o>GeneratorAtParam_[Yoneda01_AtParam] form)) =
sval ((g' o>Generator g) o>GeneratorAtParam_[Yoneda01_AtParam] form )) /\
( forall G param (form : Yoneda00_AtParam_ Yoneda10_FormParam_F param),
sval form = sval ((@unitGenerator G) o>GeneratorAtParam_[Yoneda01_AtParam] form) ) .
Definition Yoneda01_AtParam_data
:= { Yoneda01_AtParam : ( forall G (param : Yoneda00_Param_F G) (G' : obGenerator) (g : 'Generator( G' ~> G )),
Yoneda00_AtParam_ Yoneda10_FormParam_F param -> Yoneda00_AtParam_ Yoneda10_FormParam_F (g o>Generator_[sval Yoneda01_Param_F] param) ) |
Yoneda01_AtParam_functor Yoneda01_AtParam }.
Definition Yoneda01_AtParam_ : Yoneda01_AtParam_data.
Proof.
unshelve eexists.
- intros G param G' g form. exists (g o>Generator_[sval Yoneda01_Form_F] (sval form)).
abstract(rewrite -[LHS](proj2_sig Yoneda10_FormParam_F); rewrite [in LHS](proj2_sig form); reflexivity).
- abstract(split; move; simpl; intros; [ exact: (proj1 (proj2_sig Yoneda01_Form_F))
| exact: (proj2 (proj2_sig Yoneda01_Form_F)) ]).
Defined.
End Yoneda01_AtParam_.
Section Subst.
Variables (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F)
(Yoneda00_Param_F' : obGenerator -> Type)
(Yoneda01_Param_F' : Yoneda01_data Yoneda00_Param_F')
(Yoneda10_Param_subst : Yoneda10_data Yoneda01_Param_F' Yoneda01_Param_F).
Definition Yoneda00_Form_Subst : obGenerator -> Type.
Proof.
refine (fun H : obGenerator => { xf : (Yoneda00_Param_F' H * Yoneda00_Form_F H)%type |
sval Yoneda10_Param_subst _ ( fst xf ) = sval Yoneda10_FormParam_F _ ( snd xf ) } ).
Defined.
Axiom Yoneda00_Form_Subst_quotientLogical :
forall G (form form' : Yoneda00_Form_Subst G), snd (sval form) = snd (sval form') -> form = form'.
Definition Yoneda01_Form_Subst : Yoneda01_data Yoneda00_Form_Subst.
Proof.
unshelve eexists.
- intros H H' h xf.
exists ( h o>Generator_[sval Yoneda01_Param_F'] (fst (sval xf)) , h o>Generator_[sval Yoneda01_Form_F] (snd (sval xf)) ) .
abstract (simpl; rewrite -[LHS](proj2_sig Yoneda10_Param_subst); rewrite -[RHS](proj2_sig Yoneda10_FormParam_F);
congr (h o>Generator_ _); exact: (proj2_sig xf)).
- abstract (split; simpl;
first (by intros; apply: Yoneda00_Form_Subst_quotientLogical; simpl;
rewrite -[in RHS](proj1 (proj2_sig (Yoneda01_Form_F))); reflexivity);
intros H xf; apply: Yoneda00_Form_Subst_quotientLogical; simpl;
rewrite -[in RHS](proj2 (proj2_sig (Yoneda01_Form_F)));
move: (sval xf) => sval_xf; destruct sval_xf; reflexivity).
Defined.
Definition Yoneda10_FormParam_Subst : Yoneda10_data Yoneda01_Form_Subst Yoneda01_Param_F'.
Proof.
unshelve eexists.
- intros G xf. exact: (fst (sval xf)).
- abstract (move; reflexivity).
Defined.
End Subst.
Definition Yoneda10_Id : forall (Yoneda00_F : obGenerator -> Type) (Yoneda01_F : Yoneda01_data Yoneda00_F),
Yoneda10_data Yoneda01_F Yoneda01_F.
Proof.
intros; unshelve eexists.
- intros G. refine (id).
- abstract(move; reflexivity).
Defined.
End Senses_obCoMod.
(** # #
#+END_SRC
** Finiteness of the viewing-elements of some viewing-functor
The grammatical colimiting/sum/sigma/viewing-functor-objects [ViewingFunctor_default] assume some finiteness properties ( such as finite-compactness or finite-dimensionality or finite-generated ) onto the viewing-data/topology sense-decodings which they internalize . And these viewing-functor-objects are similar as generators ( representable-functors ) but to be used for functors which are already viewed-functors ( "sheaf" ) . Therefore , and knowning that the viewed-functor construction is exact and commutes with limits , oneself may add/express such things as « viewed-substitution » or « viewed-pi-substitution » , as long as the codomain is already some viewed-functor and the domain for the « cartesian » property is now some viewing-functor .
To facilitate the COQ automatic-arithmetic during the degradation lemma , here oneself shall assume that the cardinality is fixed-the-same for each of the viewing-functor .
#+BEGIN_SRC coq :exports both :results silent # # **)
Module Finiteness.
Parameter isFiniteness_Param_ : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F), Prop.
Parameter (G1 : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(isFiniteness_Param_F : isFiniteness_Param_ Yoneda01_Param_F), obGenerator).
Parameter (param1 : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(isFiniteness_Param_F : isFiniteness_Param_ Yoneda01_Param_F),
Yoneda00_Param_F (G1 isFiniteness_Param_F)).
Parameter (G2 : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(isFiniteness_Param_F : isFiniteness_Param_ Yoneda01_Param_F), obGenerator).
Parameter (param2 : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(isFiniteness_Param_F : isFiniteness_Param_ Yoneda01_Param_F),
Yoneda00_Param_F (G2 isFiniteness_Param_F)).
Section Section1.
Variables (Yoneda00_Param_F : obGenerator -> Type) (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(isFiniteness_Param_F : isFiniteness_Param_ Yoneda01_Param_F).
Inductive is_viewingFunctorParamElement12 : forall (G : obGenerator) (param : Yoneda00_Param_F G), Type :=
| Is_viewingFunctorParamElement12_viewingFunctorParamElement1 : is_viewingFunctorParamElement12 (param1 isFiniteness_Param_F)
| Is_viewingFunctorParamElement12_viewingFunctorParamElement2 : is_viewingFunctorParamElement12 (param2 isFiniteness_Param_F) .
Axiom is_viewingFunctorParamElement12_allP : forall (G : obGenerator) (param : Yoneda00_Param_F G), is_viewingFunctorParamElement12 param.
End Section1.
Parameter isFiniteness_FormParam_ : forall Yoneda00_Form_F (Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F),
forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F),
forall Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F, Prop.
Parameter (form1 form2 : forall Yoneda00_Form_F (Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F),
forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F),
forall Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F,
forall (isFiniteness_FormParam_F : isFiniteness_FormParam_ Yoneda10_FormParam_F),
forall G : obGenerator, forall param : Yoneda00_Param_F G, Yoneda00_AtParam_ Yoneda10_FormParam_F param).
Section Section2.
Variables (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F)
(isFiniteness_FormParam_F : isFiniteness_FormParam_ Yoneda10_FormParam_F)
(G : obGenerator) (param : Yoneda00_Param_F G).
Inductive is_viewingFunctorElement12 : forall (form: Yoneda00_AtParam_ Yoneda10_FormParam_F param), Type :=
| Is_viewingFunctorElement12_viewingFunctorElement1 : is_viewingFunctorElement12 (form1 isFiniteness_FormParam_F param)
| Is_viewingFunctorElement12_viewingFunctorElement2 : is_viewingFunctorElement12 (form2 isFiniteness_FormParam_F param) .
Axiom is_viewingFunctorElement12_allP : forall (form: Yoneda00_AtParam_ Yoneda10_FormParam_F param), is_viewingFunctorElement12 form.
End Section2.
End Finiteness.
(** # #
#+END_SRC
** Grammar of the objects, which carry the sense-decodings
As common , the [View] form-object/index constructor is the (covariant) Yoneda-embedding ( therefore [View G] is some contravariant metafunctor ) . Similarly for the [View_Param] parametrizator-object/index constructor .
Memo that the sum/colimit/sigma-object [ViewingFunctor_default] is simply the grammar/internalization of any (sense/external) viewing-functor which has some finiteness properties ( such as finite-compactness or finite-dimensionality or finite-generated ) , and therefore the sense-decodings of this grammatical sum/colimit/sigma-object is the same as this sense/external viewing-functor . But grammatically , only the viewing-elements of the viewing-functor are touchable (via the morphism constructor [PolyElement_default]) .
Moreover , the form-morphology has the substitution-object ( [Subst] ) , which depends on one fixed-given substitution morphism via its "Yoneda" sense-decoding [Yoneda10_Param_subst] .
And the [Format] parametrizator-index (parameter) really is the common "pullback" ; this will become clearer later in the case of « pi-substitution » objects ...
#+BEGIN_SRC coq :exports both :results silent # # **)
Inductive obCoMod : forall Yoneda00_Form_F (Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F),
forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F),
forall Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F, Type :=
| View : forall G : obGenerator, @obCoMod (Yoneda00_View G) (Yoneda01_View G)
(Yoneda00_Param_View (Parameter0 G)) (Yoneda01_Param_View (Parameter0 G)) (Yoneda10_FormParam_View G)
| ViewingFunctor_default : forall Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F,
forall (isFiniteness_Param_F : Finiteness.isFiniteness_Param_ Yoneda01_Param_F)
(isFiniteness_FormParam_F : Finiteness.isFiniteness_FormParam_ Yoneda10_FormParam_F),
@obCoMod Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F
| ViewedFunctor_default : forall Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F
(F: @obCoMod Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F)
(Param_F : @obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F),
@obCoMod Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F
| Subst : forall Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F
(F: @obCoMod Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F)
(Param_F : @obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F),
forall (Yoneda00_Param_SubstF : obGenerator -> Type)
(Yoneda01_Param_SubstF : Yoneda01_data Yoneda00_Param_SubstF)
(Param_SubstF : @obCoMod_Param Yoneda00_Param_SubstF Yoneda01_Param_SubstF),
forall (Yoneda10_Param_subst : Yoneda10_data Yoneda01_Param_SubstF Yoneda01_Param_F),
@obCoMod (Yoneda00_Form_Subst Yoneda10_FormParam_F Yoneda10_Param_subst)
(Yoneda01_Form_Subst Yoneda10_FormParam_F Yoneda10_Param_subst)
Yoneda00_Param_SubstF Yoneda01_Param_SubstF
(Yoneda10_FormParam_Subst Yoneda10_FormParam_F Yoneda10_Param_subst)
with obCoMod_Param : forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F), Type :=
| View_Param : forall P : obParametrizator, @obCoMod_Param (Yoneda00_Param_View P) (Yoneda01_Param_View P)
| ViewingFunctor_Param_default : forall Yoneda00_Param_F Yoneda01_Param_F,
forall (isFiniteness_Param_F : Finiteness.isFiniteness_Param_ Yoneda01_Param_F),
@obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F
| ViewedFunctor_Param_default : forall Yoneda00_Param_F Yoneda01_Param_F
(Param_F : @obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F),
@obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F
| Format : forall Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F
(F: @obCoMod Yoneda00_Form_F Yoneda01_Form_F Yoneda00_Param_F Yoneda01_Param_F Yoneda10_FormParam_F)
(Param_F : @obCoMod_Param Yoneda00_Param_F Yoneda01_Param_F),
@obCoMod_Param (Yoneda00_Form_Subst Yoneda10_FormParam_F (Yoneda10_Id Yoneda01_Param_F))
(Yoneda01_Form_Subst Yoneda10_FormParam_F (Yoneda10_Id Yoneda01_Param_F)) .
(** # #
#+END_SRC
* Grammatical presentation of morphisms
** Sense-decodings of the morphisms
The sense-decoding of any form-morphism is some metatransformation over the « generator » morphology . The sense-decoding of any parametrizator-morphism is some metatransformation over the « generator » morphology not the generating-parametrizator-morphology . Memo that these sense-decodings may be held for two ends : (1) to express the logical-properties which are carried-as-arguments by the many morphisms constructors ; (2) to express the dependence of the output limit-object ( pi-substitution-object ) on the parametrizator-morphisms contained in some given input diagram ( here the object [Subst] ) .
And both the form-morphology and the parametrizator-morphology have their own viewing-data and (modified-)colimiting(-structure) ( [ViewingFunctor_default] , [ViewedFunctor_default] , [ViewedFunctor1_default] , [UnitViewedFunctor_default] , [PolyElement_default] , [PolyTransf_default] , and similarly [ViewingFunctor_Param_default] ... ) . Memo that the sum/colimit/sigma-object [ViewingFunctor_default] is simply the grammar/internalization of any (sense/external) viewing-functor which has some finiteness properties ( such as finite-compactness or finite-dimensionality or finite-generated ) , and therefore the sense-decodings of this grammatical sum/colimit/sigma-object is the same as this sense/external viewing-functor . But grammatically , only the viewing-elements of the viewing-functor are touchable (via the morphism constructor [PolyElement_default]) .
As common , the [View1] form-morphism/arrow constructor ( which is used to do grammatical « action » ) is the (covariant) Yoneda-embedding ( therefore [View G] is some contravariant metafunctor ) . In contrast , the presentation of the [View1_Param] parametrizator-morphism/arrow constructor ( which is used to do grammatical « action » ) allows some action by any parametrizator-arrow whose domain is the image ( as attested by the inductive [is_Parameter0] ) of some generator-index ; similarly for the sum/colimit/sigma-parametrizator-object [ViewingFunctor_Param_default] , the domain is the image of some generator-index
Moreover , as explained above , because the generating parametrization-functor is not assumed to be « full functor » , then it does not hold that any element of some parametrizator-object (element of metafunctor over the generator-morphology not the generating-parametrizator-morphology) has some fixed-chosen extension as polyelement (metatransformation) . Therefore the constructors of the modified-colimiting-structure ( [PolyElement_default] , [PolyTransf_default] , [PolyElement_Param_default] , [PolyTransf_Param_default] ) shall carry-as-argument some « parameter polyelement-extensioner » ( here [Yoneda10_Param_param_] ) .
Memo that the summing/colimiting/copairing form-morphism constructor [PolyTransf_default] is supported-below by some cocone of parametrizator-morphisms grammatical-codes ; this is necessary during the cut-elimination resolution . Consequently , the viewed-functor constructor [ViewedFunctor1_default] is also supported-below by some parametrizator-morphism grammatical-code ; this is necessary during the cut-elimination resolution .
As common , the forget-morphism ( [Forget] ) for the substitution-object is « polymorph » because it carries/has as-argument some « accumulator form-morphism » ( [ee] ) . In contrast , the forget-morphism ( [Forget] ) and the remember-morphism ( [Remember] ) for the substitution-object are moreover « polyobject » because the precise parametrizator-morphism ( sense-decoding ) argument which defines the subtitution-object ( in the domain for [Forget] or in the codomain for [Remember] ), can be chosen ( [Yoneda10_Param_Forget'] ) .
Memo that the domain of the remember-morphism ( [Remember] ) for the substitution-object is not the most-general , but is some generator-object ( [View] , "representable-functor" ) . Such generator-object is the polymorh correspondent to the ( implicit ) « singleton set » which is used in the sense . This is the intended « cartesian » property . This ( intended , as in the lambda calculus ) limitation can be erased in the case when the generating parametrization-functor is « sense-discrete » , where the parametrizator-morphisms are nested within the inductive-type-family of the form-morphisms and are therefore priorly decidable .
Finally because for now this viewing-data is already assumed to be the default-viewing-data , it is not yet interesting to present/express/add the « common-modified-colimiting constructor » ( such as [PolyTransf_default_common] ) where the (input) target/codomain functor is already some viewed-functor .
#+BEGIN_SRC coq :exports both :results silent # # **)
Module Export Senses_morCoMod.
Lemma Yoneda10_Param_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 => (sval Yoneda10_ff') A \o (sval Yoneda10_ff_) A ).
abstract (intros; move; intros; simpl; rewrite (proj2_sig Yoneda10_ff')
(proj2_sig Yoneda10_ff_); reflexivity).
Defined.
Lemma Yoneda10_UnitCoMod_Param :
forall Yoneda00_Param_F (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F),
Yoneda10_data Yoneda01_Param_F Yoneda01_Param_F .
Proof.
intros. exists (fun G => id).
abstract (intros; move; intros; reflexivity).
Defined.
Definition Yoneda10_Param_View1 :
forall (P : obParametrizator)
(Q : obParametrizator)
(p : 'Parametrizator( P ~> Q )),
{Yoneda10 : forall G : obGenerator, Yoneda00_Param_View P G -> Yoneda00_Param_View Q G | Yoneda10_natural (Yoneda01_Param_View P) (Yoneda01_Param_View Q) Yoneda10}.
Proof.
intros. unshelve eexists.
- intros G. refine (_@ (Parameter0 G) o>Parametrizator p ).
- abstract (move; intros; rewrite /Yoneda01_action /= ; exact: polyParametrizator_morphism).
Defined.
Section is_Parameter0.
Variables (G : obGenerator).
Inductive is_Parameter0 : forall (P : obParametrizator), Type :=
| Is_Parameter0 : is_Parameter0 (Parameter0 G) .
Definition is_Parameter0_transp_rev_codom : forall (P : obParametrizator) (is_Parameter0_P : is_Parameter0 P),
forall G' (p : 'Parametrizator( G' ~> Parameter0 G )), 'Parametrizator( G' ~> P ).
Proof.
intros. destruct is_Parameter0_P. exact: p.
Defined.
Definition is_Parameter0_transp_dom : forall (P : obParametrizator) (is_Parameter0_P : is_Parameter0 P),
forall G' (p : 'Parametrizator( P ~> G' )), 'Parametrizator( Parameter0 G ~> G' ) .
Proof.
intros. destruct is_Parameter0_P. exact: p.
Defined.
End is_Parameter0.
(**MEMO: also refer [Yoneda10_Param_PolyTransf_default_Param] below *)
Definition Yoneda10_Param_PolyTransf_default :
forall (Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_Param_param_ : forall (G : obGenerator) (param : Yoneda00_Param_F G),
Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_F )
(Heq_param : forall (G : obGenerator) (param : Yoneda00_Param_F G),
param = sval (Yoneda10_Param_param_ G param) G (@unitParametrizator (Parameter0 G)) )
(Yoneda00_Param_E : obGenerator -> Type)
(Yoneda01_Param_E : Yoneda01_data Yoneda00_Param_E)
(Yoneda10_Param_ee0 :
forall (G : obGenerator) (param : Yoneda00_Param_F G), Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_E)
(Yoneda10_Param_ee0_morphism :
forall G (param : Yoneda00_Param_F G),
forall (param_ : Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_F )
(Heq_param : param = sval param_ G (@unitParametrizator (Parameter0 G)) ),
forall G' (param' : Yoneda00_Param_View (Parameter0 G) G')
G'' (param'' : Yoneda00_Param_View (Parameter0 G') G''),
sval (Yoneda10_Param_ee0 G param) G'' (param'' o>Parametrizator param') =
sval (Yoneda10_Param_ee0 G' (sval param_ G' param')) G'' param''),
Yoneda10_data Yoneda01_Param_F Yoneda01_Param_E.
Proof.
intros; unshelve eexists.
- intros G param. refine (sval (Yoneda10_Param_ee0 G param) G (unitParametrizator)).
- move; simpl; intros G G' g param; rewrite [LHS](proj2_sig (Yoneda10_Param_ee0 G param)).
rewrite -[_ o>Generator_ _]unitParametrizator_polyParametrizator.
rewrite [Parameter1 g]polyParametrizator_unitParametrizator.
rewrite [LHS](@Yoneda10_Param_ee0_morphism _ _ _ (Heq_param G param)).
rewrite [Parameter1 g]unitParametrizator_polyParametrizator.
rewrite -[in LHS](proj2_sig (Yoneda10_Param_param_ G param));
rewrite -[in LHS]Heq_param; reflexivity.
Defined.
(**MEMO: alt phrasing of [Yoneda10_Param_PolyTransf_default] above *)
Definition Yoneda10_Param_PolyTransf_default_Param :
forall (Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_Param_param_ : forall (G : obGenerator) (param : Yoneda00_Param_F G)
(P : obParametrizator) (is_Parameter0_P : is_Parameter0 G P),
Yoneda10_data (Yoneda01_Param_View P) Yoneda01_Param_F )
(Heq_param : forall (G : obGenerator) (param : Yoneda00_Param_F G)
(P : obParametrizator) (is_Parameter0_P : is_Parameter0 G P),
param = sval (Yoneda10_Param_param_ G param P is_Parameter0_P)
G (is_Parameter0_transp_rev_codom is_Parameter0_P (@unitParametrizator (Parameter0 G))) )
(Yoneda00_Param_E : obGenerator -> Type)
(Yoneda01_Param_E : Yoneda01_data Yoneda00_Param_E)
(Yoneda10_Param_ee : forall (G : obGenerator) (param : Yoneda00_Param_F G)
(P : obParametrizator) (is_Parameter0_P : is_Parameter0 G P),
Yoneda10_data (Yoneda01_Param_View P) Yoneda01_Param_E)
(Yoneda10_Param_ee_morphism :
forall G (param : Yoneda00_Param_F G) (P : obParametrizator) (is_Parameter0_P : is_Parameter0 G P),
forall (param_ : Yoneda10_data (Yoneda01_Param_View P) Yoneda01_Param_F )
(Heq_param : param = sval param_ G (is_Parameter0_transp_rev_codom is_Parameter0_P (@unitParametrizator (Parameter0 G)))),
forall G' (param' : Yoneda00_Param_View P G')
G'' (param'' : Yoneda00_Param_View (Parameter0 G') G''),
sval (Yoneda10_Param_ee G param P is_Parameter0_P) G'' (param'' o>Parametrizator param') =
sval (Yoneda10_Param_ee G' (sval param_ G' param') (Parameter0 G') (Is_Parameter0 G')) G'' param''),
Yoneda10_data Yoneda01_Param_F Yoneda01_Param_E.
Proof.
intros. pose Yoneda10_Param_param_' := ( fun G param => Yoneda10_Param_param_ G param (Parameter0 G) (Is_Parameter0 G) ).
pose Yoneda10_Param_ee' := ( fun G param => Yoneda10_Param_ee G param (Parameter0 G) (Is_Parameter0 G) ).
apply: (Yoneda10_Param_PolyTransf_default (Yoneda10_Param_param_ := Yoneda10_Param_param_') _ (Yoneda10_Param_ee0 := Yoneda10_Param_ee')).
abstract (exact: (fun G param => (Heq_param G param (Parameter0 G) (Is_Parameter0 G)))).
abstract (exact: (fun G param => (Yoneda10_Param_ee_morphism G param (Parameter0 G) (Is_Parameter0 G)))).
Defined.
Section Yoneda10_Form_data.
Variables (Yoneda00_Form_E : obGenerator -> Type)
(Yoneda01_Form_E : Yoneda01_data Yoneda00_Form_E)
(Yoneda00_Param_E : obGenerator -> Type)
(Yoneda01_Param_E : Yoneda01_data Yoneda00_Param_E)
(Yoneda10_FormParam_E : Yoneda10_data Yoneda01_Form_E Yoneda01_Param_E).
Variables (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F).
Variables (Yoneda10_Param_subst : Yoneda10_data Yoneda01_Param_E Yoneda01_Param_F).
Section Section1.
Variables (Yoneda10_Form_ff : forall (G : obGenerator) (param : Yoneda00_Param_E G),
Yoneda00_AtParam_ Yoneda10_FormParam_E ( (**TODO: (sval Yoneda10_Param_project G) **) param) ->
Yoneda00_AtParam_ Yoneda10_FormParam_F ((sval Yoneda10_Param_subst G) param)).
Definition Yoneda10_Form_natural
:= forall (G : obGenerator) (param : Yoneda00_Param_E G) (G' : obGenerator)
(g : 'Generator( G' ~> G )) (form : Yoneda00_AtParam_ Yoneda10_FormParam_E param),
sval (g o>GeneratorAtParam_[sval (Yoneda01_AtParam_(Yoneda10_FormParam_F))] (@Yoneda10_Form_ff G param form))
= sval (@Yoneda10_Form_ff G' (g o>Generator_[sval Yoneda01_Param_E] param)
(g o>GeneratorAtParam_[sval (Yoneda01_AtParam_(Yoneda10_FormParam_E))] form)) .
Definition Yoneda10_Form_quotientLogical
:= forall (G : obGenerator) (param : Yoneda00_Param_E G) (form : Yoneda00_AtParam_ Yoneda10_FormParam_E param)
(param' : Yoneda00_Param_E G) (form' : Yoneda00_AtParam_ Yoneda10_FormParam_E param'),
sval form = sval form' ->
sval (@Yoneda10_Form_ff G param form) = sval (@Yoneda10_Form_ff G param' form') .
End Section1.
Definition Yoneda10_Form_data :=
{ Yoneda10_Form : forall (G : obGenerator) (param : Yoneda00_Param_E G),
Yoneda00_AtParam_ Yoneda10_FormParam_E ( (**TODO: (sval Yoneda10_Param_project G) **) param) ->
Yoneda00_AtParam_ Yoneda10_FormParam_F ((sval Yoneda10_Param_subst G) param) |
Yoneda10_Form_natural Yoneda10_Form /\
Yoneda10_Form_quotientLogical Yoneda10_Form } .
End Yoneda10_Form_data.
Definition Yoneda10_Form_PolyCoMod :
forall (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Form_F G -> Yoneda00_Form_F G' |
Yoneda01_functor Yoneda01})
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Param_F G -> Yoneda00_Param_F G' |
Yoneda01_functor Yoneda01})
(Yoneda10_FormParam_F :
{Yoneda10_FormParam
: forall G : obGenerator, Yoneda00_Form_F G -> Yoneda00_Param_F G |
Yoneda10_natural Yoneda01_Form_F Yoneda01_Param_F Yoneda10_FormParam})
(Yoneda00_Form_F' : obGenerator -> Type)
(Yoneda01_Form_F' :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Form_F' G -> Yoneda00_Form_F' G' |
Yoneda01_functor Yoneda01})
(Yoneda00_Param_F' : obGenerator -> Type)
(Yoneda01_Param_F' :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Param_F' G -> Yoneda00_Param_F' G' |
Yoneda01_functor Yoneda01})
(Yoneda10_FormParam_F' :
{Yoneda10_FormParam
: forall G : obGenerator, Yoneda00_Form_F' G -> Yoneda00_Param_F' G |
Yoneda10_natural Yoneda01_Form_F' Yoneda01_Param_F' Yoneda10_FormParam})
(Yoneda10_Param_ff' :
{Yoneda10_Param
: forall G : obGenerator, Yoneda00_Param_F' G -> Yoneda00_Param_F G |
Yoneda10_natural Yoneda01_Param_F' Yoneda01_Param_F Yoneda10_Param})
(Yoneda10_Form_ff' :
Yoneda10_Form_data Yoneda10_FormParam_F' Yoneda10_FormParam_F
Yoneda10_Param_ff')
(Yoneda00_Form_F'' : obGenerator -> Type)
(Yoneda01_Form_F'' :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Form_F'' G -> Yoneda00_Form_F'' G' |
Yoneda01_functor Yoneda01})
(Yoneda00_Param_F'' : obGenerator -> Type)
(Yoneda01_Param_F'' :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Param_F'' G -> Yoneda00_Param_F'' G' |
Yoneda01_functor Yoneda01})
(Yoneda10_FormParam_F'' :
{Yoneda10_FormParam
: forall G : obGenerator, Yoneda00_Form_F'' G -> Yoneda00_Param_F'' G |
Yoneda10_natural Yoneda01_Form_F'' Yoneda01_Param_F'' Yoneda10_FormParam})
(Yoneda10_Param_ff_ :
{Yoneda10_Param
: forall G : obGenerator, Yoneda00_Param_F'' G -> Yoneda00_Param_F' G |
Yoneda10_natural Yoneda01_Param_F'' Yoneda01_Param_F' Yoneda10_Param})
(Yoneda10_Form_ff_ :
Yoneda10_Form_data Yoneda10_FormParam_F'' Yoneda10_FormParam_F'
Yoneda10_Param_ff_) ,
Yoneda10_Form_data Yoneda10_FormParam_F'' Yoneda10_FormParam_F
(Yoneda10_Param_PolyCoMod Yoneda10_Param_ff_
Yoneda10_Param_ff').
Proof.
intros. unshelve eexists.
- intros G param dataIn. unshelve eexists.
+ apply: (sval (sval Yoneda10_Form_ff' _ (sval Yoneda10_Param_ff_ _ param) _)). unshelve eexists.
* exact: (sval (sval Yoneda10_Form_ff_ _ param dataIn)).
* abstract (exact: (proj2_sig (sval Yoneda10_Form_ff_ _ _ _ ))).
+ abstract (simpl; rewrite [LHS](proj2_sig (sval Yoneda10_Form_ff' _ _ _)); reflexivity).
- abstract (split; [ move; simpl; intros; rewrite [LHS](proj1 (proj2_sig Yoneda10_Form_ff'));
apply: (proj2 (proj2_sig Yoneda10_Form_ff'));
simpl; exact: (proj1 (proj2_sig Yoneda10_Form_ff_))
(*ALT: rewrite [LHS](proj1 (proj2_sig Yoneda10_Form_ff_)).
apply: (proj2 (proj2_sig Yoneda10_Form_ff_)). *)
| move; simpl; intros; apply: (proj2 (proj2_sig Yoneda10_Form_ff'));
simpl; apply: (proj2 (proj2_sig Yoneda10_Form_ff_)); assumption ]).
Defined.
Definition Yoneda10_UnitCoMod
(Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F) :
Yoneda10_Form_data Yoneda10_FormParam_F Yoneda10_FormParam_F (Yoneda10_UnitCoMod_Param Yoneda01_Param_F).
Proof.
intros; unshelve eexists.
- refine (fun G param => id).
- abstract (split; move; simpl; intros; [ reflexivity | assumption ]).
Defined.
Definition Yoneda10_Form_View1 :
forall (G : obGenerator) (H : obGenerator) (g : 'Generator( H ~> G )),
Yoneda10_Form_data (Yoneda10_FormParam_View H) (Yoneda10_FormParam_View G)
(Yoneda10_Param_View1 (Parameter1 g)) .
Proof.
intros G H hg. unshelve eexists.
- intros G0 x h . exists ( (sval h) o>Generator hg ).
abstract (move: (proj2_sig h); rewrite /Yoneda10_Param_View1 /Yoneda10_FormParam_View /= ;
rewrite Parameter_morphism ; move -> ; reflexivity).
- abstract (split; [ move; simpl; intros ; rewrite /Yoneda01_action /= ; exact: polyGenerator_morphism
| move; simpl; intros; congr ( _ o>Generator hg ); assumption] ).
Defined.
Definition Yoneda10_Form_PolyElement_default :
forall (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F)
(Yoneda10_Param_form_ : forall G : obGenerator, Yoneda00_Param_F G -> Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_F)
(Heq_param : forall (G : obGenerator) (param : Yoneda00_Param_F G), param = sval (Yoneda10_Param_form_ G param) G unitParametrizator)
(G : obGenerator)
(param : Yoneda00_Param_F G)
(form : Yoneda00_AtParam_ Yoneda10_FormParam_F param),
Yoneda10_Form_data (Yoneda10_FormParam_View G) Yoneda10_FormParam_F (Yoneda10_Param_form_ G param).
Proof.
intros. unshelve eexists.
- intros G0 param0 form0. exists (sval ( (sval form0) o>GeneratorAtParam_[sval (Yoneda01_AtParam_ Yoneda10_FormParam_F)] form )).
abstract (rewrite -[LHS](proj2_sig Yoneda10_FormParam_F);
rewrite [in LHS](proj2_sig form);
rewrite [param in LHS]Heq_param;
rewrite [LHS](proj2_sig (Yoneda10_Param_form_ _ _));
congr ( sval (Yoneda10_Param_form_ _ _) );
rewrite [LHS]/Yoneda01_action [LHS]/= -[LHS]unitParametrizator_polyParametrizator;
exact: (proj2_sig form0) ).
- abstract (split; [ move; simpl; intros; rewrite -[RHS](proj1 (proj2_sig Yoneda01_Form_F)); reflexivity
| move; simpl; intros; congr ( _ o>Generator_ (sval form) ); assumption ]).
Defined.
Definition Yoneda10_Form_PolyTransf_default :
forall (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F)
(Yoneda10_Param_param_ : forall G : obGenerator, Yoneda00_Param_F G -> Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_F)
(Heq_param : forall (G : obGenerator) (param : Yoneda00_Param_F G), param = sval (Yoneda10_Param_param_ G param) G unitParametrizator)
(Yoneda00_Form_E : obGenerator -> Type)
(Yoneda01_Form_E : Yoneda01_data Yoneda00_Form_E)
(Yoneda00_Param_E : obGenerator -> Type)
(Yoneda01_Param_E : Yoneda01_data Yoneda00_Param_E)
(Yoneda10_FormParam_E : Yoneda10_data Yoneda01_Form_E Yoneda01_Param_E)
(Yoneda10_Param_ee0 : forall G : obGenerator, Yoneda00_Param_F G -> Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_E)
(Yoneda10_Param_ee0_morphism :
forall G (param : Yoneda00_Param_F G),
forall (param_ : Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_F )
(Heq_param : param = sval param_ G (@unitParametrizator (Parameter0 G)) ),
forall G' (param' : Yoneda00_Param_View (Parameter0 G) G')
G'' (param'' : Yoneda00_Param_View (Parameter0 G') G''),
sval (Yoneda10_Param_ee0 G param) G'' (param'' o>Parametrizator param') =
sval (Yoneda10_Param_ee0 G' (sval param_ G' param')) G'' param'')
(Yoneda10_Param_ee : forall (G : obGenerator) (param : Yoneda00_Param_F G), Yoneda00_AtParam_ Yoneda10_FormParam_F param -> Yoneda10_data (Yoneda01_Param_View (Parameter0 G)) Yoneda01_Param_E)
(Yoneda10_Form_ee :
forall (G : obGenerator) (param : Yoneda00_Param_F G) (form : Yoneda00_AtParam_ Yoneda10_FormParam_F param),
Yoneda10_Form_data (Yoneda10_FormParam_View G) Yoneda10_FormParam_E (Yoneda10_Param_ee G param form))
(Heq_param_ee :
forall (G : obGenerator) (param : Yoneda00_Param_F G) (form : Yoneda00_AtParam_ Yoneda10_FormParam_F param) (G' : obGenerator) (param' : Yoneda00_Param_View (Parameter0 G) G'),
sval (Yoneda10_Param_ee G param form) G' param' = sval (Yoneda10_Param_ee0 G param) G' param')
(Yoneda10_Form_ee_quotientLogical :
forall (G : obGenerator) (param : Yoneda00_Param_F G) (form : {form : Yoneda00_Form_F G | sval Yoneda10_FormParam_F G form = param}) (param' : Yoneda00_Param_F G)
(form' : {form0 : Yoneda00_Form_F G | sval Yoneda10_FormParam_F G form0 = param'}),
sval form = sval form' ->
forall (G0 : obGenerator) (param0 : Yoneda00_Param_View (Parameter0 G) G0) (form0 : 'Generator ( G0 ~> G @_ param0 )),
sval (sval (Yoneda10_Form_ee G param form) G0 param0 form0) = sval (sval (Yoneda10_Form_ee G param' form') G0 param0 form0))
(Yoneda10_Form_ee_morphism :
forall (G G' : obGenerator) (g : 'Generator( G' ~> G )) (param : Yoneda00_Param_F G) (form : Yoneda00_AtParam_ Yoneda10_FormParam_F param) (G'' : obGenerator)
(param' : Yoneda00_Param_View (Parameter0 G') G'') (form' : 'Generator ( G'' ~> G' @_ param' )),
sval (sval (Yoneda10_Form_ee G param form) G'' (param' o>Parametrizator Parameter1 g) (form' o>GeneratorAtParam g)) =
sval (sval (Yoneda10_Form_ee G' (g o>Generator_[sval Yoneda01_Param_F] param) (g o>GeneratorAtParam_[sval (Yoneda01_AtParam_(Yoneda10_FormParam_F))] form)) G'' param' form')),
Yoneda10_Form_data Yoneda10_FormParam_F Yoneda10_FormParam_E (Yoneda10_Param_PolyTransf_default Heq_param Yoneda10_Param_ee0_morphism).
Proof.
intros. unshelve eexists.
- intros G param form; simpl. unshelve eexists.
+ exact: (sval (sval (Yoneda10_Form_ee G param form) _ _ unitGenerator_AtParam)).
+ abstract (rewrite [LHS](proj2_sig (sval (Yoneda10_Form_ee G param form) _ _ _));
rewrite Heq_param_ee; reflexivity).
- abstract (split; [ move; simpl; intros G param G' g form;
rewrite [LHS](proj1 (proj2_sig (Yoneda10_Form_ee G param form))) /=;
rewrite -[RHS]Yoneda10_Form_ee_morphism;
apply: (proj2 (proj2_sig (Yoneda10_Form_ee G param form))); simpl;
rewrite -[LHS]unitGenerator_polyGenerator;
exact: polyGenerator_unitGenerator
| move; simpl; intros G param form param' form' Heq;
apply: Yoneda10_Form_ee_quotientLogical; assumption ]).
Defined.
Definition Yoneda10_Form_Forget :
forall (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Form_F G -> Yoneda00_Form_F G' |
Yoneda01_functor Yoneda01})
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) -> Yoneda00_Param_F G -> Yoneda00_Param_F G' |
Yoneda01_functor Yoneda01})
(Yoneda10_FormParam_F :
{Yoneda10 : forall G : obGenerator, Yoneda00_Form_F G -> Yoneda00_Param_F G |
Yoneda10_natural Yoneda01_Form_F Yoneda01_Param_F Yoneda10})
(Yoneda00_Param_SubstF : obGenerator -> Type)
(Yoneda01_Param_SubstF :
{Yoneda01
: forall G G' : obGenerator,
'Generator( G' ~> G ) ->
Yoneda00_Param_SubstF G -> Yoneda00_Param_SubstF G' |
Yoneda01_functor Yoneda01})
(Yoneda10_Param_Forget :
{Yoneda10
: forall G : obGenerator, Yoneda00_Param_SubstF G -> Yoneda00_Param_F G |
Yoneda10_natural Yoneda01_Param_SubstF Yoneda01_Param_F Yoneda10})
(Yoneda10_Param_Forget' :
{Yoneda10
: forall G : obGenerator, Yoneda00_Param_SubstF G -> Yoneda00_Param_F G |
Yoneda10_natural Yoneda01_Param_SubstF Yoneda01_Param_F Yoneda10})
(Heq_subst : forall G param, sval Yoneda10_Param_Forget' G param = sval Yoneda10_Param_Forget G param),
Yoneda10_Form_data
(Yoneda10_FormParam_Subst Yoneda10_FormParam_F Yoneda10_Param_Forget')
Yoneda10_FormParam_F Yoneda10_Param_Forget.
Proof.
intros. unshelve eexists.
- intros G param form . exists (snd (sval (sval form))).
abstract(rewrite -[LHS](proj2_sig (sval form)); rewrite Heq_subst;
congr (sval Yoneda10_Param_Forget); exact: (proj2_sig form)).
- abstract (split; [move; simpl; intros; reflexivity
| move; simpl; intros; congr (snd (sval _ )); assumption] ).
Defined.
Definition Yoneda10_Form_Remember :
forall (Yoneda00_Form_F : obGenerator -> Type) (Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F) (Yoneda00_Param_F : obGenerator -> Type) (Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F) (Yoneda00_Param_SubstF : obGenerator -> Type)
(Yoneda01_Param_SubstF : Yoneda01_data Yoneda00_Param_SubstF) (Yoneda10_Param_Forget : Yoneda10_data Yoneda01_Param_SubstF Yoneda01_Param_F),
forall Yoneda10_Param_Forget'
(Heq_subst : forall G param, sval Yoneda10_Param_Forget' G param = sval Yoneda10_Param_Forget G param),
forall (Yoneda00_Form_L : obGenerator -> Type) (Yoneda01_Form_L : Yoneda01_data Yoneda00_Form_L) (Yoneda00_Param_L : obGenerator -> Type) (Yoneda01_Param_L : Yoneda01_data Yoneda00_Param_L)
(Yoneda10_FormParam_L : Yoneda10_data Yoneda01_Form_L Yoneda01_Param_L)
(Yoneda10_Param_ll_ : Yoneda10_data Yoneda01_Param_L Yoneda01_Param_SubstF),
forall (Yoneda10_Param_ll : Yoneda10_data Yoneda01_Param_L Yoneda01_Param_F) (Yoneda10_Form_ll : Yoneda10_Form_data Yoneda10_FormParam_L Yoneda10_FormParam_F Yoneda10_Param_ll),
forall (Heq_param : forall G param, sval Yoneda10_Param_ll G param
= sval (Yoneda10_Param_PolyCoMod Yoneda10_Param_ll_ Yoneda10_Param_Forget) G param),
Yoneda10_Form_data Yoneda10_FormParam_L (Yoneda10_FormParam_Subst Yoneda10_FormParam_F Yoneda10_Param_Forget') Yoneda10_Param_ll_ .
Proof.
intros. unshelve eexists.
- intros G param form. unshelve eexists.
+ unshelve eexists.
* refine ( (sval Yoneda10_Param_ll_ G param) , (sval (sval Yoneda10_Form_ll _ _ form))).
* abstract (simpl; rewrite [RHS](proj2_sig (sval Yoneda10_Form_ll _ _ _ )); rewrite Heq_subst Heq_param; reflexivity).
+ abstract (simpl; reflexivity).
- abstract (split; [ move; simpl; intros; apply: Yoneda00_Form_Subst_quotientLogical; simpl;
(*TODO: HERE*) rewrite [X in X = _](proj1 (proj2_sig Yoneda10_Form_ll)); reflexivity
| move; simpl; intros; apply: Yoneda00_Form_Subst_quotientLogical; simpl;
apply: (proj2 (proj2_sig Yoneda10_Form_ll)); assumption ]).
Defined.
Definition Yoneda10_Param_Formatting :
forall (Yoneda00_Form_F : obGenerator -> Type)
(Yoneda01_Form_F : Yoneda01_data Yoneda00_Form_F)
(Yoneda00_Param_F : obGenerator -> Type)
(Yoneda01_Param_F : Yoneda01_data Yoneda00_Param_F)
(Yoneda10_FormParam_F : Yoneda10_data Yoneda01_Form_F Yoneda01_Param_F)
(Yoneda00_Form_E : obGenerator -> Type)
(Yoneda01_Form_E : Yoneda01_data Yoneda00_Form_E)
(Yoneda00_Param_E : obGenerator -> Type)
(Yoneda01_Param_E : Yoneda01_data Yoneda00_Param_E)
(Yoneda10_FormParam_E : Yoneda10_data Yoneda01_Form_E Yoneda01_Param_E)