Topic: CoCalc injectivity
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.
Kevin Buzzard (Apr 18 2020 at 20:38):
´´´ (the one at the top)
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
b have type
Patrick Massot (Apr 18 2020 at 20:40):
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