Re: [isabelle] New AFP entry: Monoidal Categories

Re: [isabelle] New AFP entry: Monoidal Categories

[1337777.OOO]

Proph

https://github.com/1337777/maclane/blob/master/maclaneSolution2.thy
https://github.com/1337777/maclane/blob/master/maclaneSolution2.v
https://github.com/1337777/dosen/blob/master/coherence2.v

solves how 1337777 mom associativity pentagon is some recursive square
(reflective-functorial associativity-bracket-elimination
cut-elimination resolution)

The only thing to remember : this grammatical
associativity-bracket-elimination cut-elimination resolution and
confluence technique is the foundation of polymorph mathematics ...

What is the metalogic for polymorphism ? ( "HOL vs COQ" )

HOL has its own metalogic which is parallel-search ( "sequent/natural"
, using unlimited-outer-nesting-of-metaconsequences as questioned by
Kubota ) deduction with unification of metavariables . Therefore HOL
may erase logical-properties from progamming and instead deleguate ,
to some ad-hoc particular "object-logic" , the task of automatic
inferences involved during programming-under-logical-context . For
example , definite/indefinite descriptions or how to simulate implicit
parameters in the polymorphism object-logic :

( wellIndexed f A B ==> wellIndexed g B C ==> ( CompositionImplicit f g
= ( Composition A B f C g :: morphismsDatatype ) ) )

COQ unites programs carrying logical-properties via indexed/dependent
datatypes ; the consequence is the semi-automatic
inference/unification of implicit/hidden parameters via
existential/meta-variables . Does this say that dependent-types (
beyond its semi-automatic inference/unification algorithms ) is better
for polymorphism ( "category theory" ) ? NO ... The pretty search into
the ``categorical semantics of (higher-)dependent-types as internal
logic'' is for the museum mostly ; the angle of view of polymorphism
mathematics is that itself is ( by-definition ... ) some computational
logic .

-----

Proph

https://gitlab.com/1337777/cartier/blob/master/cartierSolution4.v

solves half of some question of Cartier which is how to program
grammatical polymorph internal ( "typed" , "small" )
pairing-projections ( "product" ) ...

The ends is to do polymorph mathematics which is internal/small/typed
ref some indexer/types (metacategory/topos/modos) ; this infers that
the objects and morphisms can no longer be touched individually but
many objects shall be touched at the same time via some
indexing/dimension/type and many morphisms shall be touched at the
same time via some indexing/dimension/type . And for internal
polymorph mathematics , the common operations on the morphisms are
coordinatewise/dimensional/pointwise ; this contrast from
enriched/multifolded polymorph mathematics where each object is
touched individually and many morphisms are touched at the same time
and the common operations on the morphisms are multiplicative .

How to describe the two indexes which encode those pair objects and
those pairing-projections morphisms ? Oneself could decode ( "Yoneda"
) these two index-for-objects and index-for-morphisms as two
metafunctors on this indexer/metacategory ; then these two
metafunctors may be commonly programmed by two
inductive-families-presentations where the constructors of these two
inductive-families-presentations are the decoding ( "Yoneda" ) as
metatransformations of the whatever-is-interesting arrows between
these two index-for-objects and index-for-morphisms .

The conversion-relation shall convert across two morphisms whose
domain/codomain-computation arguments are not
syntactically/grammatically-the-same. But oneself does show that, by
logical-deduction, these two domain/codomain-computations are indeed
propositionally equal ( "soundness lemma" ) .

Finally, some linear total/asymptotic grade is defined on the
morphisms and the tactics-automated degradation lemma shows that each
of the conversion indeed degrades the redex morphism .

For instant first impression , the conversion-relation constructor
which says that the first projection morphism is natural/polyarrowing
(commutativity along the arrow-action cut-constructor) , is written as
:

#+BEGIN_EXAMPLE
| Project1_arrow : forall (A : obIndexer) (F1 F2 : obCoMod A),
    forall (Z1 : obCoMod A) (zz1 : 'CoMod(0 F1 ~> Z1 )0),
    forall (A' : obIndexer) (a : 'Indexer(0 A' ~> A )0),
          ( ~_1 @ (ObCoMod_Poly a F2) o>CoMod (a o>* zz1) )
            <~~ ( a o>* ( ~_1 @ F2 o>CoMod zz1 ) )
#+END_EXAMPLE

KEYWORDS : 1337777.OOO ; COQ ; cut-elimination ; internal functors ;
internal product ; polymorph metafunctors-grammar ; modos

OUTLINE :

  * Generating data internal some indexer , by decoding the indexes as
metafunctors and the arrows as metatransformations

  * Grammatical presentation of objects and morphisms internal some
indexer , by decoding the indexes as metafunctors and the arrows as
metatransformations
  ** Grammatical presentation of objects
  ** Grammatical presentation of morphisms

  * Grammatical conversions of morphisms , which infer the same
domain/codomain-computation
  ** Grammatical conversions of morphisms
  ** Same domain/codomain-computation for convertible morphisms
  ** Linear total/asymptotic grade and the degradation lemma

  * Solution
  ** Solution morphisms without polyarrowing/polymorphism
  ** Destruction of morphisms with inner-instantiation of object-indexes

  * Polyarrowing/polymorphism/cut-elimination by
computational/total/asymptotic/reduction/(multi-step) resolution

-----

Proph

https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution5.v

solves half of some question of Cartier which is how to program
grammatical polymorph contextual ( "weighted" ) multifold ( "enriched"
) pairing-projections ( "product" ) ...

The ends is to do polymorph mathematics which is multifolded/enriched
ref some indexer (symmetric-associative-monoidal
metalogic/metacategory) ; this infers that the morphisms can no longer
be touched individually but many morphisms shall be touched at the
same time via some indexing/multiplier . And for multifold-enriched
polymorph mathematics , the common operations on the morphisms are
multifold/multiplicative ; this contrast from internal polymorph
mathematics where many objects are touched at the same time and
moreover many morphisms are touched at the same time and the common
operations on the morphisms are coordinatewise/dimensional/pointwise .

Each decoding ( "Yoneda" ) of some index-for-morphisms which encodes
all the morphisms-at-some-domain-codomain is some metafunctor , which
is programmed by some inductive-family-presentation whose
additional/embedded 2 constructors  signify the functoriality (
"parameter-arrow-action" and  "structure-arrow-action" ) . Each
decoding ( "Yoneda" ) of the whatever-is-interesting arrows between
the indexes-for-morphisms are metatransformations which are programmed
as some grammatical-constructors of this inductive-family-presentation
of the morphisms .

The conversion-relation would convert across two morphisms whose
multiplicities-indexes are not syntactically/grammatically-the-same.
But oneself does show that , by structure-arrow-action (
metalogic-deduction ) , these two multiplicities are indeed (
symmetric-associative-monoidal-metalogic ) propositionally equal (
"soundness lemma" ) .

Finally, some linear total/asymptotic grade is defined on the
morphisms and the tactics-automated degradation lemma shows that each
of the conversion indeed degrades the redex morphism .

For instant first impression , the conversion-relation constructor
which says that the first projection morphism is natural/polyarrowing
(commutativity along the parameter-arrow-action cut-constructor) , is
written as :

#+BEGIN_EXAMPLE
| Project1_MorCoMod_Poly_Param : forall (F1 F2 : obCoMod) (Z1 : obCoMod)
    (A : obIndexer) (zz1 : 'CoMod(0 A |- F1 ~> Z1 )0), forall (A' : obIndexer)
    (a : 'Indexer(0 A' ~> A @ Cong.MorIndexer_Param.morIndexer )0 %cong),
      ( ~_1 @ F2 o>CoMod (a o>* zz1) )
        <~~ ( (Cong.Context1_arrow a) o>* ( ~_1 @ F2 o>CoMod zz1 ) )
#+END_EXAMPLE

KEYWORDS : 1337777.OOO ; COQ ; cut-elimination ; multifold-enriched
functors ; contextual-weighted multifold-enriched product ; polymorph
metafunctors-grammar ; modos

OUTLINE :

  * Indexer metalogic for multifold-enrichment , lemma for commutation
of parameter-polyarrowing along structure-arrow-action
  ** Indexer metalogic is half-grammatical half-sense and is
symmetric-associative-monoidal with some context ( "product-weight" )
constructor , and is presented in the congruent-rewrite style
  ** Lemma for commutation of parameter-polyarrowing along
structure-arrow-action

  * Generating data multifolded-enriched ref some indexer

  * Grammatical presentation of objects and morphisms
multifolded/enriched ref some indexer , by distinguishing
parameter-polyarrowing from structure-arrow-action

  * Grammatical conversions of morphisms , which infer the same
multiplicity-computation
  ** Grammatical conversions of morphisms
  ** Same multiplicity-computation for convertible morphisms
  ** Linear total/asymptotic grade and the degradation lemma

  * Solution
  ** Solution morphisms without (parameter-polyarrowing)/polymorphism
  ** Destruction of morphisms with inner-instantiation of object-indexes

  * (parameter-polyarrowing)/polymorphism/cut-elimination by
computational/total/asymptotic/reduction/(multi-step) resolution

-----

                             {YinYang> fiction }

<anointed one> so are you going to
<anointed one> also ...
<anointed one> pay/review/cite 1337777 mom recursive square ?
<anointed one> hint : github.com/1337777/maclane/issues
<noisea> but but
<noisea> I don't want to "endorse" her recursive square
<anointed one> you mean that you would instead
force-fool-and-theft/lie/falsification
<anointed one> and misappropriate public funds via
interdependent-detour ... detournement de fonds publics
<noisea> anybody needs to steal these stuff ? these trivial stuff
don't solve world hunger
<anointed one> did YOUR heir steal MY autonomous stuff , as medium for
coward malice ?
<anointed one> hint : it is not absence of knowledge ...
<anointed one> primo your lies-that-your-are-not-thief causes the
wrong question , secondo your answer to this wrong question is
perverted !
<anointed one> here is some analogy/parallel along the "aircraft
paradox" en.wikipedia.org/wiki/Survivorship_bias
<anointed one> at the end , two questions are possible :
<anointed one> (A) did tribalistic-interdependence (cockpit area)
steal the money-funding (SAM projectile hit) of the failed
work-projects (downed lost aircraft) ?
<anointed one> or (B) from the visible surviving work-projects
(returning surviving aircraft) which are only half of the total
work-projects (aircraft missions) , how to make the money-funding
"more uniform" across the public (wing area) and
tribalistic-interdependence (cockpit area) ?
<anointed one> primo, tribalistic-interdependence
lies-that-it-did-not-steal will cause the distraction from question
(A) to question (B)
<anointed one> secondo, aesthetic-perversion will cause to make the
money-funding "more uniform" by shielding the public (wing area)
against receiving money-funding !1?
<noisea> I meant ...
         {yang> you are not Gauss or something }
<anointed one> anyway the public audience is seeking to hire some new
publisher-in-chief
<anointed one> your new tooling is simple :
<anointed one> ` wget https://github.com/1337777/maclane/  -e
robots=off -np -r -l 1 -p --warc-file=maclaneCache ; ipwb index
maclaneCache.warc.gz >> maclaneCache.cdxj ; ipwb replay
10101010IPFS0101SWARM0101 `
<noisea> but but
<noisea> the "reviewer" must have his tribalistic-interdependence
hidden such to "feel" "freedom of speech" of mathematics
<anointed one> this is for another "aircraft paradox"-style or "linux
vs micro$oft"-style question , but let's skip to the punchline
<anointed one> you forgot ITP2015 quickly eh ? so you want to hide that you are
<anointed one> the same "reviewer" who did deny to pay the 1337777 mom
recursive square
<anointed one> and forced her son out of your noiseaous classroom ...
               {yin> mandatory bidet-washlet is not enough , LOL }
<anointed one> by calling the PLA army ?!1!
<noisea> INAPPROPRIATE ! WOOF ! WOOF ! INAPPROPRIATE !

-----

BUY MOM RECURSIVE T-SQUARE paypal.me/1337777 1337777.OOO@gmail.com ;
微信支付 2796386464@qq.com ; eth
0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon
amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777