Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • main default protected
  • master
2 results
Created with Raphaël 2.2.010Oct9875329Sep26222015730Aug2823221584128Jul25201811325Jun2085432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861representableRelation on injNat, injArrsome work on normalizationone easy manual case of normalization proofsome progress on the monad simplifier proof. Used the Nbe solver forimplement the end-to-end monad normalization functionoutline of normalizationImplement Nbe for solving substitution equationswork on nbenbe stuffbegin Nbe for substitutionsremove two more more outdated syntax filesRemove outdated syntax filesNew intensional term syntaxInductive definition of perturbationsWeak bisimilarity relation on Lift XAdditions to Lift.agdadoublePosetCombinatorsupdate representableRelationupdate DoublePosetInit double poset constructions fileDouble posets and their morphismssome writingQuasi-Representable RelationsFinish concrete poset semantics of the term syntax"Product" of monotone relationsmake some definitions more universe-polymorphicMonoid-related definitions and constructionsWork on intensional concrete semantics (pseudo-representable relations)Construct dyn as a poset with perturbation monoidsPosets with two perturbation monoids (one for emb, one for proj)Additions to Common.agdaDefine iterated composition of monotone endofunctionsMore constructions on posetsMore proofs involving Liftcomplete homo proof for LPWPchanges in Constructions.agdaadd hom proof for LPWPchanges to Later.agdaadditions to Lift.agdaConstructions on thin double cats via constructions on displayed cats