# Can we bring unification results under cofibrations outside?

Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do we still get correct results? To put it more formally, when we do something like $$\Gamma,\varphi \vdash ~?\equiv v:A$$ where $$?$$ is a metavariable generated during type checking outside of $$\varphi$$, and $$v$$ is a well-typed term of type $$A$$. Can we solve $$?$$ to $$v$$ and bring the solution to the place where it is generated, which does not have $$\varphi$$ in the context?

• I am not sure I understand what you're talking about, but perhaps you're asking whether weakening is valid in your setup. Sep 17 at 19:58
• In what sense is this a question about cubical type theory, rather than simple/dependent type theory?
– Couchy
Sep 19 at 2:48
• @Couchy ordinary type theory does not have judgments under a cofibration. Sep 19 at 4:48
• I am not an expert in cubical stuff, but if I understand correctly, you run the risk of a non-unique solution: what if ? should have a value which is more general than v, but collapses to v in the particular φ you are looking at? The analogy I have in mind is when you generate a predicate ?P as the return type of a dependent if. In the true branch, you can try and instantiate ?P with the type inferred for the branch, but doing this you force ?P to be constant, and might get a spurious error in the false branch… Sep 19 at 12:03
• And also, as @Andrej remarked, is it possible that you v only makes sense in φ? If this is the case, then the metavariable which should make sense outside of φ cannot possibly be instantiated with v. Although I would rather call this a failure of strengthening (removing bits of the context), rather than weakening (extending the context). Sep 19 at 12:06