Timings for Nat.v
(* -*- mode: coq; mode: visual-line -*- *)
(** * Defining the natural numbers from univalence and propresizing. *)
Require Import PropResizing.PropResizing.
Local Open Scope path_scope.
(* Be careful about [Import]ing this file! Usually you want to use the standard [Nat] instead. *)
(** Using propositional resizing and univalence, we can construct the natural numbers rather than defining them as an inductive type. In concrete practice there is no reason we would want to do this, but semantically it means that an elementary (oo,1)-topos (unlike an elementary 1-topos) automatically has a natural numbers object. *)
Context {UA:Univalence} {PR:PropResizing}.
(** The basic idea is that since the universe is closed under coproducts, it is already "infinite", so we can find the "smallest infininte set" N inside it. To get rid of the automorphisms in the universe coming from univalence and make N a set, instead of the universe of types we consider graphs (we could use posets or many other things too; in fact the graphs we are interested in will be posets). *)
(** Here is the readable definition of [Graph]:
> Definition Graph := { V : Type & { E : V -> V -> Type & forall x y, IsHProp@{hp} (E x y) }}.
However, to enable performance speedups by controlling universes, we write out its universe parameters explicitly, making it less readable. Moreover, since here we will eventually only be interested in those graphs that represent natural numbers, it does no harm to fix these universes at the outset throughout the entire development. *)
(** [s] : universe of the vertex and edge types
[u] : universe of the graph type, morally [s+1] *)
Definition Graph@{} := @sig@{u u} Type@{s} (fun V => @sig@{u u} (V -> V -> Type@{s}) (fun E => forall x y, IsHProp (E x y))).
(** We also write out its constructors and fields explicitly to control their universes. *)
Definition Build_Graph@{} (vert : Type@{s}) (edge : vert -> vert -> Type@{s})
(ishprop_edge : forall x y, IsHProp (edge x y))
: Graph
:= @exist@{u u} Type@{s} (fun V => @sig@{u u} (V -> V -> Type@{s}) (fun E => forall x y, IsHProp (E x y)))
vert
(@exist@{u u} (vert -> vert -> Type@{s}) (fun E => forall x y, IsHProp (E x y))
edge ishprop_edge).
Definition vert@{} : Graph -> Type@{s} := pr1.
Definition edge@{} (A : Graph) : vert A -> vert A -> Type@{s} := pr1 (pr2 A).
Instance ishprop_edge@{} (A : Graph) (x y : vert A) : IsHProp (edge A x y)
:= pr2 (pr2 A) x y.
(** We will need universe annotations in a few more places, but not many. *)
Definition equiv_path_graph@{} (A B : Graph)
: { f : vert A <~> vert B &
forall x y, edge A x y <-> edge B (f x) (f y) }
<~> (A = B).
srefine (equiv_path_sigma _ A B oE _).
srefine (equiv_functor_sigma' (equiv_path_universe (vert A) (vert B)) _).
srefine (equiv_path_sigma_hprop _ _ oE _).
srefine (equiv_path_forall _ _ oE _).
srefine (equiv_functor_forall' (f^-1) _).
srefine (equiv_path_forall _ _ oE _).
srefine (equiv_functor_forall' (f^-1) _).
rewrite transport_arrow_toconst.
rewrite !transport_path_universe_V.
srefine (equiv_path_universe _ _ oE _).
srefine (equiv_equiv_iff_hprop _ _).
(** N will be the set of graphs generated by the empty graph as
"zero", and "adding a new top element" as "successor". *)
Definition graph_zero@{} : Graph
:= Build_Graph Empty
(fun x y => @Empty_rec@{u} Type@{s} x)
(fun x y => Empty_rec x).
Definition graph_succ@{} (A : Graph) : Graph.
srefine (Build_Graph (sum@{s s} (vert A) Unit) _ _).
cbn; intros [x|x] [y|y]; exact _.
(** The following lemmas about graphs will be used later on to prove
the Peano axioms about N. *)
Definition graph_succ_top@{} {A : Graph} (x : vert (graph_succ A))
: edge (graph_succ A) x (inr tt).
destruct x as [x|x]; exact tt.
Definition graph_succ_top_unique@{}
{A : Graph} (y : vert (graph_succ A))
(yt : forall x, edge (graph_succ A) x y)
: y = inr tt.
Definition graph_succ_not_top@{} {A : Graph} (x : vert A)
: ~(edge (graph_succ A) (inr tt) (inl x))
:= idmap.
Definition graph_succ_not_top_unique@{} {A : Graph} (x : vert (graph_succ A))
(xt : ~(edge (graph_succ A) (inr tt) x))
: is_inl x.
Section Graph_Succ_Equiv.
Context {A B : Graph} (f : vert (graph_succ A) <~> vert (graph_succ B))
(e : forall x y, edge (graph_succ A) x y <-> edge (graph_succ B) (f x) (f y)).
Definition graph_succ_equiv_inr@{} : f (inr tt) = inr tt.
apply (graph_succ_top_unique (f (inr tt))).
rewrite <- (eisretr f x).
apply (fst (e (f^-1 x) (inr tt))).
Local Definition Ha@{} : forall x, is_inl (f (inl x)).
apply graph_succ_not_top_unique.
rewrite <- (eisretr f (inr tt)).
apply (snd (e (f^-1 (inr tt)) (inl x))) in ed.
pose (finr := graph_succ_equiv_inr).
apply moveL_equiv_V in finr.
exact (graph_succ_not_top x ed).
(* Coq bug: without the [:Unit] annotation some floating universe appears. *)
Local Definition Hb@{} : forall x:Unit, is_inr (f (inr x)).
srefine (transport@{s Set} is_inr graph_succ_equiv_inr^ tt).
Definition graph_unsucc_equiv_vert@{} : vert A <~> vert B
:= equiv_unfunctor_sum_l@{s s s s s s Set Set Set Set}
f Ha Hb.
Definition graph_unsucc_equiv_edge@{} (x y : vert A)
: iff@{s s s} (edge A x y) (edge B (graph_unsucc_equiv_vert x) (graph_unsucc_equiv_vert y)).
pose (h := e (inl x) (inl y)).
rewrite <- (unfunctor_sum_l_beta f Ha x) in h.
rewrite <- (unfunctor_sum_l_beta f Ha y) in h.
Definition graph_succ_path_equiv@{} (A B : Graph)
: (A = B) <~> (graph_succ A = graph_succ B).
refine ((equiv_path_graph _ _) oE _).
refine (_ oE (equiv_path_graph _ _)^-1).
srefine (equiv_adjointify _ _ _ _).
destruct x as [x|x]; destruct y as [y|y]; cbn.
exists (graph_unsucc_equiv_vert f e).
exact (graph_unsucc_equiv_edge f e).
apply path_sigma_hprop; cbn.
apply path_equiv, path_arrow; intros [x|[]]; cbn.
apply unfunctor_sum_l_beta.
symmetry; apply graph_succ_equiv_inr, e.
apply path_sigma_hprop; cbn.
apply path_equiv, path_arrow; intros x; reflexivity.
Definition graph_unsucc_path@{} (A B : Graph)
: (graph_succ A = graph_succ B) -> A = B
:= (graph_succ_path_equiv A B)^-1.
(** Here is the impredicative definition of N, as the smallest
subtype of [Graph] containing [graph_zero] and closed under
[graph_succ]. *)
Definition in_N@{p} (n : Graph)
:= forall (P : Graph -> Type@{p}),
(forall A, IsHProp (P A))
-> P graph_zero
-> (forall A, P A -> P (graph_succ A))
-> P n.
Instance ishprop_in_N@{p sp} (n : Graph) : IsHProp@{sp} (in_N@{p} n).
(** [p] : universe of [N], morally [u+1] i.e. [s+2]. *)
Definition N@{} : Type@{p}
:= @sig@{u p} Graph in_N@{u}.
Definition path_N@{} (n m : N) : n.1 = m.1 -> n = m
:= path_sigma_hprop@{u p p} n m.
intros P PH P0 Ps; exact P0.
Definition succ@{} : N -> N.
(** First Peano axiom: successor is injective *)
Definition succ_inj@{} (n m : N) (p : succ n = succ m) : n = m.
apply ((graph_succ_path_equiv n.1 m.1)^-1).
(** A slightly more general version of the theorem that N is a set,
which will be useful later. *)
Lemma ishprop_path_graph_in_N@{} (A B : Graph) (Arec : in_N@{u} A) : IsHProp (A = B).
apply hprop_inhabited_contr; intros [].
apply contr_inhabited_hprop; try exact 1.
equiv_intro (equiv_path_graph graph_zero graph_zero) fe.
equiv_intro (equiv_path_graph graph_zero graph_zero) fe'.
apply equiv_ap; try exact _.
apply path_sigma_hprop, path_equiv@{s s s}, path_arrow.
refine (contr_equiv (B = B) (graph_succ_path_equiv B B)).
Instance ishprop_path_N@{} (n : N) (A : Graph) : IsHProp (n.1 = A).
apply ishprop_path_graph_in_N, pr2.
Instance ishset_N@{} : IsHSet N.
change (IsHProp (n = m)).
refine (istrunc_equiv_istrunc (n.1 = m.1) (equiv_path_sigma_hprop n m)).
Definition graph_zero_neq_succ@{} {A : Graph}
: graph_zero <> graph_succ A.
destruct ((equiv_path_graph graph_zero (graph_succ A))^-1 p) as [f e].
(** Second Peano axiom: zero is not a successor *)
Definition zero_neq_succ@{} (n : N) : zero <> succ n.
intros p; apply pr1_path in p; refine (graph_zero_neq_succ p).
(** This tweak is sometimes necessary to avoid universe inconsistency.
It's how the impredicativity of propositional resizing enters. *)
Definition resize_nrec@{p0 p1} (n : Graph) (nrec : in_N@{p0} n)
: in_N@{p1} n.
srefine ((equiv_resize_hprop (P' n))^-1
(nrec (fun A => resize_hprop (P' A)) _ _ _));
try exact _; cbn.
exact (equiv_resize_hprop (P' graph_zero) P0').
exact (equiv_resize_hprop (P' (graph_succ A))
(Ps' A ((equiv_resize_hprop (P' A))^-1 P'A))).
Local Instance ishprop_graph_zero_or_succ@{} : forall n : Graph,
IsHProp ((n = graph_zero) + { m : N & n = graph_succ m.1 }).
apply ishprop_sum@{u p p}.
apply (@istrunc_equiv_istrunc _ _ (equiv_path_inverse _ _)),ishprop_path_graph_in_N.
apply @ishprop_sigma_disjoint.
intros m;apply (@istrunc_equiv_istrunc _ _ (equiv_path_inverse _ _)).
apply ishprop_path_graph_in_N.
apply zero_neq_succ with m, path_N.
Local Instance ishprop_N_zero_or_succ@{} : forall n : N,
IsHProp ((n = zero) + { m : N & n = succ m }).
apply ishprop_sigma_disjoint.
apply succ_inj;path_via n.
apply zero_neq_succ with m.
Definition N_zero_or_succ@{} (n : N)
: (n = zero) + { m : N & n = succ m }.
apply (functor_sum (path_N _ _)
(functor_sigma (Q := fun m:N => n = succ m) idmap (fun m => path_N _ (succ m)))).
destruct n as [n nrec]; cbn.
srefine (resize_nrec n nrec
(fun n => (n = graph_zero) +
{m : N & n = graph_succ m.1}) _ _ _); cbn.
intros A [A0|[m As]]; apply inr.
Definition pred_in_N@{} (n : Graph) (snrec : in_N@{u} (graph_succ n))
: in_N@{u} n.
destruct (N_zero_or_succ (graph_succ n ; snrec)) as [H0|[m Hs]].
apply pr1_path in H0; cbn in H0.
destruct (graph_zero_neq_succ H0^).
apply graph_unsucc_path in Hs.
apply (transport@{u p} in_N Hs^).
(** Final Peano axiom: induction. Importantly, the universe of the motive [P] is not constrained but can be arbitrary. *)
Definition N_propind@{P} (P : N -> Type@{P}) `{forall n, IsHProp (P n)}
(P0 : P zero) (Ps : forall n, P n -> P (succ n))
: forall n, P n.
pose (Q := fun m:Graph => forall (mrec : in_N m), P (m;mrec)).
(* The try clause below is only needed for Coq <= 8.11 *)
refine (resize_nrec n nrec Q _ _ _ nrec);clear n nrec; try (intros A; apply trunc_forall).
refine (transport P _ P0).
pose (m := (A ; pred_in_N A Asrec) : N).
refine (transport P _ (Ps m (QA (pred_in_N A Asrec)))).
apply path_N; reflexivity.
(** Sometimes we just need a bigger fish. *)
(** A first application *)
Definition N_neq_succ@{} (n : N) : n <> succ n.
revert n; apply N_propind@{p}.
intros n;exact istrunc_arrow@{p p p}.
exact (succ_inj n (succ n) e).
(** Now we want to use induction to define recursion. The basic
idea is the same as always: define partial attempts and show by
induction that they are uniquely defined. But we have to be careful
to phrase it in a way that works without assuming any truncation
restritions on the codomain.
First we need inequality on N, which we define in terms of addition.
Normally addition is defined *using* recursion, but here we can
"cheat" because we know how to add graphs, and then prove that it
satisfies the recursive equations for addition. *)
Definition graph_add@{} (A B : Graph) : Graph.
exists (vert A + vert B).
exists (fun ab ab' =>
match ab, ab' return Type@{s} with
| inl a, inl a' => edge A a a'
| inl a, inr b => Unit
| inr b, inl a => Empty
| inr b, inr b' => edge B b b'
end).
intros [a|b] [a'|b']; exact _.
Definition graph_add_zero_r@{} (A : Graph) : graph_add A graph_zero = A.
exists (sum_empty_r (vert A)).
apply iff_reflexive@{u s}.
Definition graph_add_zero_l@{} (A : Graph) : graph_add graph_zero A = A.
exists (sum_empty_l (vert A)).
apply iff_reflexive@{u s}.
Definition graph_add_succ@{} (A B : Graph)
: graph_add A (graph_succ B) = graph_succ (graph_add A B).
exists (equiv_inverse (equiv_sum_assoc (vert A) (vert B) Unit)).
intros [x|[x|[]]] [y|[y|[]]];apply iff_reflexive@{u s}.
Definition graph_add_assoc@{} (A B C : Graph)
: graph_add (graph_add A B) C = graph_add A (graph_add B C).
exists (equiv_sum_assoc _ _ _).
intros [[x|x]|x] [[y|y]|y]; apply iff_reflexive@{u s}.
Definition graph_one@{} : Graph
:= Build_Graph Unit (fun _ _ : Unit => Unit) _.
Definition graph_add_one_succ@{} (A : Graph)
: graph_add A graph_one = graph_succ A.
intros [x|[]] [y|[]]; apply iff_reflexive@{u s}.
Definition graph_succ_zero@{} : graph_succ graph_zero = graph_one.
rewrite <- graph_add_one_succ.
rewrite <- graph_succ_zero.
Definition N_add@{} (n m : N) : N.
exists (graph_add n.1 m.1).
apply (transport P (graph_add_zero_r n.1)^).
apply (transport P (graph_add_succ n.1 A)^).
Notation "n + m" := (N_add n m).
Definition N_add_zero_l@{} (n : N) : zero + n = n.
apply path_N, graph_add_zero_l.
Definition N_add_zero_r@{} (n : N) : n + zero = n.
apply path_N, graph_add_zero_r.
Definition N_add_succ@{} (n m : N) : n + succ m = succ (n + m).
apply path_N, graph_add_succ.
Definition N_add_assoc@{} (n m k : N) : (n + m) + k = n + (m + k).
apply path_N, graph_add_assoc.
Definition N_add_cancel_r@{} (n m k : N) (H : n + k = m + k)
: n = m.
refine (N_propind _ _ _).
intros H; rewrite !N_add_zero_r in H; exact H.
rewrite !N_add_succ in H2.
Definition N_add_cancel_zero_r@{} (n k : N) (H : k + n = n)
: k = zero.
refine (N_add_cancel_r k zero n _).
apply path_N, graph_add_zero_l.
Definition N_add_one_r@{} (n : N) : n + one = succ n.
apply graph_add_one_succ.
Definition N_add_one_l@{} (n : N) : one + n = succ n.
revert n; refine (N_propind (fun m => one + m = succ m) _ _).
symmetry; apply graph_succ_zero.
Definition N_add_succ_l@{} (n m : N) : succ n + m = succ (n + m).
rewrite <- (N_add_one_r n).
(** Now we define inequality in terms of addition. *)
Definition N_le@{} (n m : N) : Type@{p}
:= { k : N & k + n = m }.
Notation "n <= m" := (N_le n m).
Local Instance ishprop_N_le@{} n m : IsHProp (n <= m).
apply ishprop_sigma_disjoint.
apply N_add_cancel_r with n.
Definition N_zero_le@{} (n : N) : zero <= n.
Definition N_le_zero@{} (n : N) (H : n <= zero) : n = zero.
apply ((equiv_path_graph _ _)^-1), pr1 in H.
pose proof ((fun x => H (inr x)) : (vert n.1) -> Empty) as f.
apply path_N, equiv_path_graph.
srefine ((Build_Equiv _ _ f _);_); cbn.
intros x y; destruct (f x).
Instance contr_le_zero@{} : Contr {n:N & n <= zero}.
apply (Build_Contr _ (exist (fun n => n <= zero) zero (N_zero_le zero))).
Instance reflexive_N_le@{} : Reflexive N_le.
Definition N_lt@{} (n m : N) : Type@{p}
:= { k : N & (succ k) + n = m }.
Notation "n < m" := (N_lt n m).
Lemma ishprop_N_lt@{} n m : IsHProp (n < m).
apply ishprop_sigma_disjoint.
apply N_add_cancel_r with (succ n).
rewrite !N_add_succ, <-!N_add_succ_l.
Local Existing Instance ishprop_N_lt.
Definition N_lt_zero@{} (n : N) : ~(n < zero).
unfold N_lt; intros [k H].
apply pr1_path, (equiv_path_graph _ _)^-1, pr1 in H.
exact (H (inl (inr tt))).
Definition N_lt_irref@{} (n : N) : ~(n < n).
revert n; apply N_propind@{p}.
intros n;exact istrunc_arrow@{p p p}.
apply succ_inj; assumption.
Definition N_le_eq_or_lt@{} (n m : N) (H : n <= m)
: (n = m) + (n < m).
assert (HP : IsHProp ((n = m) + (n < m))).
apply ishprop_sum; try exact _.
apply N_add_cancel_zero_r in K.
symmetry in K; apply zero_neq_succ in K; assumption.
destruct (N_zero_or_succ k) as [k0|[l L]].
rewrite (N_add_zero_l n) in K.
Definition N_succ_nlt@{} (n : N) : ~(succ n < n).
revert n; apply N_propind@{p}.
intros n;exact istrunc_arrow@{p p p}.
Definition N_lt_succ@{} (n : N) : n < succ n.
Definition N_succ_lt@{} (n m : N) (H : n < m) : succ n < succ m.
Definition N_lt_le@{} (n m : N) (H : n < m) : n <= m.
Definition N_lt_iff_succ_le@{} (n m : N) :
(n < m) <-> (succ n <= m).
split; intros [k H]; exists k.
rewrite N_add_succ, <- N_add_succ_l.
rewrite N_add_succ_l, <- N_add_succ.
Definition N_lt_succ_iff_le@{} (n m : N) : (n < succ m) <-> (n <= m).
split; intros [k H]; exists k.
rewrite N_add_succ_l in H.
rewrite N_add_succ_l; apply ap, H.
Definition equiv_N_segment@{} (n : N)
: { m : N & m <= n } <~> (sum@{p p} {m : N & m < n} Unit).
srefine (equiv_adjointify _ _ _ _).
destruct (N_le_eq_or_lt mH.1 n mH.2) as [H0|Hs].
exact (mH.1; N_lt_le mH.1 n mH.2).
abstract (intros [[m H]|[]]; cbn;
[ generalize (N_le_eq_or_lt m n (N_lt_le m n H));
intros [H0|Hs]; cbn;
[ apply Empty_rec;
rewrite H0 in H; exact (N_lt_irref n H)
| apply ap, ap, path_ishprop ]
| generalize (N_le_eq_or_lt n n (reflexive_N_le n));
intros [H0|Hs];
[ reflexivity
| apply Empty_rec;
exact (N_lt_irref n Hs) ]]).
abstract (intros [m H]; cbn;
generalize (N_le_eq_or_lt m n H);
intros [H0|Hs]; cbn;
[ apply path_sigma_hprop;
symmetry; assumption
| apply ap, path_ishprop ]).
Definition equiv_N_segment_succ@{} (n : N)
: { m : N & m <= succ n } <~> @sum@{p p} {m : N & m <= n} Unit.
refine (_ oE equiv_N_segment (succ n)).
apply equiv_functor_sum_r.
apply equiv_functor_sigma_id.
intros m; apply equiv_iff_hprop_uncurried, N_lt_succ_iff_le.
(** A fancy name for [1] so that we can [rewrite] with it later. *)
Definition equiv_N_segment_succ_inv_inl@{} (n : N) (mh : {m:N & m <= n})
: ((equiv_N_segment_succ n)^-1 (inl mh)).1 = mh.1.
Definition equiv_N_segment_lt_succ@{} (n : N)
: { m : N & m < succ n } <~> {m : N & m <= n}.
apply equiv_functor_sigma_id.
intros; apply equiv_iff_hprop; apply N_lt_succ_iff_le.
Definition zero_seg@{} (n : N) : { m : N & m <= n }
:= (zero ; N_zero_le n).
Definition succ_seg@{} (n : N)
: { m : N & m < n } -> { m : N & m <= n }
:= fun mh =>
let (m,H) := mh in
(succ m; fst (N_lt_iff_succ_le m n) H).
Definition refl_seg@{} (n : N) : {m : N & m <= n}.
(** Now we're finally ready to prove recursion. *)
(** Here is the type we will recurse into. Importantly, it doesn't have to be a set! *)
(** [nr] is the universe of [partial_Nrec], morally [max(p,x)]. Note that it shouldn't be [large], see constraints on [contr_partial_Nrec_zero]. *)
Context (X : Type@{x}) (x0 : X) (xs : X -> X).
(** The type of partially defined recursive functions "up to [n]". *)
Local Definition partial_Nrec@{} (n : N) : Type@{nr}
:= sig@{nr nr}
(fun f : ({ m : N & m <= n} -> X) =>
prod@{x nr} (f (zero_seg n) = x0)
(forall (mh : {m:N & m < n}),
f (succ_seg n mh) = xs (f ((equiv_N_segment n)^-1 (inl mh))))).
(** The crucial point that makes it work for arbitrary [X] is to
prove in one big induction that these types are always
contractible. Here is the base case. *)
Lemma contr_partial_Nrec_zero@{} : Contr (partial_Nrec zero).
srefine (istrunc_equiv_istrunc {f0 : {f : {m : N & m <= zero} -> X &
(f (zero_seg zero) = x0)} &
(forall mh : {m : N & m < zero},
f0.1 (succ_seg zero mh) =
xs (f0.1 ((equiv_N_segment zero)^-1 (inl mh))))} _).
refine (_ oE equiv_inverse (equiv_sigma_assoc _ _)).
apply equiv_functor_sigma_id; intros f.
cbn; apply equiv_sigma_prod0.
refine (@istrunc_sigma@{nr nr large nr} _ _ _ _ _).
srefine (Build_Contr _ _ _).
exists (fun _ => x0); reflexivity.
srefine (path_sigma _ _ _ _ _); cbn.
apply path_forall; intros m.
exact (H^ @ ap g (path_ishprop _ _)).
rewrite transport_paths_Fl.
rewrite ap10_path_forall.
rewrite inv_pp, inv_V, concat_p1.
transitivity ((ap g 1)^ @ H).
apply (Build_Contr _ (fun mh => Empty_rec (N_lt_zero mh.1 mh.2))).
apply path_forall; intros m.
destruct (N_lt_zero m.1 m.2).
Local Existing Instance contr_partial_Nrec_zero.
Local Definition equiv_N_segment_succ_maps@{} (n : N)
: Equiv@{nr nr} (prod@{nr x} ({ m : N & m <= n} -> X) X) ({ m : N & m <= succ n} -> X).
refine (_ oE @equiv_sum_ind@{x nr nr nr nr p p p}
_ {m:N&m<=n} Unit (fun _ => X) oE _).
apply equiv_N_segment_succ.
apply equiv_functor_prod_l.
apply equiv_unit_rec@{x nr}.
Local Definition equiv_seg_succ@{} (n m : N) (H : m < succ n)
(f : { m : N & m <= n} -> X) (xsn : X)
: equiv_N_segment_succ_maps n (f,xsn) (m ; N_lt_le m _ H) = f (exist (fun m=>m<=n) m (fst (N_lt_succ_iff_le m _) H)).
generalize (N_le_eq_or_lt m (succ n) (N_lt_le m (succ n) H)).
apply ap, path_sigma_hprop; reflexivity.
(** And here, essentially, is the inductive step. *)
Local Definition partial_Nrec_succ0 (n : N)
: partial_Nrec n <~> partial_Nrec (succ n).
srefine (equiv_functor_sigma' (equiv_N_segment_succ_maps n) _ oE _).
srefine ((f (zero_seg n) = x0) *
((forall (mh : {m:N & m < n}),
f (succ_seg n mh) = xs (f ((equiv_N_segment n)^-1 (inl mh)))) *
(xsn = xs (f (refl_seg n))))).
apply equiv_functor_prod'.
generalize (N_le_eq_or_lt zero (succ n) (N_zero_le (succ n))).
destruct (zero_neq_succ n (H0)).
apply path_sigma_hprop; reflexivity.
srefine ((equiv_functor_forall_pb
(equiv_N_segment_lt_succ n)^-1)^-1 oE _).
srefine ((equiv_functor_forall_pb (equiv_N_segment n)^-1)^-1 oE _).
srefine (equiv_sum_ind _ oE _).
apply equiv_functor_prod'.
apply equiv_functor_forall_id; intros [m H].
transitivity ((equiv_N_segment_succ_maps n)
(f,xsn)
(succ m; N_lt_le _ _ (N_succ_lt m n H))).
apply ap, path_sigma_hprop; reflexivity.
cbv [equiv_fun equiv_inv equiv_isequiv equiv_inverse equiv_adjointify isequiv_adjointify equiv_compose' equiv_compose equiv_precompose' equiv_functor_sigma_id equiv_N_segment_succ equiv_sum_ind equiv_functor_prod_l equiv_functor_sum_r equiv_functor_sigma' equiv_functor_sum equiv_functor_sum' equiv_functor_sigma equiv_functor_prod equiv_functor_prod' equiv_idmap isequiv_idmap equiv_unit_rec isequiv_functor_sigma equiv_iff_hprop equiv_iff_hprop_uncurried eisretr inverse transport succ_seg equiv_N_segment_succ_maps equiv_N_segment_lt_succ equiv_N_segment];
cbn.
match goal with
| [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
end.
apply Empty_rec; rewrite L in H.
apply ap, path_sigma_hprop; reflexivity.
refine ((equiv_contr_forall _)^-1 oE _).
match goal with
| [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
end.
cbv [eisretr equiv_adjointify equiv_compose equiv_compose' equiv_fun equiv_functor_prod equiv_functor_prod' equiv_functor_prod_l equiv_functor_sigma equiv_functor_sigma' equiv_functor_sigma_id equiv_functor_sum equiv_functor_sum' equiv_functor_sum_r equiv_idmap equiv_iff_hprop equiv_iff_hprop_uncurried equiv_inv equiv_inverse equiv_isequiv equiv_N_segment equiv_N_segment_lt_succ equiv_N_segment_succ equiv_N_segment_succ_maps equiv_precompose' equiv_sum_ind equiv_unit_rec inverse isequiv_adjointify isequiv_functor_sigma isequiv_idmap transport];
cbn [fst snd pr1 pr2 functor_sigma].
match goal with
| [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
end.
apply ap, path_sigma_hprop.
refine (equiv_sigma_prod _ oE _).
apply equiv_functor_sigma_id.
refine (equiv_functor_sigma_id (fun b:X => equiv_sigma_prod0 _ _) oE _).
refine (equiv_sigma_symm _ oE _).
refine (_ oE (equiv_sigma_prod0 _ _)^-1).
apply equiv_functor_sigma_id; intros f0.
refine (equiv_functor_sigma_id (fun b:X => equiv_sigma_prod0 _ _) oE _).
refine (equiv_sigma_symm _ oE _).
exact ((equiv_sigma_contr _)^-1%equiv).
Local Definition partial_Nrec_succ@{}
:= Eval unfold partial_Nrec_succ0
in partial_Nrec_succ0@{nr nr}.
Local Instance contr_partial_Nrec@{} (n : N) : Contr (partial_Nrec n).
revert n; apply N_propind; try exact _.
refine (istrunc_equiv_istrunc _ (partial_Nrec_succ n)).
(** This will be useful later. *)
Local Definition partial_Nrec_restr@{} (n : N)
: partial_Nrec (succ n) -> partial_Nrec n.
destruct f as [f [f0 fs]].
exists (fun mh => f ((equiv_N_segment_succ n)^-1 (inl mh))).
apply ap, path_sigma_hprop.
refine (_ @ fs (((equiv_N_segment_lt_succ n)^-1)
((equiv_N_segment n)^-1 (inl mh))) @ _).
apply path_sigma_hprop; reflexivity.
apply path_sigma_hprop; reflexivity.
(** Finally, we want to put all this together to show that the
type of fully defined recursive functions is contractible, so that
N has the universal property of a natural numbers object. If we
attack it directly, this can lead to quite annoying path algebra.
Instead, we will show that it is a retract of the product of all
the types of partial attempts, which is contractible since each of
them is. *)
Local Definition partials@{} := forall n, partial_Nrec n.
Local Instance contr_partials@{} : Contr partials := istrunc_forall@{p nr nr}.
(** From a family of partial attempts, we get a totally defined
recursive function. *)
Local Definition N_rec'@{} : N -> X
:= fun n => (pf n).1 (refl_seg n).
Definition N_rec_beta_zero'@{} : N_rec' zero = x0.
refine (_ @ fst (pf zero).2).
apply ap, path_sigma_hprop; reflexivity.
Definition N_rec_beta_succ'@{} (n : N)
: N_rec' (succ n) = xs (N_rec' n).
refine (_ @ snd (pf (succ n)).2
(n ; N_lt_succ n) @ _).
apply ap, path_sigma_hprop; reflexivity.
transitivity ((partial_Nrec_restr n (pf (succ n))).1 (refl_seg n)).
refine (ap (pf (succ n)).1 _).
apply path_sigma_hprop; reflexivity.
(** Applying this to the "canonical" partial attempts, we get "the recursor". *)
Definition N_rec@{} : N -> X := N_rec' (center partials).
Definition N_rec_beta_zero@{} : N_rec zero = x0
:= N_rec_beta_zero' (center partials).
Definition N_rec_beta_succ@{} (n : N)
: N_rec (succ n) = xs (N_rec n)
:= N_rec_beta_succ' (center partials) n.
(** Here is the type of totally defined recursive functions that
we want to prove to be contractible. *)
Definition NRec : Type@{nr}
:= sig@{nr nr} (fun f : N -> X =>
prod@{x nr} (f zero = x0)
(forall m:N, f (succ m) = xs (f m))).
Local Definition nrec_partials@{} : NRec -> partials.
exists (fun mh => f.1 mh.1).
(** This is a weird lemma. We could prove it by [path_contr], but
we give an explicit proof instead using [path_sigma], so that
later on we know what happens when [pr1_path] is applied to it. *)
Local Definition nrec_partials_succ@{} (n : N) (f : NRec)
: partial_Nrec_restr n (nrec_partials f (succ n)) = nrec_partials f n.
change (?x = ?y) with ((x.1; x.2) = (y.1; y.2)).
srefine (path_sigma'@{nr nr nr} _ 1 _).
abstract (rewrite transport_1;
apply path_prod;
[ cbn [partial_Nrec_restr nrec_partials fst pr2 pr1];
rewrite ap_compose;
rewrite ap_pr1_path_sigma_hprop;
apply concat_1p
| cbn [partial_Nrec_restr nrec_partials pr1 pr2 snd];
apply path_forall; intros mh;
rewrite ap_compose;
rewrite ap_pr1_path_sigma_hprop;
rewrite ap_1, concat_1p;
refine (_ @ concat_p1 _); apply whiskerL;
refine (_ @ ap_1 _ xs); apply ap;
rewrite ap_compose;
rewrite ap_pr1_path_sigma_hprop;
reflexivity ]).
Local Definition partials_nrec@{} : partials -> NRec.
exact (N_rec_beta_zero' pf, N_rec_beta_succ' pf).
Local Definition nrec_partials_sect@{} (f : NRec)
: partials_nrec (nrec_partials f) = f.
destruct f as [f [f0 fs]].
unfold partials_nrec, nrec_partials.
unfold N_rec', N_rec_beta_zero'; cbn.
apply ap@{nr nr}, path_prod.
rewrite ap_pr1_path_sigma_hprop.
apply path_forall; intros n.
cbn [fst snd pr1 pr2];
cbv [equiv_fun equiv_inverse equiv_inv equiv_isequiv equiv_compose' equiv_compose isequiv_compose equiv_functor_sum_r equiv_functor_sigma_id equiv_functor_sigma' equiv_functor_sigma equiv_functor_sum' equiv_functor_sum equiv_adjointify isequiv_adjointify isequiv_functor_sum isequiv_idmap equiv_idmap isequiv_functor_sigma equiv_iff_hprop_uncurried functor_sum functor_sigma equiv_N_segment equiv_N_segment_succ inverse transport eisretr];
cbn [fst snd pr1 pr2 refl_seg].
rewrite ap_pr1_path_sigma_hprop.
rewrite (ap_compose pr1 f).
rewrite ap_pr1_path_sigma_hprop.
refine (_ @ (concat_p1 _)); apply whiskerL.
set (refl_seg_n := refl_seg n).
(** Here is where we use [nrec_partials_succ]: the [path_contr] equal to it, which allows us to identify [ap pr1] of the latter. (Note that [ap pr1] of a [path_contr] can be nontrivial even when the endpoints happen to coincide judgmentally, for instance (x;p) and (x;1) in {y:X & y = x}, so there really is something to prove here.) *)
transitivity (ap xs (ap10 (ap pr1 (nrec_partials_succ n (f;(f0,fs)))) refl_seg_n)).
assert (p : path_contr _ _ = nrec_partials_succ n (f; (f0, fs))).
exact (ap (fun h => ap10 (ap pr1 h) refl_seg_n) p).
unfold nrec_partials_succ.
rewrite ap_pr1_path_sigma.
Global Instance contr_NRec@{} : Contr NRec.
refine (istrunc_isequiv_istrunc partials partials_nrec).
refine (isequiv_adjointify _ nrec_partials nrec_partials_sect _).
intros x; apply path_contr.