Library Exercise_2_6_1_5


Require Import Setoid Utf8.

Lemma fiber_is_relation X B (f : XB) : Equivalence (λ x y, f x = f y).
  split; repeat intro; simpl;
  repeat match goal with
           | [ H : context[f _] |- _ ] ⇒ revert H
           | [ |- context[f ?x] ] ⇒ generalize (f x); intro
         end;
  intros; subst; reflexivity.
Qed.