Zulip Chat Archive

Stream: general

Topic: CoCalc injectivity


view this post on Zulip Emiel Lanckriet (Apr 18 2020 at 20:37):

I made the exercise about injectivity of compositions in CoCalc, first I tried:

intros a b,
intro hab,
apply hg,

But got the error:

invalid apply tactic, failed to unify
  a = b
with
  ?m_1 = ?m_2
state:
X Y Z : Type,
f : X  Y,
hf : injective f,
g : Y  Z,
hg : injective g,
a b : X,
hab : (g  f) a = (g  f) b
 a = b

Could someone tell why a=b cannot unify with ?m_1 = ?m_2.
I know this is wrong and the correct answer is first apply hf, but I just want to know why it doesn't unify.

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 20:38):

``` not ´´´ (the one at the top)

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 20:40):

It can't unify it because the conclusion of hg is that two terms of type Y are equal, but a and b have type X.

view this post on Zulip Patrick Massot (Apr 18 2020 at 20:40):

(deleted)

view this post on Zulip Emiel Lanckriet (Apr 18 2020 at 20:41):

Ah, ok, thanks, I hadn't thought that far. Thanks a lot.


Last updated: May 09 2021 at 19:11 UTC