proposition: Lemma hfiber_graph : (Σ x : bool, hfiber neg x) <~> Σ x : bool, neg_fib x.
proof: Proof. unshelve refine {| equiv_fun := fun h => (h.1, _) |}. red. destruct h as [res [arg Heq]]. exists arg. simpl. destruct Heq. auto. simpl. unshelve refine {| equiv_inv h := (h.1, _) |}. red. destruct h as [res [arg Heq]]. exists arg. simpl. induction Heq; reflexivity. red. - intros [x [res Hind]]. simpl. induction Hind using neg_graph_rect_dep; simpl; reflexivity. - intros [res [arg Heq]]. simpl. destruct Heq; simpl. apply path_sigma_uncurried. simpl. exists id_refl. simpl. apply path_sigma_uncurried. simpl. exists id_refl. simpl. destruct arg. simpl. reflexivity. simpl. reflexivity. - simpl. intros [res [arg Heq]]. destruct Heq. destruct arg. simpl. reflexivity. simpl. reflexivity. Qed.
imports: Equations.Type.All Examples.HoTT_light Relations