1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
Set Warnings "-notation-overridden".
Require Import Equations.Type.All.
Require Import Examples.HoTT_light.
Set Universe Polymorphism.
Require Import Relations.
Import Id_Notations.
Import Sigma_Notations.
Derive Signature for Id.
Equations neg (b : bool) : bool :=
neg true := false; neg false := true.
Definition neg_fib (x : bool) := Σ a : bool, neg_graph a x.
#[local] Hint Resolve neg_graph_correct : core.
Definition neg_graph_rec := neg_graph_rect.
Scheme neg_graph_rect_dep := Induction for neg_graph Sort Type.
Lemma hfiber_graph : (Σ x : bool, hfiber neg x) <~> Σ x : bool, neg_fib x.
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.
|
