Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory kan lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology natural nforum nlab nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topological topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorNima
    • CommentTimeSep 26th 2021
    • (edited Sep 26th 2021)

    I’m wondering if there’s been a study of unification and anti-unification of HoTT types? Or even maybe depedent type theory? I’ve looked around but haven’t been able to find a good reference. I’ve found papers on anti-unification for other type systems, such as [1] [2] but not having much luck generalizing them to HoTT.

    Unification seems a bit more straightforward, but anti-unification (or least general generalization) of two types has flummoxed me. The problem is in introducing a variable to take the place of two types that are not equivalent and can no longer be split up. For example, take the following two types:

    A:Σ x:XP(x) A :\equiv \Sigma_{x:X} P(x)

    B:Σ x:XQ(x) B :\equiv \Sigma_{x:X} Q(x)

    Our aim in anti-unification is to find a type CC that would unify with both AA and BB by means of variable substitution. If following the algorithm in [1], we’d first recognize that both AA and BB use the same constructor (of the Sigma type), so we would drill down one level and attempt to anti-unify (or generalize) the two arguments. The first argument is the same for both, so we can copy that straight to CC. However, the second argument is now an expression which is invoking two different predicates of type XUX \rightarrow U. In a traditional anti-unification algorithm, we would define a new variable that would be substituted with either P(x)P(x) or Q(x)Q(x) when unifying CC with AA and BB.

    Here however, there seems to be more than one option. Calling this new variable yy, we could have y:Uy:U or y:XUy:X \rightarrow U. There could even be more options if P(x)P(x) and Q(x)Q(x) weren’t of the same type. Let’s assume Q:YUQ: Y \rightarrow U. Then we could have y:(XU)+(YU)y: (X \rightarrow U) + (Y \rightarrow U).

    Even if making one of these choices, the formulation of CC eludes me. Do we write C:Σ x:XΣ f:XUf(x)C :\equiv \Sigma_{x:X} \Sigma_{f: X \rightarrow U} f(x), or C:Π f:XUΣ x:Xf(x)C :\equiv \Pi_{f: X \rightarrow U} \Sigma_{x:X} f(x), or something else? Any help or direction would be much appreciated!

    • CommentRowNumber2.
    • CommentAuthorUlrik
    • CommentTimeSep 27th 2021

    There’s a 1991 LICS paper by Frank Pfenning, Unification and Anti-Unification in the Calculus of Constructions, which should be helpful. Anti-unification is in Sec. 5 with the discussion of binders on p. 8.

    I haven’t read the details, but my guess would be that we simply get C x:XY(x)C \equiv \sum_{x:X}Y(x), where Y:XUY : X \to U is a fresh variable.

    • CommentRowNumber3.
    • CommentAuthorNima
    • CommentTimeSep 27th 2021

    Thanks Ulrik. I found that paper to be incomprehensible due to the unfamiliar notation, but I’ll give it another go.