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.028Aug23221584128Jul25201811325Jun2085432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861"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 catsadd monad-assoc to Liftupdate LaterPropertiesupdate PosetWithPtbmodify posetModel and PosetSemanticsadd new file: PosetWithPtbAddition to monotone combinatorsUpdates to lock-step error ordering fileAdditions to Common.agdaUpdates to monotone relationsInit abstract modelNew formulation of Dyn as a PosetInit poset modeladditions to thin double catBegin formalizing thin double categoriesUpdates to monotone-related filesAdditions to Common.agdaBegin concrete poset semanticsMore poset stuffMonotone stuffDyn as a PosetLock step error orderingMore properties of laterExtensional Surfish Syntax and Intensional Terms/Logicprove clocked relation associativity