cmcma20 / cubical-mini Goto Github PK

Third time I think about path composition definition and find it biased. Can we do better? Yes, need to create an experimental branch, redefine composition with refl as top path and not as the left one. In the process of refactoring everything else we can uncover the subtleties in the new definition, maybe it doesn't work as good for unification or whatever, need to check this.

Also it would be nice to:

• consistently reorient all the n-cubes
• add some drawings for newcomers
• define Square rotations
• vertical/horizontal composition of squares

There's a clear hierarchy of n-ary functions, in order of increasing expressivity (and increasing complexity + unification-unfriendliness):

• Homogeneous non-dependent
  A -> A -> A -> ... -> R
  These were easy to use (see 7199c36), but too restrictive.
• Heterogeneous non-dependent
  A -> B -> C -> ... -> R
  Unusable without reflection, enough for basic tasks.
• Heterogeneous dependent
  (a : A) -> (b : B a) -> C a b -> ... -> R
  Deviously hard. See old drafts by Roman Kireev

The last point is also a prerequisite for generics.

Manual implementation would be useful too until we get generics

What's the intended usage? See the official docs and paper.
Need to experiment and find out whether the feature is usable.

Do we want to make levels abstract?

• HLevel , is-of-hlevel
  Probably not worth the hassle, as we frequently rely on computation for the latter.

There are cases where records were used just to ensure no unneccessary reduction takes place.

• n-Type and other structured types
  Refactoring this sound promising: we would define all these literally as sigmas/Type-with without record isomoprhism macros

Can we make all abstract definitions opaque instead? There aren't a lot of these, and they're all related either to hlevels or path algebra. Btw, making path algebra stuff abstract would be really nice as it's built from hcomps anyway.

Moving Erased to Correspondences was a mistake, lack of subtyping between erased and nonerased types is painful.
We need to get erased counterparts for all definitions in Foundations, that's a lot of work.

• erased is-of-hlevel should be defined with only one base case (contractibility), because is-prop is NOT equivalent to inductive case under erasure
• erased fibre
• all higher constructors in HITs must be erased (see truncations etc)
• isomorphism and equivalence with erased proofs is a must because we have plenty of stuff which is perfectly computable but uses univalence in proofs
• Dec with erased proof

Still need:

• universal property, closure, relationship with double negation
• stability
• effect instances (don't touch, wait for effect system)

Follow the original paper by Danielsson and the sequel, code here

• Π-compact types are called exhaustible here
• ∃-compact types are called omniscient₁ here
• Σ-compact types are what we lack now. It's a strong form of omniscience so should go somewhere near the corresponding module.

Instance's too inflexible, overlapping instances start to creep in algebraic structures. We need a macro which would banish overlap and allow extracting not only underling types from structured ones but also underlying functions (embeddings, surjections) etc.

Currently we have Meta.Witness and it's really bad from the point of UX: user is forced to separately define a Dec something then define something in another opaque block for it to be filled by witness! tactic. The tactic must not require such manipulations.

Investigate the cause of this behaviour and leave a comment. First hypothesis: the problem stems from a wacky implementation of Meta.Search tactics, which doesn't provide an easy way to granularly control reductions when composing search hints.

Second part is more subtle. It may be possible to reformulate Meta.Search.Decidable using n-ary Decidable predicate instead of Dec. I'll have no doubt the unifier's gonna choke on such a definition, but it's worth trying.

https://www.cs.bham.ac.uk/~mhe/TypeTopology/PathSequences.index.html seems like a piece of useful infrastructure

• infinity-magma
• n-magma
• semigroup
• 2-semigroup
• monoid
• commutative monoid
• 2-monoid
• group
• abelian group
• braided 2-monoid
• symmetric 2-monoid
• rig
• partially/naturally ordered rig
• ring
• commutative ring

This is a very vast topic, and needs a lot of further research. One thing is clear though \em no monad transformers and Haskell bullshit like MonadIO, MonadBase IO, MonadBaseControl IO etc.

Guess we'll need something based on interaction trees (hello, algebraic effects). If you love history, read this dusty paper. Hefty algebras are cutting edge level, but I'm afraid they might be too hefty for a minimal library.

Guillaume implemented IO for agda-stdlib, this is what we use now, but it's based on old coinduction. Can we do something like this but with later modality?