Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex 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 foundation 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 homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory 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 nforum nlab 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 sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorNima
   • CommentTimeSep 26th 2021
   • (edited Sep 26th 2021)
   • PermaLink
   Author: Nima
   Format: MarkdownItexI'm wondering if there's been a study of [unification](https://en.wikipedia.org/wiki/Unification_(computer_science)) and [anti-unification](https://en.wikipedia.org/wiki/Anti-unification_(computer_science)) 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]](https://hal.inria.fr/file/index/docid/765862/filename/main.pdf) [[2]](https://www.ri.cmu.edu/pub_files/pub2/lu_jianguo_1998_2/lu_jianguo_1998_2.pdf) 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 :\equiv \Sigma_{x:X} P(x) $ $ B :\equiv \Sigma_{x:X} Q(x) $ Our aim in anti-unification is to find a type $C$ that would unify with both $A$ and $B$ by means of variable substitution. If following the algorithm in [1], we'd first recognize that both $A$ and $B$ 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 $C$. However, the second argument is now an expression which is invoking two different predicates of type $X \rightarrow U$. In a traditional anti-unification algorithm, we would define a new variable that would be substituted with either $P(x)$ or $Q(x)$ when unifying $C$ with $A$ and $B$. Here however, there seems to be more than one option. Calling this new variable $y$, we could have $y:U$ or $y:X \rightarrow U$. There could even be more options if $P(x)$ and $Q(x)$ weren't of the same type. Let's assume $Q: Y \rightarrow U$. Then we could have $y: (X \rightarrow U) + (Y \rightarrow U)$. Even if making one of these choices, the formulation of $C$ eludes me. Do we write $C :\equiv \Sigma_{x:X} \Sigma_{f: X \rightarrow U} f(x)$, or $C :\equiv \Pi_{f: X \rightarrow U} \Sigma_{x:X} f(x)$, or something else? Any help or direction would be much appreciated!

   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 :\equiv \Sigma_{x:X} P(x)$

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

   Our aim in anti-unification is to find a type $C$ that would unify with both $A$ and $B$ by means of variable substitution. If following the algorithm in [1], we’d first recognize that both $A$ and $B$ 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 $C$. However, the second argument is now an expression which is invoking two different predicates of type $X \rightarrow U$. In a traditional anti-unification algorithm, we would define a new variable that would be substituted with either $P(x)$ or $Q(x)$ when unifying $C$ with $A$ and $B$.

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

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

2. • CommentRowNumber2.
   • CommentAuthorUlrik
   • CommentTimeSep 27th 2021
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexThere's a 1991 LICS paper by Frank Pfenning, [Unification and Anti-Unification in the Calculus of Constructions](https://www.cs.cmu.edu/~fp/papers/lics91.pdf), 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 \equiv \sum_{x:X}Y(x)$, where $Y : X \to U$ is a fresh variable.

   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 \equiv \sum_{x:X}Y(x)$, where $Y : X \to U$ is a fresh variable.

3. • CommentRowNumber3.
   • CommentAuthorNima
   • CommentTimeSep 28th 2021
   • PermaLink
   Author: Nima
   Format: MarkdownItexThanks Ulrik. I found that paper to be incomprehensible due to the unfamiliar notation, but I'll give it another go.

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