pullback and fibres

Let be a category with terminal object,

a pullback and element such that ,i.e.

commutes.

Then the pullback square induces an isomorphism on fibres

follows from:

• glueing lemma for pullbacks / Window Lemma for pullbacks
  

where the morphism is precisely the morphism induced by universal property unique up to unique isomorphism