[HoTT] Re: [CMU-HoTT] Special lectures Directed Type Theory — via dependent profunctor-types following Kosta Dosen

[HoTT] Re: [CMU-HoTT] Special lectures Directed Type Theory — via dependent profunctor-types following Kosta Dosen

[admin]

Salut DCC, ton 2ème cours sémantique m'ennuyait alors en attente du 3ème cours syntaxique voici une response at yesterday's Joyal hint towards hes alternative presentation via barrels (profunctors):

  https://ncatlab.org/joyalscatlab/published/Distributors+and+barrels

implemented as cut-elimination in the double category of dependent-profunctors with J-rule-eliminated adjunctions:

  https://github.com/1337777/cartier/blob/master/cartierSolution12.lp

Here, a covering (co)sieve is implemented simply as a fibration of profunctors, which covers some base (unit-hom) profunctor at some fixed covariant variable (the contravariant piece is understood as some codomain fibration of categories). This was hinted also in Joyal's page.

Now this failure of sieves being monomorphisms is the motivation for the new “grammatical sheaf cohomology”, where the redundant storage space for functions defined over the topology is what allows possibly-incompatible functions to be glued:

  gluing: F(U0)⊕F(U1)⊕F(U01) → F(U)
  ((f0,f01),(g1,g01),(h01)) ↦ (f0,g1,f01+g01-h01)

Another alternative from “type theory” and its types with (global) elements, is instead Kosta Dosen-style “categorial programming” which is about morphisms (generalized elements) between profunctor-types (of arrows data). This new functorial lambda calculus evaluation has been implemented as:

  “ϵ_(B,O)∘ B⊗(g)” ∘ (x⊗f)
  = “ϵ_(A,O)∘ A⊗((x⇒O) ∘ (g ∘ f))” , for x:A→B

where the input argument x is simply accumulated using the implication _⇒_ bifunctor. And the new “J-rule” has been implemented as simply the construction that, given some global element of some profunctor datatype, it generates the morphism (transformation) from the unit-hom-profunctor towards this profunctor datatype (semantically by covariant/contravariant action/composition):

  | Unit_con_transf : Π [I A B J : cat] [F : func I A] [R : mod A B] [G : func I B], Π (M : func J A), hom F R G → transf (Unit_mod M F) Id_func (M ∘>> R) G

Therefore, this general setup has facilitated the implementation of cut-elimination (J-rule elimination) for any adjunctions of functors and of their decidability of equations between data (arrows inside categories). Also this implementation has expressed and proved computationally that any right adjoint functor preserves the profunctor-weighted limits of other functors:

  assert [B J J' A I : cat] (F : func J B) (W : mod J' J) (F_⇐_W : func J' B) (isl : isLimit F W F_⇐_W) (R : func B A) (L : func A B) (isa : isAdj L R) (M : func I A) ⊢
  ((((M)_'∘> (Adj_cov_hom isa F)) ⇐2 (Id_transf W))
    ''∘ (limit_intro_transf isl (M ∘> L)))
          ''∘ ((Adj_con_hom isa M) ∘>'_(F_⇐_W))
  : transf ((Unit_mod M (R <∘ F)) ⇐ W) Id_func (Unit_mod M (R <∘ F_⇐_W)) Id_func

This implementation moreover would enable new executable applications to the study of graphs transformations understood as categorial rewriting in a double category, where the objects are graphs, the vertical monomorphisms are pattern-matching subterms inside contexts and the horizontal morphisms are congruent/contextual rewriting steps.

Finally, the core difficulty at implementing Kosta Dosen (ref [1], [2], [3], [4], [5]) would be the long-term synchronized industrial labor and the new format for reviewers-productive-output, which requires tools such as:

  [CfP] WorkSchool 365 is a new marketing format for authors/brands to disqualify reviewers/customers, sign-in at https://WorkSchool365.com 

[1] Dosen-Petric: Cut Elimination in Categories 1999;
[2] Proof-Theoretical Coherence 2004; 
[3] Proof-Net Categories 2005; 
[4] Coherence in Linear Predicate Logic 2007; 
[5] Coherence for closed categories with biproducts 2022
[6] Pierre Cartier



-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/BYAPR20MB2790C743D51D7ADF7AFA077291819%40BYAPR20MB2790.namprd20.prod.outlook.com.