(** * Defining the natural numbers from univalence and propositional resizing. *)
Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import HProp.
Require Import Universes.Smallness.
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. *)

Section AssumeStuff.
  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 infinite 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] *)
  Universes s u.

  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).
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} <~>
A = B
  Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} <~>
A = B
    srefine (equiv_path_sigma _ A B oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} <~>
{p : A.1 = B.1 &
transport
  (fun V : Type =>
   {E : V -> V -> Type & is_mere_relation V E}) p A.2 =
B.2}
    srefine (equiv_functor_sigma' (equiv_path_universe (vert A) (vert B)) _).
UA: Univalence
PR: PropResizing
A, B: Graph
forall a : vert A <~> vert B,
(fun f : vert A <~> vert B =>
 forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) a <~>
(fun p : A.1 = B.1 =>
 transport
   (fun V : Type =>
    {E : V -> V -> Type & is_mere_relation V E}) p A.2 =
 B.2) (equiv_path_universe (vert A) (vert B) a)
    intros f; cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
(forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) <~>
transport
  (fun V : Type =>
   {E : V -> V -> Type & is_mere_relation V E})
  (path_universe_uncurried f) A.2 = B.2
    rewrite transport_sigma.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
(forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) <~>
(transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1;
transportD (fun x : Type => x -> x -> Type)
  (fun (x : Type) (y : x -> x -> Type) =>
   is_mere_relation x y) (path_universe_uncurried f)
  (A.2).1 (A.2).2) = B.2
    srefine (equiv_path_sigma_hprop _ _ oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
(forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) <~>
(transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1;
transportD (fun x : Type => x -> x -> Type)
  (fun (x : Type) (y : x -> x -> Type) =>
   is_mere_relation x y) (path_universe_uncurried f)
  (A.2).1 (A.2).2).1 = (B.2).1 cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
(forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) <~>
transport (fun x : Type => x -> x -> Type)
  (path_universe_uncurried f) (A.2).1 = (B.2).1
    srefine (equiv_path_forall _ _ oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
(forall x y : vert A,
 edge A x y <-> edge B (f x) (f y)) <~>
transport (fun x : Type => x -> x -> Type)
  (path_universe_uncurried f) (A.2).1 == (B.2).1
    srefine (equiv_functor_forall' (f^-1) _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
forall b : vert B,
(fun a : vert A =>
 forall y : vert A, edge A a y <-> edge B (f a) (f y))
  (f^-1%equiv b) <~>
(fun b0 : vert B =>
 transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1 b0 = (B.2).1 b0)
  b
    intros x.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x: vert B
(fun a : vert A =>
 forall y : vert A, edge A a y <-> edge B (f a) (f y))
  (f^-1%equiv x) <~>
(fun b : vert B =>
 transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1 b = (B.2).1 b)
  x
    srefine (equiv_path_forall _ _ oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x: vert B
(forall y : vert A,
 edge A (f^-1%equiv x) y <->
 edge B (f (f^-1%equiv x)) (f y)) <~>
transport (fun x : Type => x -> x -> Type)
  (path_universe_uncurried f) (A.2).1 x == (B.2).1 x
    srefine (equiv_functor_forall' (f^-1) _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x: vert B
forall b : vert B,
(fun a : vert A =>
 edge A (f^-1%equiv x) a <->
 edge B (f (f^-1%equiv x)) (f a)) (f^-1%equiv b) <~>
(fun b0 : vert B =>
 transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1 x b0 =
 (B.2).1 x b0) b
    intros y.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(fun a : vert A =>
 edge A (f^-1%equiv x) a <->
 edge B (f (f^-1%equiv x)) (f a)) (f^-1%equiv y) <~>
(fun b : vert B =>
 transport (fun x : Type => x -> x -> Type)
   (path_universe_uncurried f) (A.2).1 x b =
 (B.2).1 x b) y cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <->
 edge B (f (f^-1 x)) (f (f^-1 y))) <~>
transport (fun x : Type => x -> x -> Type)
  (path_universe_uncurried f) (A.2).1 x y =
(B.2).1 x y
    rewrite transport_arrow.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <->
 edge B (f (f^-1 x)) (f (f^-1 y))) <~>
transport (fun x : Type => x -> Type)
  (path_universe_uncurried f)
  ((A.2).1
     (transport idmap (path_universe_uncurried f)^ x))
  y = (B.2).1 x y
    rewrite transport_arrow_toconst.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <->
 edge B (f (f^-1 x)) (f (f^-1 y))) <~>
(A.2).1
  (transport idmap (path_universe_uncurried f)^ x)
  (transport idmap (path_universe_uncurried f)^ y) =
(B.2).1 x y
    rewrite !transport_path_universe_V.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <->
 edge B (f (f^-1 x)) (f (f^-1 y))) <~>
(A.2).1 (f^-1 x) (f^-1 y) = (B.2).1 x y
    rewrite !eisretr.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <-> edge B x y) <~>
(A.2).1 (f^-1 x) (f^-1 y) = (B.2).1 x y
    srefine (equiv_path_universe _ _ oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
x, y: vert B
(edge A (f^-1 x) (f^-1 y) <-> edge B x y) <~>
((A.2).1 (f^-1 x) (f^-1 y) <~> (B.2).1 x y)
    srefine (equiv_equiv_iff_hprop _ _).
  Qed.

  (** 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.
UA: Univalence
PR: PropResizing
A: Graph
Graph
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
Graph
    srefine (Build_Graph (sum@{s s} (vert A) Unit) _ _).
UA: Univalence
PR: PropResizing
A: Graph
vert A + Unit -> vert A + Unit -> Type
UA: Univalence
PR: PropResizing
A: Graph
is_mere_relation (vert A + Unit) ?edge
    -
UA: Univalence
PR: PropResizing
A: Graph
vert A + Unit -> vert A + Unit -> Type intros [x|x] [y|y].
UA: Univalence
PR: PropResizing
A: Graph
x, y: vert A
Type
UA: Univalence
PR: PropResizing
A: Graph
x: vert A
y: Unit
Type
UA: Univalence
PR: PropResizing
A: Graph
x: Unit
y: vert A
Type
UA: Univalence
PR: PropResizing
A: Graph
x, y: Unit
Type
      +
UA: Univalence
PR: PropResizing
A: Graph
x, y: vert A
Type exact (edge A x y).
      +
UA: Univalence
PR: PropResizing
A: Graph
x: vert A
y: Unit
Type exact Unit.
      +
UA: Univalence
PR: PropResizing
A: Graph
x: Unit
y: vert A
Type exact Empty.
      +
UA: Univalence
PR: PropResizing
A: Graph
x, y: Unit
Type exact Unit.
    -
UA: Univalence
PR: PropResizing
A: Graph
is_mere_relation (vert A + Unit)
  (fun X : vert A + Unit =>
   match X with
   | inl v =>
       (fun (x0 : vert A) (X0 : vert A + Unit) =>
        match X0 with
        | inl v0 =>
            (fun y0 : vert A => edge A x0 y0) v0
        | inr u => unit_name Unit u
        end) v
   | inr u =>
       unit_name
         (fun X0 : vert A + Unit =>
          match X0 with
          | inl v => (fun _ : vert A => Empty) v
          | inr u0 => unit_name Unit u0
          end) u
   end) cbn; intros [x|x] [y|y]; exact _.
  Defined.

  (** 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).
UA: Univalence
PR: PropResizing
A: Graph
x: vert (graph_succ A)
edge (graph_succ A) x (inr tt)
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
x: vert (graph_succ A)
edge (graph_succ A) x (inr tt)
    destruct x as [x|x]; exact tt.
  Qed.

  Definition graph_succ_top_unique@{}
             {A : Graph} (y : vert (graph_succ A))
             (yt : forall x, edge (graph_succ A) x y)
    : y = inr tt.
UA: Univalence
PR: PropResizing
A: Graph
y: vert (graph_succ A)
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x y
y = inr tt
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
y: vert (graph_succ A)
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x y
y = inr tt
    destruct y as [y|[]].
UA: Univalence
PR: PropResizing
A: Graph
y: vert A
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x (inl y)
inl y = inr tt
UA: Univalence
PR: PropResizing
A: Graph
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x (inr tt)
inr tt = inr tt
    -
UA: Univalence
PR: PropResizing
A: Graph
y: vert A
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x (inl y)
inl y = inr tt destruct (yt (inr tt)).
    -
UA: Univalence
PR: PropResizing
A: Graph
yt: forall x : vert (graph_succ A),
edge (graph_succ A) x (inr tt)
inr tt = inr tt reflexivity.
  Qed.

  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.
UA: Univalence
PR: PropResizing
A: Graph
x: vert (graph_succ A)
xt: ~ edge (graph_succ A) (inr tt) x
is_inl x
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
x: vert (graph_succ A)
xt: ~ edge (graph_succ A) (inr tt) x
is_inl x
    destruct x as [x|x].
UA: Univalence
PR: PropResizing
A: Graph
x: vert A
xt: ~ edge (graph_succ A) (inr tt) (inl x)
is_inl (inl x)
UA: Univalence
PR: PropResizing
A: Graph
x: Unit
xt: ~ edge (graph_succ A) (inr tt) (inr x)
is_inl (inr x)
    -
UA: Univalence
PR: PropResizing
A: Graph
x: vert A
xt: ~ edge (graph_succ A) (inr tt) (inl x)
is_inl (inl x) exact tt.
    -
UA: Univalence
PR: PropResizing
A: Graph
x: Unit
xt: ~ edge (graph_succ A) (inr tt) (inr x)
is_inl (inr x) destruct (xt tt).
  Qed.

  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.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
f (inr tt) = inr tt
    Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
f (inr tt) = inr tt
      apply (graph_succ_top_unique (f (inr tt))).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x : vert (graph_succ B),
edge (graph_succ B) x (f (inr tt))
      intros x.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert (graph_succ B)
edge (graph_succ B) x (f (inr tt))
      rewrite <- (eisretr f x).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert (graph_succ B)
edge (graph_succ B) (f (f^-1 x)) (f (inr tt))
      apply (fst (e (f^-1 x) (inr tt))).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert (graph_succ B)
edge (graph_succ A) (f^-1 x) (inr tt)
      apply graph_succ_top.
    Qed.

    Local Definition Ha@{} : forall x, is_inl (f (inl x)).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x : vert A, is_inl (f (inl x))
    Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x : vert A, is_inl (f (inl x))
      intros x.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
is_inl (f (inl x))
      apply graph_succ_not_top_unique.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
~ edge (graph_succ B) (inr tt) (f (inl x))
      rewrite <- (eisretr f (inr tt)).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
~ edge (graph_succ B) (f (f^-1 (inr tt))) (f (inl x))
      intros ed.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
ed: edge (graph_succ B) (f (f^-1 (inr tt)))
  (f (inl x))
Empty
      apply (snd (e (f^-1 (inr tt)) (inl x))) in ed.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
ed: edge (graph_succ A) (f^-1 (inr tt)) (inl x)
Empty
      pose (finr := graph_succ_equiv_inr).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
ed: edge (graph_succ A) (f^-1 (inr tt)) (inl x)
finr:= graph_succ_equiv_inr: f (inr tt) = inr tt
Empty
      apply moveL_equiv_V in finr.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
ed: edge (graph_succ A) (f^-1 (inr tt)) (inl x)
finr: inr tt = f^-1 (inr tt)
Empty
      rewrite <- finr in ed.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
ed: edge (graph_succ A) (inr tt) (inl x)
finr: inr tt = f^-1 (inr tt)
Empty
      exact (graph_succ_not_top x ed).
    Qed.

    (* Coq bug: without the [:Unit] annotation some floating universe appears. *)
    Local Definition Hb@{} : forall x:Unit, is_inr (f (inr x)).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x : Unit, is_inr (f (inr x))
    Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x : Unit, is_inr (f (inr x))
      destruct x.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
is_inr (f (inr tt))
      srefine (transport@{s Set} is_inr graph_succ_equiv_inr^ tt).
    Qed.

    Definition graph_unsucc_equiv_vert@{} : vert A <~> vert B
      := equiv_unfunctor_sum_l@{s s s s s s} 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)).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x, y: vert A
edge A x y <->
edge B (graph_unsucc_equiv_vert x)
  (graph_unsucc_equiv_vert y)
    Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x, y: vert A
edge A x y <->
edge B (graph_unsucc_equiv_vert x)
  (graph_unsucc_equiv_vert y)
      pose (h := e (inl x) (inl y)).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x, y: vert A
h:= e (inl x) (inl y): edge (graph_succ A) (inl x) (inl y) <->
edge (graph_succ B) (f (inl x)) (f (inl y))
edge A x y <->
edge B (graph_unsucc_equiv_vert x)
  (graph_unsucc_equiv_vert y)
      rewrite <- (unfunctor_sum_l_beta f Ha x) in h.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x, y: vert A
h: edge (graph_succ A) (inl x) (inl y) <->
edge (graph_succ B) (inl (unfunctor_sum_l f Ha x))
  (f (inl y))
edge A x y <->
edge B (graph_unsucc_equiv_vert x)
  (graph_unsucc_equiv_vert y)
      rewrite <- (unfunctor_sum_l_beta f Ha y) in h.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x, y: vert A
h: edge (graph_succ A) (inl x) (inl y) <->
edge (graph_succ B) (inl (unfunctor_sum_l f Ha x))
  (inl (unfunctor_sum_l f Ha y))
edge A x y <->
edge B (graph_unsucc_equiv_vert x)
  (graph_unsucc_equiv_vert y)
      exact h.
    Qed.

  End Graph_Succ_Equiv.

  Definition graph_succ_path_equiv@{} (A B : Graph)
    : (A = B) <~> (graph_succ A = graph_succ B).
UA: Univalence
PR: PropResizing
A, B: Graph
A = B <~> graph_succ A = graph_succ B
  Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
A = B <~> graph_succ A = graph_succ B
    refine ((equiv_path_graph _ _) oE _).
UA: Univalence
PR: PropResizing
A, B: Graph
A = B <~>
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)}
    refine (_ oE (equiv_path_graph _ _)^-1).
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} <~>
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)}
    srefine (equiv_adjointify _ _ _ _).
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} ->
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)}
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)} ->
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)}
UA: Univalence
PR: PropResizing
A, B: Graph
?f o ?g == idmap
UA: Univalence
PR: PropResizing
A, B: Graph
?g o ?f == idmap
    -
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} ->
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)} intros [f e].
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)}
      exists (f +E 1).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) ((f +E 1) x) ((f +E 1) y)
      intros x y.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x, y: vert (graph_succ A)
edge (graph_succ A) x y <->
edge (graph_succ B) ((f +E 1) x) ((f +E 1) y)
      destruct x as [x|x]; destruct y as [y|y]; cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x, y: vert A
edge A x y <-> edge B (f x) (f y)
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x: vert A
y: Unit
Unit <-> Unit
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x: Unit
y: vert A
Empty <-> Empty
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x, y: Unit
Unit <-> Unit
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x, y: vert A
edge A x y <-> edge B (f x) (f y) apply e.
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x: vert A
y: Unit
Unit <-> Unit split; apply idmap.
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x: Unit
y: vert A
Empty <-> Empty split; apply idmap.
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
x, y: Unit
Unit <-> Unit split; apply idmap.
    -
UA: Univalence
PR: PropResizing
A, B: Graph
{f : vert (graph_succ A) <~> vert (graph_succ B) &
forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)} ->
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)} intros [f e].
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
{f : vert A <~> vert B &
forall x y : vert A, edge A x y <-> edge B (f x) (f y)}
      exists (graph_unsucc_equiv_vert f e).
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
forall x y : vert A,
edge A x y <->
edge B (graph_unsucc_equiv_vert f e x)
  (graph_unsucc_equiv_vert f e y)
      exact (graph_unsucc_equiv_edge f e).
    -
UA: Univalence
PR: PropResizing
A, B: Graph
(fun
   X : {f : vert A <~> vert B &
       forall x y : vert A,
       edge A x y <-> edge B (f x) (f y)} =>
 (fun (f : vert A <~> vert B)
    (e : forall x y : vert A,
         edge A x y <-> edge B (f x) (f y)) =>
  (f +E 1;
  fun x y : vert (graph_succ A) =>
  match
    x as s
    return
      (edge (graph_succ A) s y <->
       edge (graph_succ B) ((f +E 1) s) ((f +E 1) y))
  with
  | inl v =>
      (fun x0 : vert A =>
       match
         y as s
         return
           (edge (graph_succ A) (inl x0) s <->
            edge (graph_succ B) ((f +E 1) (inl x0))
              ((f +E 1) s))
       with
       | inl v0 =>
           (fun y0 : vert A =>
            e x0 y0
            :
            edge (graph_succ A) (inl x0) (inl y0) <->
            edge (graph_succ B) ((f +E 1) (inl x0))
              ((f +E 1) (inl y0))) v0
       | inr u =>
           (fun y0 : Unit =>
            (idmap, idmap)
            :
            edge (graph_succ A) (inl x0) (inr y0) <->
            edge (graph_succ B) ((f +E 1) (inl x0))
              ((f +E 1) (inr y0))) u
       end) v
  | inr u =>
      (fun x0 : Unit =>
       match
         y as s
         return
           (edge (graph_succ A) (inr x0) s <->
            edge (graph_succ B) ((f +E 1) (inr x0))
              ((f +E 1) s))
       with
       | inl v =>
           (fun y0 : vert A =>
            (idmap, idmap)
            :
            edge (graph_succ A) (inr x0) (inl y0) <->
            edge (graph_succ B) ((f +E 1) (inr x0))
              ((f +E 1) (inl y0))) v
       | inr u0 =>
           (fun y0 : Unit =>
            (idmap, idmap)
            :
            edge (graph_succ A) (inr x0) (inr y0) <->
            edge (graph_succ B) ((f +E 1) (inr x0))
              ((f +E 1) (inr y0))) u0
       end) u
  end)) X.1 X.2)
o (fun
     X : {f
         : vert (graph_succ A) <~> vert (graph_succ B)
         &
         forall x y : vert (graph_succ A),
         edge (graph_succ A) x y <->
         edge (graph_succ B) (f x) (f y)} =>
   (fun
      (f : vert (graph_succ A) <~> vert (graph_succ B))
      (e : forall x y : vert (graph_succ A),
           edge (graph_succ A) x y <->
           edge (graph_succ B) (f x) (f y)) =>
    (graph_unsucc_equiv_vert f e;
    graph_unsucc_equiv_edge f e)) X.1 X.2) == idmap intros [f e].
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
(graph_unsucc_equiv_vert f e +E 1;
fun x y : vert (graph_succ A) =>
match
  x as s
  return
    (edge (graph_succ A) s y <->
     edge (graph_succ B)
       ((graph_unsucc_equiv_vert f e +E 1) s)
       ((graph_unsucc_equiv_vert f e +E 1) y))
with
| inl v =>
    match
      y as s
      return
        (edge (graph_succ A) (inl v) s <->
         edge (graph_succ B)
           ((graph_unsucc_equiv_vert f e +E 1) (inl v))
           ((graph_unsucc_equiv_vert f e +E 1) s))
    with
    | inl v0 => graph_unsucc_equiv_edge f e v v0
    | inr _ => (idmap, idmap)
    end
| inr u =>
    match
      y as s
      return
        (edge (graph_succ A) (inr u) s <->
         edge (graph_succ B)
           ((graph_unsucc_equiv_vert f e +E 1) (inr u))
           ((graph_unsucc_equiv_vert f e +E 1) s))
    with
    | inl _ => (idmap, idmap)
    | inr _ => (idmap, idmap)
    end
end) = (f; e)
      apply path_sigma_hprop; cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
graph_unsucc_equiv_vert f e +E 1 = f
      apply path_equiv, path_arrow; intros [x|[]]; cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
inl (unfunctor_sum_l f (Ha f e) x) = f (inl x)
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
inr tt = f (inr tt)
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
x: vert A
inl (unfunctor_sum_l f (Ha f e) x) = f (inl x) apply unfunctor_sum_l_beta.
      +
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert (graph_succ A) <~> vert (graph_succ B)
e: forall x y : vert (graph_succ A),
edge (graph_succ A) x y <->
edge (graph_succ B) (f x) (f y)
inr tt = f (inr tt) symmetry; apply graph_succ_equiv_inr, e.
    -
UA: Univalence
PR: PropResizing
A, B: Graph
(fun
   X : {f
       : vert (graph_succ A) <~> vert (graph_succ B) &
       forall x y : vert (graph_succ A),
       edge (graph_succ A) x y <->
       edge (graph_succ B) (f x) (f y)} =>
 (fun
    (f : vert (graph_succ A) <~> vert (graph_succ B))
    (e : forall x y : vert (graph_succ A),
         edge (graph_succ A) x y <->
         edge (graph_succ B) (f x) (f y)) =>
  (graph_unsucc_equiv_vert f e;
  graph_unsucc_equiv_edge f e)) X.1 X.2)
o (fun
     X : {f : vert A <~> vert B &
         forall x y : vert A,
         edge A x y <-> edge B (f x) (f y)} =>
   (fun (f : vert A <~> vert B)
      (e : forall x y : vert A,
           edge A x y <-> edge B (f x) (f y)) =>
    (f +E 1;
    fun x y : vert (graph_succ A) =>
    match
      x as s
      return
        (edge (graph_succ A) s y <->
         edge (graph_succ B) ((f +E 1) s) ((f +E 1) y))
    with
    | inl v =>
        (fun x0 : vert A =>
         match
           y as s
           return
             (edge (graph_succ A) (inl x0) s <->
              edge (graph_succ B) ((f +E 1) (inl x0))
                ((f +E 1) s))
         with
         | inl v0 =>
             (fun y0 : vert A =>
              e x0 y0
              :
              edge (graph_succ A) (inl x0) (inl y0) <->
              edge (graph_succ B) ((f +E 1) (inl x0))
                ((f +E 1) (inl y0))) v0
         | inr u =>
             (fun y0 : Unit =>
              (idmap, idmap)
              :
              edge (graph_succ A) (inl x0) (inr y0) <->
              edge (graph_succ B) ((f +E 1) (inl x0))
                ((f +E 1) (inr y0))) u
         end) v
    | inr u =>
        (fun x0 : Unit =>
         match
           y as s
           return
             (edge (graph_succ A) (inr x0) s <->
              edge (graph_succ B) ((f +E 1) (inr x0))
                ((f +E 1) s))
         with
         | inl v =>
             (fun y0 : vert A =>
              (idmap, idmap)
              :
              edge (graph_succ A) (inr x0) (inl y0) <->
              edge (graph_succ B) ((f +E 1) (inr x0))
                ((f +E 1) (inl y0))) v
         | inr u0 =>
             (fun y0 : Unit =>
              (idmap, idmap)
              :
              edge (graph_succ A) (inr x0) (inr y0) <->
              edge (graph_succ B) ((f +E 1) (inr x0))
                ((f +E 1) (inr y0))) u0
         end) u
    end)) X.1 X.2) == idmap intros [f e].
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
(graph_unsucc_equiv_vert (f +E 1)
   (fun x y : vert (graph_succ A) =>
    match
      x as s
      return
        (edge (graph_succ A) s y <->
         edge (graph_succ B) ((f +E 1) s) ((f +E 1) y))
    with
    | inl v =>
        match
          y as s
          return
            (edge (graph_succ A) (inl v) s <->
             edge (graph_succ B) ((f +E 1) (inl v))
               ((f +E 1) s))
        with
        | inl v0 => e v v0
        | inr _ => (idmap, idmap)
        end
    | inr u =>
        match
          y as s
          return
            (edge (graph_succ A) (inr u) s <->
             edge (graph_succ B) ((f +E 1) (inr u))
               ((f +E 1) s))
        with
        | inl _ => (idmap, idmap)
        | inr _ => (idmap, idmap)
        end
    end);
graph_unsucc_equiv_edge (f +E 1)
  (fun x y : vert (graph_succ A) =>
   match
     x as s
     return
       (edge (graph_succ A) s y <->
        edge (graph_succ B) ((f +E 1) s) ((f +E 1) y))
   with
   | inl v =>
       match
         y as s
         return
           (edge (graph_succ A) (inl v) s <->
            edge (graph_succ B) ((f +E 1) (inl v))
              ((f +E 1) s))
       with
       | inl v0 => e v v0
       | inr _ => (idmap, idmap)
       end
   | inr u =>
       match
         y as s
         return
           (edge (graph_succ A) (inr u) s <->
            edge (graph_succ B) ((f +E 1) (inr u))
              ((f +E 1) s))
       with
       | inl _ => (idmap, idmap)
       | inr _ => (idmap, idmap)
       end
   end)) = (f; e)
      apply path_sigma_hprop; cbn.
UA: Univalence
PR: PropResizing
A, B: Graph
f: vert A <~> vert B
e: forall x y : vert A,
edge A x y <-> edge B (f x) (f y)
graph_unsucc_equiv_vert (f +E 1)
  (fun x y : vert A + Unit =>
   match
     x as s
     return
       (match s with
        | inl v =>
            fun X : vert A + Unit =>
            match X with
            | inl v0 => edge A v v0
            | inr _ => Unit
            end
        | inr _ =>
            fun X : vert A + Unit =>
            match X with
            | inl _ => Empty
            | inr _ => Unit
            end
        end y <->
        match functor_sum f idmap s with
        | inl v =>
            fun X : vert B + Unit =>
            match X with
            | inl v0 => edge B v v0
            | inr _ => Unit
            end
        | inr _ =>
            fun X : vert B + Unit =>
            match X with
            | inl _ => Empty
            | inr _ => Unit
            end
        end (functor_sum f idmap y))
   with
   | inl v =>
       match
         y as s
         return
           (match s with
            | inl v0 => edge A v v0
            | inr _ => Unit
            end <->
            match functor_sum f idmap s with
            | inl v0 => edge B (f v) v0
            | inr _ => Unit
            end)
       with
       | inl v0 => e v v0
       | inr _ => (idmap, idmap)
       end
   | inr _ =>
       match
         y as s
         return
           (match s with
            | inl _ => Empty
            | inr _ => Unit
            end <->
            match functor_sum f idmap s with
            | inl _ => Empty
            | inr _ => Unit
            end)
       with
       | inl _ => (idmap, idmap)
       | inr _ => (idmap, idmap)
       end
   end) = f
      apply path_equiv, path_arrow; intros x; reflexivity.
  Defined.

  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).
UA: Univalence
PR: PropResizing
n: Graph
IsHProp (in_N n)
  Proof.
UA: Univalence
PR: PropResizing
n: Graph
IsHProp (in_N n)
    apply istrunc_forall.
  Qed.

  (** [p] : universe of [N], morally [u+1] i.e. [s+2]. *)
  Universe p.
  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.

  Definition zero@{} : N.
UA: Univalence
PR: PropResizing
N
  Proof.
UA: Univalence
PR: PropResizing
N
    exists graph_zero.
UA: Univalence
PR: PropResizing
in_N graph_zero
    intros P PH P0 Ps; exact P0.
  Defined.

  Definition succ@{} : N -> N.
UA: Univalence
PR: PropResizing
N -> N
  Proof.
UA: Univalence
PR: PropResizing
N -> N
    intros [n nrec].
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
N
    exists (graph_succ n).
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
in_N (graph_succ n)
    intros P PH P0 Ps.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P (graph_succ n) apply Ps.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P n
    exact (nrec P PH P0 Ps).
  Defined.

  (** First Peano axiom: successor is injective *)
  Definition succ_inj@{} (n m : N) (p : succ n = succ m) : n = m.
UA: Univalence
PR: PropResizing
n, m: N
p: succ n = succ m
n = m
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
p: succ n = succ m
n = m
    apply path_N.
UA: Univalence
PR: PropResizing
n, m: N
p: succ n = succ m
n.1 = m.1
    apply ((graph_succ_path_equiv n.1 m.1)^-1).
UA: Univalence
PR: PropResizing
n, m: N
p: succ n = succ m
graph_succ n.1 = graph_succ m.1
    exact (p..1).
  Qed.

  (** 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).
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
IsHProp (A = B)
  Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
IsHProp (A = B)
    apply hprop_inhabited_contr; intros [].
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
Contr (A = A)
    apply Arec; try exact _.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
Contr (graph_zero = graph_zero)
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
forall A : Graph,
Contr (A = A) -> Contr (graph_succ A = graph_succ A)
    -
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
Contr (graph_zero = graph_zero) apply contr_inhabited_hprop; try exact 1.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
IsHProp (graph_zero = graph_zero)
      apply hprop_allpath.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
forall x y : graph_zero = graph_zero, x = y
      equiv_intro (equiv_path_graph graph_zero graph_zero) fe.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
fe: {f : vert graph_zero <~> vert graph_zero &
forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)}
forall y : graph_zero = graph_zero,
equiv_path_graph graph_zero graph_zero fe = y
      destruct fe as [f e].
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
f: vert graph_zero <~> vert graph_zero
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)
forall y : graph_zero = graph_zero,
equiv_path_graph graph_zero graph_zero (f; e) = y
      equiv_intro (equiv_path_graph graph_zero graph_zero) fe'.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
f: vert graph_zero <~> vert graph_zero
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)
fe': {f : vert graph_zero <~> vert graph_zero &
forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)}
equiv_path_graph graph_zero graph_zero (f; e) =
equiv_path_graph graph_zero graph_zero fe'
      destruct fe' as [f' e'].
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
f: vert graph_zero <~> vert graph_zero
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)
f': vert graph_zero <~> vert graph_zero
e': forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f' x) (f' y)
equiv_path_graph graph_zero graph_zero (f; e) =
equiv_path_graph graph_zero graph_zero (f'; e')
      apply equiv_ap; try exact _.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
f: vert graph_zero <~> vert graph_zero
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)
f': vert graph_zero <~> vert graph_zero
e': forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f' x) (f' y)
(f; e) = (f'; e')
      apply path_sigma_hprop, path_equiv@{s s s}, path_arrow.
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
f: vert graph_zero <~> vert graph_zero
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f x) (f y)
f': vert graph_zero <~> vert graph_zero
e': forall x y : vert graph_zero,
edge graph_zero x y <->
edge graph_zero (f' x) (f' y)
(f; e).1 == (f'; e').1
      intros [].
    -
UA: Univalence
PR: PropResizing
A, B: Graph
Arec: in_N A
forall A : Graph,
Contr (A = A) -> Contr (graph_succ A = graph_succ A) try clear B;intros B BC.
UA: Univalence
PR: PropResizing
A: Graph
Arec: in_N A
B: Graph
BC: Contr (B = B)
Contr (graph_succ B = graph_succ B)
      refine (contr_equiv (B = B) (graph_succ_path_equiv B B)).
  Qed.

  Instance ishprop_path_N@{} (n : N) (A : Graph) : IsHProp (n.1 = A).
UA: Univalence
PR: PropResizing
n: N
A: Graph
IsHProp (n.1 = A)
  Proof.
UA: Univalence
PR: PropResizing
n: N
A: Graph
IsHProp (n.1 = A)
    apply ishprop_path_graph_in_N, pr2.
  Qed.

  Instance ishset_N@{} : IsHSet N.
UA: Univalence
PR: PropResizing
IsHSet N
  Proof.
UA: Univalence
PR: PropResizing
IsHSet N
    apply istrunc_S.
UA: Univalence
PR: PropResizing
is_mere_relation N paths
    intros n m.
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n = m)
    change (IsHProp (n = m)).
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n = m)
    refine (istrunc_equiv_istrunc (n.1 = m.1) (equiv_path_sigma_hprop n m)).
  Qed.

  Definition graph_zero_neq_succ@{} {A : Graph}
    : graph_zero <> graph_succ A.
UA: Univalence
PR: PropResizing
A: Graph
graph_zero <> graph_succ A
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
graph_zero <> graph_succ A
    intros p.
UA: Univalence
PR: PropResizing
A: Graph
p: graph_zero = graph_succ A
Empty
    destruct ((equiv_path_graph graph_zero (graph_succ A))^-1 p) as [f e].
UA: Univalence
PR: PropResizing
A: Graph
p: graph_zero = graph_succ A
f: vert graph_zero <~> vert (graph_succ A)
e: forall x y : vert graph_zero,
edge graph_zero x y <->
edge (graph_succ A) (f x) (f y)
Empty
    exact (f^-1 (inr tt)).
  Qed.

  (** Second Peano axiom: zero is not a successor *)
  Definition zero_neq_succ@{} (n : N) : zero <> succ n.
UA: Univalence
PR: PropResizing
n: N
zero <> succ n
  Proof.
UA: Univalence
PR: PropResizing
n: N
zero <> succ n
    intros p; apply pr1_path in p; refine (graph_zero_neq_succ p).
  Qed.

  (** 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.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
in_N n
  Proof.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
in_N n
    intros P' PH' P0' Ps'.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
P' n
    srefine ((equiv_smalltype (P' n))
             (nrec (fun A => smalltype (P' A)) _ _ _));
      try exact _; cbn.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
smalltype (P' graph_zero)
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
forall A : Graph,
smalltype (P' A) -> smalltype (P' (graph_succ A))
    -
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
smalltype (P' graph_zero) exact ((equiv_smalltype (P' graph_zero))^-1 P0').
    -
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
forall A : Graph,
smalltype (P' A) -> smalltype (P' (graph_succ A)) intros A P'A.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
P': Graph -> Type
PH': forall A : Graph, IsHProp (P' A)
P0': P' graph_zero
Ps': forall A : Graph, P' A -> P' (graph_succ A)
A: Graph
P'A: smalltype (P' A)
smalltype (P' (graph_succ A))
      exact ((equiv_smalltype (P' (graph_succ A)))^-1
                                (Ps' A ((equiv_smalltype (P' A)) P'A))).
  Qed.

  Local Instance ishprop_graph_zero_or_succ@{} : forall n : Graph,
      IsHProp ((n = graph_zero) + { m : N & n = graph_succ m.1 }).
UA: Univalence
PR: PropResizing
forall n : Graph,
IsHProp
  ((n = graph_zero) + {m : N & n = graph_succ m.1})
  Proof.
UA: Univalence
PR: PropResizing
forall n : Graph,
IsHProp
  ((n = graph_zero) + {m : N & n = graph_succ m.1})
    intros n.
UA: Univalence
PR: PropResizing
n: Graph
IsHProp
  ((n = graph_zero) + {m : N & n = graph_succ m.1}) apply ishprop_sum@{u p p}.
UA: Univalence
PR: PropResizing
n: Graph
IsHProp (n = graph_zero)
UA: Univalence
PR: PropResizing
n: Graph
IsHProp {m : N & n = graph_succ m.1}
UA: Univalence
PR: PropResizing
n: Graph
n = graph_zero ->
{m : N & n = graph_succ m.1} -> Empty
    -
UA: Univalence
PR: PropResizing
n: Graph
IsHProp (n = graph_zero) apply (@istrunc_equiv_istrunc _ _ (equiv_path_inverse _ _)),ishprop_path_graph_in_N.
UA: Univalence
PR: PropResizing
n: Graph
in_N graph_zero
      exact zero.2.
    -
UA: Univalence
PR: PropResizing
n: Graph
IsHProp {m : N & n = graph_succ m.1} apply @ishprop_sigma_disjoint.
UA: Univalence
PR: PropResizing
n: Graph
forall a : N, IsHProp (n = graph_succ a.1)
UA: Univalence
PR: PropResizing
n: Graph
forall x y : N,
n = graph_succ x.1 -> n = graph_succ y.1 -> x = y
      +
UA: Univalence
PR: PropResizing
n: Graph
forall a : N, IsHProp (n = graph_succ a.1) intros m;apply (@istrunc_equiv_istrunc _ _ (equiv_path_inverse _ _)).
UA: Univalence
PR: PropResizing
n: Graph
m: N
IsHProp (graph_succ m.1 = n)
        apply ishprop_path_graph_in_N.
UA: Univalence
PR: PropResizing
n: Graph
m: N
in_N (graph_succ m.1) exact ((succ m).2).
      +
UA: Univalence
PR: PropResizing
n: Graph
forall x y : N,
n = graph_succ x.1 -> n = graph_succ y.1 -> x = y intros x y ex ey.
UA: Univalence
PR: PropResizing
n: Graph
x, y: N
ex: n = graph_succ x.1
ey: n = graph_succ y.1
x = y
        apply succ_inj, path_N.
UA: Univalence
PR: PropResizing
n: Graph
x, y: N
ex: n = graph_succ x.1
ey: n = graph_succ y.1
(succ x).1 = (succ y).1 path_via n.
    -
UA: Univalence
PR: PropResizing
n: Graph
n = graph_zero ->
{m : N & n = graph_succ m.1} -> Empty intros e0 [m es].
UA: Univalence
PR: PropResizing
n: Graph
e0: n = graph_zero
m: N
es: n = graph_succ m.1
Empty
      apply zero_neq_succ with m, path_N.
UA: Univalence
PR: PropResizing
n: Graph
e0: n = graph_zero
m: N
es: n = graph_succ m.1
zero.1 = (succ m).1 path_via n.
  Qed.

  Local Instance ishprop_N_zero_or_succ@{} : forall n : N,
      IsHProp ((n = zero) + { m : N & n = succ m }).
UA: Univalence
PR: PropResizing
forall n : N,
IsHProp ((n = zero) + {m : N & n = succ m})
  Proof.
UA: Univalence
PR: PropResizing
forall n : N,
IsHProp ((n = zero) + {m : N & n = succ m})
    intros n.
UA: Univalence
PR: PropResizing
n: N
IsHProp ((n = zero) + {m : N & n = succ m}) apply ishprop_sum.
UA: Univalence
PR: PropResizing
n: N
IsHProp (n = zero)
UA: Univalence
PR: PropResizing
n: N
IsHProp {m : N & n = succ m}
UA: Univalence
PR: PropResizing
n: N
n = zero -> {m : N & n = succ m} -> Empty
    -
UA: Univalence
PR: PropResizing
n: N
IsHProp (n = zero) exact _.
    -
UA: Univalence
PR: PropResizing
n: N
IsHProp {m : N & n = succ m} apply ishprop_sigma_disjoint.
UA: Univalence
PR: PropResizing
n: N
forall x y : N, n = succ x -> n = succ y -> x = y intros x y ex ey.
UA: Univalence
PR: PropResizing
n, x, y: N
ex: n = succ x
ey: n = succ y
x = y
      apply succ_inj;path_via n.
    -
UA: Univalence
PR: PropResizing
n: N
n = zero -> {m : N & n = succ m} -> Empty intros e0 [m es].
UA: Univalence
PR: PropResizing
n: N
e0: n = zero
m: N
es: n = succ m
Empty
      apply zero_neq_succ with m.
UA: Univalence
PR: PropResizing
n: N
e0: n = zero
m: N
es: n = succ m
zero = succ m path_via n.
  Qed.

  Definition N_zero_or_succ@{} (n : N)
    : (n = zero) + { m : N & n = succ m }.
UA: Univalence
PR: PropResizing
n: N
(n = zero) + {m : N & n = succ m}
  Proof.
UA: Univalence
PR: PropResizing
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)))).
UA: Univalence
PR: PropResizing
n: N
(n.1 = zero.1) + {m : N & n.1 = (succ m).1}
    destruct n as [n nrec]; cbn.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
(n = graph_zero) + {m : N & n = graph_succ m.1}
    srefine (resize_nrec n nrec
             (fun n => (n = graph_zero) +
                    {m : N & n = graph_succ m.1}) _ _ _); cbn.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
(graph_zero = graph_zero) +
{m : N & graph_zero = graph_succ m.1}
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
forall A : Graph,
(A = graph_zero) + {m : N & A = graph_succ m.1} ->
(graph_succ A = graph_zero) +
{m : N & graph_succ A = graph_succ m.1}
    -
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
(graph_zero = graph_zero) +
{m : N & graph_zero = graph_succ m.1} apply inl; reflexivity.
    -
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
forall A : Graph,
(A = graph_zero) + {m : N & A = graph_succ m.1} ->
(graph_succ A = graph_zero) +
{m : N & graph_succ A = graph_succ m.1} intros A [A0|[m As]]; apply inr.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
A0: A = graph_zero
{m : N & graph_succ A = graph_succ m.1}
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
m: N
As: A = graph_succ m.1
{m : N & graph_succ A = graph_succ m.1}
      +
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
A0: A = graph_zero
{m : N & graph_succ A = graph_succ m.1} exists zero.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
A0: A = graph_zero
graph_succ A = graph_succ zero.1
        rewrite A0.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
A0: A = graph_zero
graph_succ graph_zero = graph_succ zero.1
        reflexivity.
      +
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
m: N
As: A = graph_succ m.1
{m : N & graph_succ A = graph_succ m.1} exists (succ m).
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
m: N
As: A = graph_succ m.1
graph_succ A = graph_succ (succ m).1
        rewrite As.
UA: Univalence
PR: PropResizing
n: Graph
nrec: in_N n
A: Graph
m: N
As: A = graph_succ m.1
graph_succ (graph_succ m.1) = graph_succ (succ m).1
        reflexivity.
  Qed.

  Definition pred_in_N@{} (n : Graph) (snrec : in_N@{u} (graph_succ n))
    : in_N@{u} n.
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
in_N n
  Proof.
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
in_N n
    destruct (N_zero_or_succ (graph_succ n ; snrec)) as [H0|[m Hs]].
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
H0: (graph_succ n; snrec) = zero
in_N n
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
m: N
Hs: (graph_succ n; snrec) = succ m
in_N n
    -
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
H0: (graph_succ n; snrec) = zero
in_N n apply pr1_path in H0; cbn in H0.
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
H0: graph_succ n = graph_zero
in_N n
      destruct (graph_zero_neq_succ H0^).
    -
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
m: N
Hs: (graph_succ n; snrec) = succ m
in_N n apply pr1_path in Hs.
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
m: N
Hs: (graph_succ n; snrec).1 = (succ m).1
in_N n
      apply graph_unsucc_path in Hs.
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
m: N
Hs: n = m.1
in_N n
      apply (transport@{u p} in_N Hs^).
UA: Univalence
PR: PropResizing
n: Graph
snrec: in_N (graph_succ n)
m: N
Hs: n = m.1
in_N m.1
      exact m.2.
  Qed.

  (** 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.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
forall n : N, P n
  Proof.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
forall n : N, P n
    intros [n nrec].
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
n: Graph
nrec: in_N n
P (n; nrec)
    pose (Q := fun m:Graph => forall (mrec : in_N m), P (m;mrec)).
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
n: Graph
nrec: in_N n
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
P (n; nrec)
    refine (resize_nrec n nrec Q _ _ _ nrec); clear n nrec.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
Q graph_zero
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
forall A : Graph, Q A -> Q (graph_succ A)
    -
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
Q graph_zero intros zrec.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
zrec: in_N graph_zero
P (graph_zero; zrec)
      refine (transport P _ P0).
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
zrec: in_N graph_zero
zero = (graph_zero; zrec)
      apply ap.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
zrec: in_N graph_zero
(fun (P : Graph -> Type)
   (_ : forall A : Graph, IsHProp (P A))
   (P0 : P graph_zero)
   (_ : forall A : Graph, P A -> P (graph_succ A)) =>
 P0) = zrec
      apply path_ishprop.
    -
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
forall A : Graph, Q A -> Q (graph_succ A) intros A QA Asrec.
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
A: Graph
QA: Q A
Asrec: in_N (graph_succ A)
P (graph_succ A; Asrec)
      pose (m := (A ; pred_in_N A Asrec) : N).
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
A: Graph
QA: Q A
Asrec: in_N (graph_succ A)
m:= (A; pred_in_N A Asrec) : N: N
P (graph_succ A; Asrec)
      refine (transport P _ (Ps m (QA (pred_in_N A Asrec)))).
UA: Univalence
PR: PropResizing
P: N -> Type
H: forall n : N, IsHProp (P n)
P0: P zero
Ps: forall n : N, P n -> P (succ n)
Q:= fun m : Graph => forall mrec : in_N m, P (m; mrec): Graph -> Type
A: Graph
QA: Q A
Asrec: in_N (graph_succ A)
m:= (A; pred_in_N A Asrec) : N: N
succ m = (graph_succ A; Asrec)
      apply path_N; reflexivity.
  Qed.

  (** A first application *)
  Definition N_neq_succ@{} (n : N) : n <> succ n.
UA: Univalence
PR: PropResizing
n: N
n <> succ n
  Proof.
UA: Univalence
PR: PropResizing
n: N
n <> succ n
    revert n; apply N_propind@{p}.
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (n <> succ n)
UA: Univalence
PR: PropResizing
zero <> succ zero
UA: Univalence
PR: PropResizing
forall n : N, n <> succ n -> succ n <> succ (succ n)
    -
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (n <> succ n) intros n;exact istrunc_arrow@{p p p}.
    -
UA: Univalence
PR: PropResizing
zero <> succ zero apply zero_neq_succ.
    -
UA: Univalence
PR: PropResizing
forall n : N, n <> succ n -> succ n <> succ (succ n) intros n H e.
UA: Univalence
PR: PropResizing
n: N
H: n <> succ n
e: succ n = succ (succ n)
Empty
      apply H.
UA: Univalence
PR: PropResizing
n: N
H: n <> succ n
e: succ n = succ (succ n)
n = succ n
      exact (succ_inj n (succ n) e).
  Qed.

  (** 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
  restrictions 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.
UA: Univalence
PR: PropResizing
A, B: Graph
Graph
  Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
Graph
    exists (vert A + vert B).
UA: Univalence
PR: PropResizing
A, B: Graph
{E : vert A + vert B -> vert A + vert B -> Type &
is_mere_relation (vert A + vert B) E}
    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).
UA: Univalence
PR: PropResizing
A, B: Graph
forall x y : vert A + vert B,
IsHProp
  match x with
  | inl a =>
      match y with
      | inl a' => edge A a a'
      | inr _ => Unit
      end
  | inr b =>
      match y with
      | inl _ => Empty
      | inr b' => edge B b b'
      end
  end
    intros [a|b] [a'|b']; exact _.
  Defined.

  Definition graph_add_zero_r@{} (A : Graph) : graph_add A graph_zero = A.
UA: Univalence
PR: PropResizing
A: Graph
graph_add A graph_zero = A
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
graph_add A graph_zero = A
    apply equiv_path_graph.
UA: Univalence
PR: PropResizing
A: Graph
{f : vert (graph_add A graph_zero) <~> vert A &
forall x y : vert (graph_add A graph_zero),
edge (graph_add A graph_zero) x y <->
edge A (f x) (f y)}
    exists (sum_empty_r (vert A)).
UA: Univalence
PR: PropResizing
A: Graph
forall x y : vert (graph_add A graph_zero),
edge (graph_add A graph_zero) x y <->
edge A (sum_empty_r (vert A) x)
  (sum_empty_r (vert A) y)
    intros [x|[]] [y|[]].
UA: Univalence
PR: PropResizing
A: Graph
x, y: vert A
edge (graph_add A graph_zero) (inl x) (inl y) <->
edge A (sum_empty_r (vert A) (inl x))
  (sum_empty_r (vert A) (inl y))
    apply iff_reflexive@{u s}.
  Qed.

  Definition graph_add_zero_l@{} (A : Graph) : graph_add graph_zero A = A.
UA: Univalence
PR: PropResizing
A: Graph
graph_add graph_zero A = A
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
graph_add graph_zero A = A
    apply equiv_path_graph.
UA: Univalence
PR: PropResizing
A: Graph
{f : vert (graph_add graph_zero A) <~> vert A &
forall x y : vert (graph_add graph_zero A),
edge (graph_add graph_zero A) x y <->
edge A (f x) (f y)}
    exists (sum_empty_l (vert A)).
UA: Univalence
PR: PropResizing
A: Graph
forall x y : vert (graph_add graph_zero A),
edge (graph_add graph_zero A) x y <->
edge A (sum_empty_l (vert A) x)
  (sum_empty_l (vert A) y)
    intros [[]|x] [[]|y].
UA: Univalence
PR: PropResizing
A: Graph
x, y: vert A
edge (graph_add graph_zero A) (inr x) (inr y) <->
edge A (sum_empty_l (vert A) (inr x))
  (sum_empty_l (vert A) (inr y))
    apply iff_reflexive@{u s}.
  Qed.

  Definition graph_add_succ@{} (A B : Graph)
    : graph_add A (graph_succ B) = graph_succ (graph_add A B).
UA: Univalence
PR: PropResizing
A, B: Graph
graph_add A (graph_succ B) =
graph_succ (graph_add A B)
  Proof.
UA: Univalence
PR: PropResizing
A, B: Graph
graph_add A (graph_succ B) =
graph_succ (graph_add A B)
    apply equiv_path_graph.
UA: Univalence
PR: PropResizing
A, B: Graph
{f
: vert (graph_add A (graph_succ B)) <~>
  vert (graph_succ (graph_add A B)) &
forall x y : vert (graph_add A (graph_succ B)),
edge (graph_add A (graph_succ B)) x y <->
edge (graph_succ (graph_add A B)) (f x) (f y)}
    exists (equiv_inverse (equiv_sum_assoc (vert A) (vert B) Unit)).
UA: Univalence
PR: PropResizing
A, B: Graph
forall x y : vert (graph_add A (graph_succ B)),
edge (graph_add A (graph_succ B)) x y <->
edge (graph_succ (graph_add A B))
  ((equiv_sum_assoc (vert A) (vert B) Unit)^-1%equiv x)
  ((equiv_sum_assoc (vert A) (vert B) Unit)^-1%equiv y)
    intros [x|[x|[]]] [y|[y|[]]];apply iff_reflexive@{u s}.
  Qed.

  Definition graph_add_assoc@{} (A B C : Graph)
    : graph_add (graph_add A B) C = graph_add A (graph_add B C).
UA: Univalence
PR: PropResizing
A, B, C: Graph
graph_add (graph_add A B) C =
graph_add A (graph_add B C)
  Proof.
UA: Univalence
PR: PropResizing
A, B, C: Graph
graph_add (graph_add A B) C =
graph_add A (graph_add B C)
    apply equiv_path_graph.
UA: Univalence
PR: PropResizing
A, B, C: Graph
{f
: vert (graph_add (graph_add A B) C) <~>
  vert (graph_add A (graph_add B C)) &
forall x y : vert (graph_add (graph_add A B) C),
edge (graph_add (graph_add A B) C) x y <->
edge (graph_add A (graph_add B C)) (f x) (f y)}
    exists (equiv_sum_assoc _ _ _).
UA: Univalence
PR: PropResizing
A, B, C: Graph
forall x y : vert (graph_add (graph_add A B) C),
edge (graph_add (graph_add A B) C) x y <->
edge (graph_add A (graph_add B C))
  (equiv_sum_assoc (vert A) (vert B) (vert C) x)
  (equiv_sum_assoc (vert A) (vert B) (vert C) y)
    intros [[x|x]|x] [[y|y]|y]; apply iff_reflexive@{u s}.
  Qed.

  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.
UA: Univalence
PR: PropResizing
A: Graph
graph_add A graph_one = graph_succ A
  Proof.
UA: Univalence
PR: PropResizing
A: Graph
graph_add A graph_one = graph_succ A
    apply equiv_path_graph.
UA: Univalence
PR: PropResizing
A: Graph
{f
: vert (graph_add A graph_one) <~> vert (graph_succ A)
&
forall x y : vert (graph_add A graph_one),
edge (graph_add A graph_one) x y <->
edge (graph_succ A) (f x) (f y)}
    exists equiv_idmap.
UA: Univalence
PR: PropResizing
A: Graph
forall x y : vert (graph_add A graph_one),
edge (graph_add A graph_one) x y <->
edge (graph_succ A) (1%equiv x) (1%equiv y)
    intros [x|[]] [y|[]]; apply iff_reflexive@{u s}.
  Qed.

  Definition graph_succ_zero@{} : graph_succ graph_zero = graph_one.
UA: Univalence
PR: PropResizing
graph_succ graph_zero = graph_one
  Proof.
UA: Univalence
PR: PropResizing
graph_succ graph_zero = graph_one
    rewrite <- graph_add_one_succ.
UA: Univalence
PR: PropResizing
graph_add graph_zero graph_one = graph_one
    apply graph_add_zero_l.
  Qed.

  Definition one@{} : N.
UA: Univalence
PR: PropResizing
N
  Proof.
UA: Univalence
PR: PropResizing
N
    exists graph_one.
UA: Univalence
PR: PropResizing
in_N graph_one
    intros P PH P0 Ps.
UA: Univalence
PR: PropResizing
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P graph_one
    rewrite <- graph_succ_zero.
UA: Univalence
PR: PropResizing
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P (graph_succ graph_zero)
    apply Ps, P0.
  Defined.

  Definition N_add@{} (n m : N) : N.
UA: Univalence
PR: PropResizing
n, m: N
N
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
N
    exists (graph_add n.1 m.1).
UA: Univalence
PR: PropResizing
n, m: N
in_N (graph_add n.1 m.1)
    intros P PH P0 Ps.
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P (graph_add n.1 m.1)
    apply m.2.
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
forall A : Graph, IsHProp (P (graph_add n.1 A))
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P (graph_add n.1 graph_zero)
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
forall A : Graph,
P (graph_add n.1 A) ->
P (graph_add n.1 (graph_succ A))
    -
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
forall A : Graph, IsHProp (P (graph_add n.1 A)) intros; apply PH.
    -
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P (graph_add n.1 graph_zero) apply (transport P (graph_add_zero_r n.1)^).
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
P n.1
      exact (n.2 P PH P0 Ps).
    -
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
forall A : Graph,
P (graph_add n.1 A) ->
P (graph_add n.1 (graph_succ A)) intros A PA.
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
A: Graph
PA: P (graph_add n.1 A)
P (graph_add n.1 (graph_succ A))
      apply (transport P (graph_add_succ n.1 A)^).
UA: Univalence
PR: PropResizing
n, m: N
P: Graph -> Type
PH: forall A : Graph, IsHProp (P A)
P0: P graph_zero
Ps: forall A : Graph, P A -> P (graph_succ A)
A: Graph
PA: P (graph_add n.1 A)
P (graph_succ (graph_add n.1 A))
      apply Ps, PA.
  Defined.

  Notation "n + m" := (N_add n m).

  Definition N_add_zero_l@{} (n : N) : zero + n = n.
UA: Univalence
PR: PropResizing
n: N
zero + n = n
  Proof.
UA: Univalence
PR: PropResizing
n: N
zero + n = n
    apply path_N, graph_add_zero_l.
  Qed.

  Definition N_add_zero_r@{} (n : N) : n + zero = n.
UA: Univalence
PR: PropResizing
n: N
n + zero = n
  Proof.
UA: Univalence
PR: PropResizing
n: N
n + zero = n
    apply path_N, graph_add_zero_r.
  Qed.

  Definition N_add_succ@{} (n m : N) : n + succ m = succ (n + m).
UA: Univalence
PR: PropResizing
n, m: N
n + succ m = succ (n + m)
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
n + succ m = succ (n + m)
    apply path_N, graph_add_succ.
  Qed.

  Definition N_add_assoc@{} (n m k : N) : (n + m) + k = n + (m + k).
UA: Univalence
PR: PropResizing
n, m, k: N
n + m + k = n + (m + k)
  Proof.
UA: Univalence
PR: PropResizing
n, m, k: N
n + m + k = n + (m + k)
    apply path_N, graph_add_assoc.
  Qed.

  Definition N_add_cancel_r@{} (n m k : N) (H : n + k = m + k)
    : n = m.
UA: Univalence
PR: PropResizing
n, m, k: N
H: n + k = m + k
n = m
  Proof.
UA: Univalence
PR: PropResizing
n, m, k: N
H: n + k = m + k
n = m
    revert k H.
UA: Univalence
PR: PropResizing
n, m: N
forall k : N, n + k = m + k -> n = m
    refine (N_propind _ _ _).
UA: Univalence
PR: PropResizing
n, m: N
n + zero = m + zero -> n = m
UA: Univalence
PR: PropResizing
n, m: N
forall n0 : N,
(n + n0 = m + n0 -> n = m) ->
n + succ n0 = m + succ n0 -> n = m
    -
UA: Univalence
PR: PropResizing
n, m: N
n + zero = m + zero -> n = m intros H; rewrite !N_add_zero_r in H; exact H.
    -
UA: Univalence
PR: PropResizing
n, m: N
forall n0 : N,
(n + n0 = m + n0 -> n = m) ->
n + succ n0 = m + succ n0 -> n = m intros k H1 H2.
UA: Univalence
PR: PropResizing
n, m, k: N
H1: n + k = m + k -> n = m
H2: n + succ k = m + succ k
n = m
      rewrite !N_add_succ in H2.
UA: Univalence
PR: PropResizing
n, m, k: N
H1: n + k = m + k -> n = m
H2: succ (n + k) = succ (m + k)
n = m
      apply H1.
UA: Univalence
PR: PropResizing
n, m, k: N
H1: n + k = m + k -> n = m
H2: succ (n + k) = succ (m + k)
n + k = m + k
      exact (succ_inj _ _ H2).
  Qed.

  Definition N_add_cancel_zero_r@{} (n k : N) (H : k + n = n)
    : k = zero.
UA: Univalence
PR: PropResizing
n, k: N
H: k + n = n
k = zero
  Proof.
UA: Univalence
PR: PropResizing
n, k: N
H: k + n = n
k = zero
    refine (N_add_cancel_r k zero n _).
UA: Univalence
PR: PropResizing
n, k: N
H: k + n = n
k + n = zero + n
    rewrite H; symmetry.
UA: Univalence
PR: PropResizing
n, k: N
H: k + n = n
zero + n = n
    apply path_N, graph_add_zero_l.
  Qed.

  Definition N_add_one_r@{} (n : N) : n + one = succ n.
UA: Univalence
PR: PropResizing
n: N
n + one = succ n
  Proof.
UA: Univalence
PR: PropResizing
n: N
n + one = succ n
    apply path_N; cbn.
UA: Univalence
PR: PropResizing
n: N
graph_add n.1 graph_one = graph_succ n.1
    apply graph_add_one_succ.
  Qed.

  Definition N_add_one_l@{} (n : N) : one + n = succ n.
UA: Univalence
PR: PropResizing
n: N
one + n = succ n
  Proof.
UA: Univalence
PR: PropResizing
n: N
one + n = succ n
    revert n; refine (N_propind (fun m => one + m = succ m) _ _).
UA: Univalence
PR: PropResizing
one + zero = succ zero
UA: Univalence
PR: PropResizing
forall n : N,
one + n = succ n -> one + succ n = succ (succ n)
    -
UA: Univalence
PR: PropResizing
one + zero = succ zero rewrite N_add_zero_r.
UA: Univalence
PR: PropResizing
one = succ zero
      apply path_N.
UA: Univalence
PR: PropResizing
one.1 = (succ zero).1
      symmetry; apply graph_succ_zero.
    -
UA: Univalence
PR: PropResizing
forall n : N,
one + n = succ n -> one + succ n = succ (succ n) intros n H.
UA: Univalence
PR: PropResizing
n: N
H: one + n = succ n
one + succ n = succ (succ n)
      rewrite N_add_succ.
UA: Univalence
PR: PropResizing
n: N
H: one + n = succ n
succ (one + n) = succ (succ n)
      apply ap, H.
  Qed.

  Definition N_add_succ_l@{} (n m : N) : succ n + m = succ (n + m).
UA: Univalence
PR: PropResizing
n, m: N
succ n + m = succ (n + m)
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
succ n + m = succ (n + m)
    rewrite <- (N_add_one_r n).
UA: Univalence
PR: PropResizing
n, m: N
n + one + m = succ (n + m)
    rewrite N_add_assoc.
UA: Univalence
PR: PropResizing
n, m: N
n + (one + m) = succ (n + m)
    rewrite N_add_one_l.
UA: Univalence
PR: PropResizing
n, m: N
n + succ m = succ (n + m)
    apply N_add_succ.
  Qed.

  (** 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).
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n <= m)
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n <= m)
    apply ishprop_sigma_disjoint.
UA: Univalence
PR: PropResizing
n, m: N
forall x y : N, x + n = m -> y + n = m -> x = y
    intros x y e1 e2.
UA: Univalence
PR: PropResizing
n, m, x, y: N
e1: x + n = m
e2: y + n = m
x = y
    apply N_add_cancel_r with n.
UA: Univalence
PR: PropResizing
n, m, x, y: N
e1: x + n = m
e2: y + n = m
x + n = y + n path_via m.
  Qed.

  Definition N_zero_le@{} (n : N) : zero <= n.
UA: Univalence
PR: PropResizing
n: N
zero <= n
  Proof.
UA: Univalence
PR: PropResizing
n: N
zero <= n
    exists n.
UA: Univalence
PR: PropResizing
n: N
n + zero = n
    apply N_add_zero_r.
  Qed.

  Definition N_le_zero@{} (n : N) (H : n <= zero) : n = zero.
UA: Univalence
PR: PropResizing
n: N
H: n <= zero
n = zero
  Proof.
UA: Univalence
PR: PropResizing
n: N
H: n <= zero
n = zero
    destruct H as [k H].
UA: Univalence
PR: PropResizing
n, k: N
H: k + n = zero
n = zero
    apply pr1_path in H.
UA: Univalence
PR: PropResizing
n, k: N
H: (k + n).1 = zero.1
n = zero
    apply ((equiv_path_graph _ _)^-1), pr1 in H.
UA: Univalence
PR: PropResizing
n, k: N
H: vert (k + n).1 <~> vert zero.1
n = zero
    pose proof ((fun x => H (inr x)) : (vert n.1) -> Empty) as f.
UA: Univalence
PR: PropResizing
n, k: N
H: vert (k + n).1 <~> vert zero.1
f: vert n.1 -> Empty
n = zero
    apply path_N, equiv_path_graph.
UA: Univalence
PR: PropResizing
n, k: N
H: vert (k + n).1 <~> vert zero.1
f: vert n.1 -> Empty
{f : vert n.1 <~> vert zero.1 &
forall x y : vert n.1,
edge n.1 x y <-> edge zero.1 (f x) (f y)}
    srefine ((Build_Equiv _ _ f _);_); cbn.
UA: Univalence
PR: PropResizing
n, k: N
H: vert (k + n).1 <~> vert zero.1
f: vert n.1 -> Empty
forall x y : vert n.1,
edge n.1 x y <-> Empty_rec (f x)
    intros x y; destruct (f x).
  Qed.

  Instance contr_le_zero@{} : Contr {n:N & n <= zero}.
UA: Univalence
PR: PropResizing
Contr {n : N & n <= zero}
  Proof.
UA: Univalence
PR: PropResizing
Contr {n : N & n <= zero}
    apply (Build_Contr _ (exist (fun n => n <= zero) zero (N_zero_le zero))).
UA: Univalence
PR: PropResizing
forall y : {n : N & n <= zero},
(zero; N_zero_le zero) = y
    intros [n H].
UA: Univalence
PR: PropResizing
n: N
H: n <= zero
(zero; N_zero_le zero) = (n; H)
    apply path_sigma_hprop.
UA: Univalence
PR: PropResizing
n: N
H: n <= zero
(zero; N_zero_le zero).1 = (n; H).1
    exact (N_le_zero n H)^.
  Qed.

  Instance reflexive_N_le@{} : Reflexive N_le.
UA: Univalence
PR: PropResizing
Reflexive N_le
  Proof.
UA: Univalence
PR: PropResizing
Reflexive N_le
    intros n.
UA: Univalence
PR: PropResizing
n: N
n <= n
    exists zero.
UA: Univalence
PR: PropResizing
n: N
zero + n = n
    apply N_add_zero_l.
  Qed.

  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).
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n < m)
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
IsHProp (n < m)
    apply ishprop_sigma_disjoint.
UA: Univalence
PR: PropResizing
n, m: N
forall x y : N,
succ x + n = m -> succ y + n = m -> x = y
    intros x y e1 e2.
UA: Univalence
PR: PropResizing
n, m, x, y: N
e1: succ x + n = m
e2: succ y + n = m
x = y
    apply N_add_cancel_r with (succ n).
UA: Univalence
PR: PropResizing
n, m, x, y: N
e1: succ x + n = m
e2: succ y + n = m
x + succ n = y + succ n
    rewrite !N_add_succ, <-!N_add_succ_l.
UA: Univalence
PR: PropResizing
n, m, x, y: N
e1: succ x + n = m
e2: succ y + n = m
succ x + n = succ y + n
    path_via m.
  Qed.
  Local Existing Instance ishprop_N_lt.

  Definition N_lt_zero@{} (n : N) : ~(n < zero).
UA: Univalence
PR: PropResizing
n: N
~ (n < zero)
  Proof.
UA: Univalence
PR: PropResizing
n: N
~ (n < zero)
    unfold N_lt; intros [k H].
UA: Univalence
PR: PropResizing
n, k: N
H: succ k + n = zero
Empty
    apply pr1_path, (equiv_path_graph _ _)^-1, pr1 in H.
UA: Univalence
PR: PropResizing
n, k: N
H: vert (succ k + n).1 <~> vert zero.1
Empty
    exact (H (inl (inr tt))).
  Qed.

  Definition N_lt_irref@{} (n : N) : ~(n < n).
UA: Univalence
PR: PropResizing
n: N
~ (n < n)
  Proof.
UA: Univalence
PR: PropResizing
n: N
~ (n < n)
    revert n; apply N_propind@{p}.
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (~ (n < n))
UA: Univalence
PR: PropResizing
~ (zero < zero)
UA: Univalence
PR: PropResizing
forall n : N, ~ (n < n) -> ~ (succ n < succ n)
    -
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (~ (n < n)) intros n;exact istrunc_arrow@{p p p}.
    -
UA: Univalence
PR: PropResizing
~ (zero < zero) apply N_lt_zero.
    -
UA: Univalence
PR: PropResizing
forall n : N, ~ (n < n) -> ~ (succ n < succ n) intros n H [k K].
UA: Univalence
PR: PropResizing
n: N
H: ~ (n < n)
k: N
K: succ k + succ n = succ n
Empty
      apply H; exists k.
UA: Univalence
PR: PropResizing
n: N
H: ~ (n < n)
k: N
K: succ k + succ n = succ n
succ k + n = n
      rewrite N_add_succ in K.
UA: Univalence
PR: PropResizing
n: N
H: ~ (n < n)
k: N
K: succ (succ k + n) = succ n
succ k + n = n
      apply succ_inj; assumption.
  Qed.

  Definition N_le_eq_or_lt@{} (n m : N) (H : n <= m)
    : (n = m) + (n < m).
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
((n = m) + (n < m))%type
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
((n = m) + (n < m))%type
    assert (HP : IsHProp ((n = m) + (n < m))).
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
IsHProp ((n = m) + (n < m))
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
HP: IsHProp ((n = m) + (n < m))
((n = m) + (n < m))%type
    {
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
IsHProp ((n = m) + (n < m)) apply ishprop_sum; try exact _.
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
n = m -> n < m -> Empty
      intros [] [l K].
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
l: N
K: succ l + n = n
Empty
      apply N_add_cancel_zero_r in K.
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
l: N
K: succ l = zero
Empty
      symmetry in K; apply zero_neq_succ in K; assumption. }
UA: Univalence
PR: PropResizing
n, m: N
H: n <= m
HP: IsHProp ((n = m) + (n < m))
((n = m) + (n < m))%type
    destruct H as [k K].
UA: Univalence
PR: PropResizing
n, m, k: N
K: k + n = m
HP: IsHProp ((n = m) + (n < m))
((n = m) + (n < m))%type
    destruct (N_zero_or_succ k) as [k0|[l L]].
UA: Univalence
PR: PropResizing
n, m, k: N
K: k + n = m
HP: IsHProp ((n = m) + (n < m))
k0: k = zero
((n = m) + (n < m))%type
UA: Univalence
PR: PropResizing
n, m, k: N
K: k + n = m
HP: IsHProp ((n = m) + (n < m))
l: N
L: k = succ l
((n = m) + (n < m))%type
    -
UA: Univalence
PR: PropResizing
n, m, k: N
K: k + n = m
HP: IsHProp ((n = m) + (n < m))
k0: k = zero
((n = m) + (n < m))%type rewrite k0 in K.
UA: Univalence
PR: PropResizing
n, m, k: N
K: zero + n = m
HP: IsHProp ((n = m) + (n < m))
k0: k = zero
((n = m) + (n < m))%type
      rewrite (N_add_zero_l n) in K.
UA: Univalence
PR: PropResizing
n, m, k: N
K: n = m
HP: IsHProp ((n = m) + (n < m))
k0: k = zero
((n = m) + (n < m))%type
      exact (inl K).
    -
UA: Univalence
PR: PropResizing
n, m, k: N
K: k + n = m
HP: IsHProp ((n = m) + (n < m))
l: N
L: k = succ l
((n = m) + (n < m))%type rewrite L in K.
UA: Univalence
PR: PropResizing
n, m, k, l: N
K: succ l + n = m
HP: IsHProp ((n = m) + (n < m))
L: k = succ l
((n = m) + (n < m))%type
      exact (inr (l;K)).
  Qed.

  Definition N_succ_nlt@{} (n : N) : ~(succ n < n).
UA: Univalence
PR: PropResizing
n: N
~ (succ n < n)
  Proof.
UA: Univalence
PR: PropResizing
n: N
~ (succ n < n)
    revert n; apply N_propind@{p}.
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (~ (succ n < n))
UA: Univalence
PR: PropResizing
~ (succ zero < zero)
UA: Univalence
PR: PropResizing
forall n : N,
~ (succ n < n) -> ~ (succ (succ n) < succ n)
    -
UA: Univalence
PR: PropResizing
forall n : N, IsHProp (~ (succ n < n)) intros n;exact istrunc_arrow@{p p p}.
    -
UA: Univalence
PR: PropResizing
~ (succ zero < zero) apply N_lt_zero.
    -
UA: Univalence
PR: PropResizing
forall n : N,
~ (succ n < n) -> ~ (succ (succ n) < succ n) intros n H L.
UA: Univalence
PR: PropResizing
n: N
H: ~ (succ n < n)
L: succ (succ n) < succ n
Empty
      apply H; clear H.
UA: Univalence
PR: PropResizing
n: N
L: succ (succ n) < succ n
succ n < n
      destruct L as [k H].
UA: Univalence
PR: PropResizing
n, k: N
H: succ k + succ (succ n) = succ n
succ n < n
      exists k.
UA: Univalence
PR: PropResizing
n, k: N
H: succ k + succ (succ n) = succ n
succ k + succ n = n
      rewrite N_add_succ in H.
UA: Univalence
PR: PropResizing
n, k: N
H: succ (succ k + succ n) = succ n
succ k + succ n = n
      exact (succ_inj _ _ H).
  Qed.

  Definition N_lt_succ@{} (n : N) : n < succ n.
UA: Univalence
PR: PropResizing
n: N
n < succ n
  Proof.
UA: Univalence
PR: PropResizing
n: N
n < succ n
    exists zero.
UA: Univalence
PR: PropResizing
n: N
succ zero + n = succ n
    rewrite N_add_succ_l.
UA: Univalence
PR: PropResizing
n: N
succ (zero + n) = succ n
    apply ap, N_add_zero_l.
  Qed.

  Definition N_succ_lt@{} (n m : N) (H : n < m) : succ n < succ m.
UA: Univalence
PR: PropResizing
n, m: N
H: n < m
succ n < succ m
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
H: n < m
succ n < succ m
    destruct H as [k H].
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
succ n < succ m
    exists k.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
succ k + succ n = succ m
    rewrite N_add_succ.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
succ (succ k + n) = succ m
    apply ap; assumption.
  Qed.

  Definition N_lt_le@{} (n m : N) (H : n < m) : n <= m.
UA: Univalence
PR: PropResizing
n, m: N
H: n < m
n <= m
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
H: n < m
n <= m
    destruct H as [k K].
UA: Univalence
PR: PropResizing
n, m, k: N
K: succ k + n = m
n <= m
    exact (succ k; K).
  Qed.

  Definition N_lt_iff_succ_le@{} (n m : N) :
    (n < m) <-> (succ n <= m).
UA: Univalence
PR: PropResizing
n, m: N
n < m <-> succ n <= m
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
n < m <-> succ n <= m
    split; intros [k H]; exists k.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
k + succ n = m
UA: Univalence
PR: PropResizing
n, m, k: N
H: k + succ n = m
succ k + n = m
    -
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
k + succ n = m rewrite N_add_succ, <- N_add_succ_l.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = m
succ k + n = m
      assumption.
    -
UA: Univalence
PR: PropResizing
n, m, k: N
H: k + succ n = m
succ k + n = m rewrite N_add_succ_l, <- N_add_succ.
UA: Univalence
PR: PropResizing
n, m, k: N
H: k + succ n = m
k + succ n = m
      assumption.
  Qed.

  Definition N_lt_succ_iff_le@{} (n m : N) : (n < succ m) <-> (n <= m).
UA: Univalence
PR: PropResizing
n, m: N
n < succ m <-> n <= m
  Proof.
UA: Univalence
PR: PropResizing
n, m: N
n < succ m <-> n <= m
    split; intros [k H]; exists k.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = succ m
k + n = m
UA: Univalence
PR: PropResizing
n, m, k: N
H: k + n = m
succ k + n = succ m
    -
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ k + n = succ m
k + n = m rewrite N_add_succ_l in H.
UA: Univalence
PR: PropResizing
n, m, k: N
H: succ (k + n) = succ m
k + n = m
      exact (succ_inj _ _ H).
    -
UA: Univalence
PR: PropResizing
n, m, k: N
H: k + n = m
succ k + n = succ m rewrite N_add_succ_l; apply ap, H.
  Qed.

  Definition equiv_N_segment@{} (n : N)
    : { m : N & m <= n } <~> (sum@{p p} {m : N & m < n} Unit).
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n} <~> {m : N & m < n} + Unit
  Proof.
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n} <~> {m : N & m < n} + Unit
    srefine (equiv_adjointify _ _ _ _).
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n} -> {m : N & m < n} + Unit
UA: Univalence
PR: PropResizing
n: N
{m : N & m < n} + Unit -> {m : N & m <= n}
UA: Univalence
PR: PropResizing
n: N
?f o ?g == idmap
UA: Univalence
PR: PropResizing
n: N
?g o ?f == idmap
    -
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n} -> {m : N & m < n} + Unit intros mH.
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m <= n}
({m : N & m < n} + Unit)%type
      destruct (N_le_eq_or_lt mH.1 n mH.2) as [H0|Hs].
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m <= n}
H0: mH.1 = n
({m : N & m < n} + Unit)%type
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m <= n}
Hs: mH.1 < n
({m : N & m < n} + Unit)%type
      +
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m <= n}
H0: mH.1 = n
({m : N & m < n} + Unit)%type exact (inr tt).
      +
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m <= n}
Hs: mH.1 < n
({m : N & m < n} + Unit)%type exact (inl (mH.1;Hs)).
    -
UA: Univalence
PR: PropResizing
n: N
{m : N & m < n} + Unit -> {m : N & m <= n} intros [mH|?].
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m < n}
{m : N & m <= n}
UA: Univalence
PR: PropResizing
n: N
u: Unit
{m : N & m <= n}
      +
UA: Univalence
PR: PropResizing
n: N
mH: {m : N & m < n}
{m : N & m <= n} exact (mH.1; N_lt_le mH.1 n mH.2).
      +
UA: Univalence
PR: PropResizing
n: N
u: Unit
{m : N & m <= n} exists n; reflexivity.
    -
UA: Univalence
PR: PropResizing
n: N
(fun mH : {m : N & m <= n} =>
 let s := N_le_eq_or_lt mH.1 n mH.2 in
 match s with
 | inl p => (fun _ : mH.1 = n => inr tt) p
 | inr n0 => (fun Hs : mH.1 < n => inl (mH.1; Hs)) n0
 end)
o (fun X : {m : N & m < n} + Unit =>
   match X with
   | inl s =>
       (fun mH : {m : N & m < n} =>
        (mH.1; N_lt_le mH.1 n mH.2)) s
   | inr u => unit_name (n; reflexive_N_le n) u
   end) == idmap 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) ]]).
    -
UA: Univalence
PR: PropResizing
n: N
(fun X : {m : N & m < n} + Unit =>
 match X with
 | inl s =>
     (fun mH : {m : N & m < n} =>
      (mH.1; N_lt_le mH.1 n mH.2)) s
 | inr u => unit_name (n; reflexive_N_le n) u
 end)
o (fun mH : {m : N & m <= n} =>
   let s := N_le_eq_or_lt mH.1 n mH.2 in
   match s with
   | inl p => (fun _ : mH.1 = n => inr tt) p
   | inr n0 =>
       (fun Hs : mH.1 < n => inl (mH.1; Hs)) n0
   end) == idmap 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 ]).
  Defined.

  Definition equiv_N_segment_succ@{} (n : N)
    : { m : N & m <= succ n } <~> @sum@{p p} {m : N & m <= n} Unit.
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= succ n} <~> {m : N & m <= n} + Unit
  Proof.
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= succ n} <~> {m : N & m <= n} + Unit
    refine (_ oE equiv_N_segment (succ n)).
UA: Univalence
PR: PropResizing
n: N
{m : N & m < succ n} + Unit <~>
{m : N & m <= n} + Unit
    apply equiv_functor_sum_r.
UA: Univalence
PR: PropResizing
n: N
{m : N & m < succ n} <~> {m : N & m <= n}
    apply equiv_functor_sigma_id.
UA: Univalence
PR: PropResizing
n: N
forall a : N, a < succ n <~> a <= n
    intros m; apply equiv_iff_hprop_uncurried, N_lt_succ_iff_le.
  Defined.

  (** 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.
UA: Univalence
PR: PropResizing
n: N
mh: {m : N & m <= n}
((equiv_N_segment_succ n)^-1 (inl mh)).1 = mh.1
  Proof.
UA: Univalence
PR: PropResizing
n: N
mh: {m : N & m <= n}
((equiv_N_segment_succ n)^-1 (inl mh)).1 = mh.1
    reflexivity.
  Qed.

  Definition equiv_N_segment_lt_succ@{} (n : N)
    : { m : N & m < succ n } <~> {m : N & m <= n}.
UA: Univalence
PR: PropResizing
n: N
{m : N & m < succ n} <~> {m : N & m <= n}
  Proof.
UA: Univalence
PR: PropResizing
n: N
{m : N & m < succ n} <~> {m : N & m <= n}
    apply equiv_functor_sigma_id.
UA: Univalence
PR: PropResizing
n: N
forall a : N, a < succ n <~> a <= n
    intros; apply equiv_iff_hprop; apply N_lt_succ_iff_le.
  Defined.

  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}.
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n}
  Proof.
UA: Univalence
PR: PropResizing
n: N
{m : N & m <= n}
    exists n.
UA: Univalence
PR: PropResizing
n: N
n <= n
    reflexivity.
  Defined.

  (** Now we're finally ready to prove recursion. *)
  Section NRec.
    (** 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]. *)
    Universes x nr.
    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).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr (partial_Nrec zero)
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr (partial_Nrec zero)
      unfold partial_Nrec.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr
  {f : {m : N & m <= zero} -> X &
  (f (zero_seg zero) = x0) *
  (forall mh : {m : N & m < zero},
   f (succ_seg zero mh) =
   xs (f ((equiv_N_segment zero)^-1 (inl mh))))}
      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))))} _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f0: {f : {m : N & m <= zero} -> X &
f (zero_seg zero) = x0}
mh: {m : N & m < zero}
IsEquiv (equiv_N_segment zero)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
{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)))} <~>
{f : {m : N & m <= zero} -> X &
(f (zero_seg zero) = x0) *
(forall mh : {m : N & m < zero},
 f (succ_seg zero mh) =
 xs (f ((equiv_N_segment zero)^-1 (inl mh))))}
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr
  {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)))}
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f0: {f : {m : N & m <= zero} -> X &
f (zero_seg zero) = x0}
mh: {m : N & m < zero}
IsEquiv (equiv_N_segment zero) exact _.
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
{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)))} <~>
{f : {m : N & m <= zero} -> X &
(f (zero_seg zero) = x0) *
(forall mh : {m : N & m < zero},
 f (succ_seg zero mh) =
 xs (f ((equiv_N_segment zero)^-1 (inl mh))))} refine (_ oE equiv_inverse (equiv_sigma_assoc _ _)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
{a : {m : N & m <= zero} -> X &
{p : a (zero_seg zero) = x0 &
forall mh : {m : N & m < zero},
(a; p).1 (succ_seg zero mh) =
xs ((a; p).1 ((equiv_N_segment zero)^-1 (inl mh)))}} <~>
{f : {m : N & m <= zero} -> X &
(f (zero_seg zero) = x0) *
(forall mh : {m : N & m < zero},
 f (succ_seg zero mh) =
 xs (f ((equiv_N_segment zero)^-1 (inl mh))))}
        apply equiv_functor_sigma_id; intros f.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: {m : N & m <= zero} -> X
{p : f (zero_seg zero) = x0 &
forall mh : {m : N & m < zero},
(f; p).1 (succ_seg zero mh) =
xs ((f; p).1 ((equiv_N_segment zero)^-1 (inl mh)))} <~>
(f (zero_seg zero) = x0) *
(forall mh : {m : N & m < zero},
 f (succ_seg zero mh) =
 xs (f ((equiv_N_segment zero)^-1 (inl mh))))
        cbn; apply equiv_sigma_prod0.
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr
  {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 (@istrunc_sigma@{nr nr nr} _ _ _ _ _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr
  {f : {m : N & m <= zero} -> X &
  f (zero_seg zero) = x0}
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
forall
a : {f : {m : N & m <= zero} -> X &
    f (zero_seg zero) = x0},
Contr
  (forall mh : {m : N & m < zero},
   a.1 (succ_seg zero mh) =
   xs (a.1 ((equiv_N_segment zero)^-1 (inl mh))))
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr
  {f : {m : N & m <= zero} -> X &
  f (zero_seg zero) = x0} srefine (Build_Contr _ _ _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
{f : {m : N & m <= zero} -> X &
f (zero_seg zero) = x0}
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
forall
y : {f : {m : N & m <= zero} -> X &
    f (zero_seg zero) = x0}, ?center = y
          *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
{f : {m : N & m <= zero} -> X &
f (zero_seg zero) = x0} exists (fun _ => x0); reflexivity.
          *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
forall
y : {f : {m : N & m <= zero} -> X &
    f (zero_seg zero) = x0},
(fun _ : {m : N & m <= zero} => x0; 1) = y intros [g H].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(fun _ : {m : N & m <= zero} => x0; 1) = (g; H)
            srefine (path_sigma _ _ _ _ _); cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(fun _ : {m : N & m <= zero} => x0) = g
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
transport
  (fun f : {m : N & m <= zero} -> X =>
   f (zero_seg zero) = x0) ?Goal0 1 = H
            {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(fun _ : {m : N & m <= zero} => x0) = g apply path_forall; intros m.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
m: {m : N & m <= zero}
x0 = g m
              exact (H^ @ ap g (path_ishprop _ _)). }
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
transport
  (fun f : {m : N & m <= zero} -> X =>
   f (zero_seg zero) = x0)
  (path_forall (fun _ : {m : N & m <= zero} => x0) g
     ((fun m : {m : N & m <= zero} =>
       H^ @ ap g (path_ishprop (zero_seg zero) m))
      :
      (fun _ : {m : N & m <= zero} => x0) == g)) 1 = H
            {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
transport
  (fun f : {m : N & m <= zero} -> X =>
   f (zero_seg zero) = x0)
  (path_forall (fun _ : {m : N & m <= zero} => x0) g
     ((fun m : {m : N & m <= zero} =>
       H^ @ ap g (path_ishprop (zero_seg zero) m))
      :
      (fun _ : {m : N & m <= zero} => x0) == g)) 1 = H rewrite transport_paths_Fl.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap
   (fun x : {m : N & m <= zero} -> X =>
    x (zero_seg zero))
   (path_forall (fun _ : {m : N & m <= zero} => x0) g
      (fun m : {m : N & m <= zero} =>
       H^ @ ap g (path_ishprop (zero_seg zero) m))))^ @
1 = H
              rewrite ap_apply_l.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap10
   (path_forall (fun _ : {m : N & m <= zero} => x0) g
      (fun m : {m : N & m <= zero} =>
       H^ @ ap g (path_ishprop (zero_seg zero) m)))
   (zero_seg zero))^ @ 1 = H
              rewrite ap10_path_forall.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(H^ @
 ap g (path_ishprop (zero_seg zero) (zero_seg zero)))^ @
1 = H
              rewrite inv_pp, inv_V, concat_p1.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap g (path_ishprop (zero_seg zero) (zero_seg zero)))^ @
H = H
              transitivity ((ap g 1)^ @ H).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap g (path_ishprop (zero_seg zero) (zero_seg zero)))^ @
H = (ap g 1)^ @ H
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap g 1)^ @ H = H
              -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap g (path_ishprop (zero_seg zero) (zero_seg zero)))^ @
H = (ap g 1)^ @ H apply whiskerR, ap, ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
path_ishprop (zero_seg zero) (zero_seg zero) = 1
                apply path_ishprop.
              -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
g: {m : N & m <= zero} -> X
H: g (zero_seg zero) = x0
(ap g 1)^ @ H = H apply concat_1p. }
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
forall
a : {f : {m : N & m <= zero} -> X &
    f (zero_seg zero) = x0},
Contr
  (forall mh : {m : N & m < zero},
   a.1 (succ_seg zero mh) =
   xs (a.1 ((equiv_N_segment zero)^-1 (inl mh)))) intros [f H].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: {m : N & m <= zero} -> X
H: f (zero_seg zero) = x0
Contr
  (forall mh : {m : N & m < zero},
   (f; H).1 (succ_seg zero mh) =
   xs ((f; H).1 ((equiv_N_segment zero)^-1 (inl mh))))
          apply (Build_Contr _ (fun mh => Empty_rec (N_lt_zero mh.1 mh.2))).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: {m : N & m <= zero} -> X
H: f (zero_seg zero) = x0
forall
y : forall mh : {m : N & m < zero},
    (f; H).1 (succ_seg zero mh) =
    xs ((f; H).1 ((equiv_N_segment zero)^-1 (inl mh))),
(fun mh : {m : N & m < zero} =>
 Empty_rec (N_lt_zero mh.1 mh.2)) = y
          intros g.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: {m : N & m <= zero} -> X
H: f (zero_seg zero) = x0
g: forall mh : {m : N & m < zero},
(f; H).1 (succ_seg zero mh) =
xs ((f; H).1 ((equiv_N_segment zero)^-1 (inl mh)))
(fun mh : {m : N & m < zero} =>
 Empty_rec (N_lt_zero mh.1 mh.2)) = g
          apply path_forall; intros m.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: {m : N & m <= zero} -> X
H: f (zero_seg zero) = x0
g: forall mh : {m : N & m < zero},
(f; H).1 (succ_seg zero mh) =
xs ((f; H).1 ((equiv_N_segment zero)^-1 (inl mh)))
m: {m : N & m < zero}
Empty_rec (N_lt_zero m.1 m.2) = g m
          destruct (N_lt_zero m.1 m.2).
    Qed.
    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).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} -> X) * X <~>
({m : N & m <= succ n} -> X)
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({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 _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} + Unit -> X) <~>
({m : N & m <= succ n} -> X)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} -> X) * X <~>
({m : N & m <= n} -> X) * (Unit -> X)
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} + Unit -> X) <~>
({m : N & m <= succ n} -> X) apply equiv_precompose'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{m : N & m <= succ n} <~> {m : N & m <= n} + Unit
        apply equiv_N_segment_succ.
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} -> X) * X <~>
({m : N & m <= n} -> X) * (Unit -> X) apply equiv_functor_prod_l.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
X <~> (Unit -> X)
        apply equiv_unit_rec@{x nr}.
    Defined.

    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)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
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 (succ n) H) =
f (m; fst (N_lt_succ_iff_le m n) H)
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
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 (succ n) H) =
f (m; fst (N_lt_succ_iff_le m n) H)
      cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match
       N_le_eq_or_lt m (succ n) (N_lt_le m (succ n) H)
     with
     | inl _ => inr tt
     | inr n0 => inl (m; n0)
     end) = f (m; fst (N_lt_succ_iff_le m n) H)
      generalize (N_le_eq_or_lt m (succ n) (N_lt_le m (succ n) H)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
forall s : (m = succ n) + (m < succ n),
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match s with
     | inl _ => inr tt
     | inr n0 => inl (m; n0)
     end) = f (m; fst (N_lt_succ_iff_le m n) H)
      intros [E|L].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
E: m = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) =
f (m; fst (N_lt_succ_iff_le m n) H)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
L: m < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (m; L))) =
f (m; fst (N_lt_succ_iff_le m n) H)
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
E: m = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) =
f (m; fst (N_lt_succ_iff_le m n) H) apply Empty_rec.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
E: m = succ n
Empty
        rewrite E in H.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: succ n < succ n
f: {m : N & m <= n} -> X
xsn: X
E: m = succ n
Empty
        exact (N_lt_irref _ H).
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
L: m < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (m; L))) =
f (m; fst (N_lt_succ_iff_le m n) H) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n, m: N
H: m < succ n
f: {m : N & m <= n} -> X
xsn: X
L: m < succ n
f
  (functor_sigma idmap
     (fun a : N => fst (N_lt_succ_iff_le a n)) (m; L)) =
f (m; fst (N_lt_succ_iff_le m n) H)
        apply ap, path_sigma_hprop; reflexivity.
    Qed.

    (** And here, essentially, is the inductive step. *)
    Local Definition partial_Nrec_succ0 (n : N)
      : partial_Nrec n <~> partial_Nrec (succ n).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
partial_Nrec n <~> partial_Nrec (succ n)
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
partial_Nrec n <~> partial_Nrec (succ n)
      unfold partial_Nrec.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{f : {m : N & m <= succ n} -> X &
(f (zero_seg (succ n)) = x0) *
(forall mh : {m : N & m < succ n},
 f (succ_seg (succ n) mh) =
 xs (f ((equiv_N_segment (succ n))^-1 (inl mh))))}
      srefine (equiv_functor_sigma' (equiv_N_segment_succ_maps n) _ oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} -> X) * X -> Type
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
forall a : ({m : N & m <= n} -> X) * X,
?P a <~>
(fun f : {m : N & m <= succ n} -> X =>
 (f (zero_seg (succ n)) = x0) *
 (forall mh : {m : N & m < succ n},
  f (succ_seg (succ n) mh) =
  xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))))
  (equiv_N_segment_succ_maps n a)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{x : _ & ?P x}
      {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
({m : N & m <= n} -> X) * X -> Type intros [f xsn].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
Type
        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))))). }
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
forall a : ({m : N & m <= n} -> X) * X,
(fun X0 : ({m : N & m <= n} -> X) * X =>
 (fun (f : {m : N & m <= n} -> X) (xsn : X) =>
  (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))))) (fst X0) (snd X0)) a <~>
(fun f : {m : N & m <= succ n} -> X =>
 (f (zero_seg (succ n)) = x0) *
 (forall mh : {m : N & m < succ n},
  f (succ_seg (succ n) mh) =
  xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))))
  (equiv_N_segment_succ_maps n a)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{X0 : ({m : N & m <= n} -> X) * X &
(fun (f : {m : N & m <= n} -> X) (xsn : X) =>
 (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))))) (fst X0) (snd X0)}
      {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
forall a : ({m : N & m <= n} -> X) * X,
(fun X0 : ({m : N & m <= n} -> X) * X =>
 (fun (f : {m : N & m <= n} -> X) (xsn : X) =>
  (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))))) (fst X0) (snd X0)) a <~>
(fun f : {m : N & m <= succ n} -> X =>
 (f (zero_seg (succ n)) = x0) *
 (forall mh : {m : N & m < succ n},
  f (succ_seg (succ n) mh) =
  xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))))
  (equiv_N_segment_succ_maps n a) intros [f xsn].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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)))) <~>
(equiv_N_segment_succ_maps n (f, xsn)
   (zero_seg (succ n)) = x0) *
(forall mh : {m : N & m < succ n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n) mh) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1 (inl mh))))
        apply equiv_functor_prod'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
f (zero_seg n) = x0 <~>
equiv_N_segment_succ_maps n (f, xsn)
  (zero_seg (succ n)) = x0
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall mh : {m : N & m < succ n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n) mh) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1 (inl mh))))
        {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
f (zero_seg n) = x0 <~>
equiv_N_segment_succ_maps n (f, xsn)
  (zero_seg (succ n)) = x0 apply equiv_concat_l.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
equiv_N_segment_succ_maps n (f, xsn)
  (zero_seg (succ n)) = f (zero_seg n)
          cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match
       N_le_eq_or_lt zero (succ n)
         (N_zero_le (succ n))
     with
     | inl _ => inr tt
     | inr n0 => inl (zero; n0)
     end) = f (zero_seg n)
          generalize (N_le_eq_or_lt zero (succ n) (N_zero_le (succ n))).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
forall s : (zero = succ n) + (zero < succ n),
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match s with
     | inl _ => inr tt
     | inr n0 => inl (zero; n0)
     end) = f (zero_seg n)
          intros [H0|Hs].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
H0: zero = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) = f (zero_seg n)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
Hs: zero < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (zero; Hs))) = f (zero_seg n)
          +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
H0: zero = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) = f (zero_seg n) destruct (zero_neq_succ n (H0)).
          +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
Hs: zero < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (zero; Hs))) = f (zero_seg n) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
Hs: zero < succ n
f
  (functor_sigma idmap
     (fun a : N => fst (N_lt_succ_iff_le a n))
     (zero; Hs)) = f (zero_seg n) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
Hs: zero < succ n
functor_sigma idmap
  (fun a : N => fst (N_lt_succ_iff_le a n)) (zero; Hs) =
zero_seg n
            apply path_sigma_hprop; reflexivity. }
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall mh : {m : N & m < succ n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n) mh) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1 (inl mh))))
        {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall mh : {m : N & m < succ n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n) mh) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1 (inl mh)))) srefine ((equiv_functor_forall_pb
                     (equiv_N_segment_lt_succ n)^-1)^-1 oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall b : {m : N & m <= n},
 (fun a : {m : N & m < succ n} =>
  equiv_N_segment_succ_maps n (f, xsn)
    (succ_seg (succ n) a) =
  xs
    (equiv_N_segment_succ_maps n (f, xsn)
       ((equiv_N_segment (succ n))^-1 (inl a))))
   ((equiv_N_segment_lt_succ n)^-1%equiv b))
          srefine ((equiv_functor_forall_pb (equiv_N_segment n)^-1)^-1 oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall b : {m : N & m < n} + Unit,
 (fun a : {m : N & m <= n} =>
  (fun a0 : {m : N & m < succ n} =>
   equiv_N_segment_succ_maps n (f, xsn)
     (succ_seg (succ n) a0) =
   xs
     (equiv_N_segment_succ_maps n (f, xsn)
        ((equiv_N_segment (succ n))^-1 (inl a0))))
    ((equiv_N_segment_lt_succ n)^-1%equiv a))
   ((equiv_N_segment n)^-1%equiv b))
          srefine (equiv_sum_ind _ oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(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))) <~>
(forall a : {m : N & m < n},
 (fun s : {m : N & m < n} + Unit =>
  (fun a0 : {m : N & m <= n} =>
   (fun a1 : {m : N & m < succ n} =>
    equiv_N_segment_succ_maps n (f, xsn)
      (succ_seg (succ n) a1) =
    xs
      (equiv_N_segment_succ_maps n (f, xsn)
         ((equiv_N_segment (succ n))^-1 (inl a1))))
     ((equiv_N_segment_lt_succ n)^-1%equiv a0))
    ((equiv_N_segment n)^-1%equiv s)) (inl a)) *
(forall b : Unit,
 (fun s : {m : N & m < n} + Unit =>
  (fun a : {m : N & m <= n} =>
   (fun a0 : {m : N & m < succ n} =>
    equiv_N_segment_succ_maps n (f, xsn)
      (succ_seg (succ n) a0) =
    xs
      (equiv_N_segment_succ_maps n (f, xsn)
         ((equiv_N_segment (succ n))^-1 (inl a0))))
     ((equiv_N_segment_lt_succ n)^-1%equiv a))
    ((equiv_N_segment n)^-1%equiv s)) (inr b))
          apply equiv_functor_prod'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(forall mh : {m : N & m < n},
 f (succ_seg n mh) =
 xs (f ((equiv_N_segment n)^-1 (inl mh)))) <~>
(forall a : {m : N & m < n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n)
      ((equiv_N_segment_lt_succ n)^-1%equiv
         ((equiv_N_segment n)^-1%equiv (inl a)))) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1
         (inl
            ((equiv_N_segment_lt_succ n)^-1%equiv
               ((equiv_N_segment n)^-1%equiv (inl a)))))))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
xsn = xs (f (refl_seg n)) <~>
(forall b : Unit,
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n)
      ((equiv_N_segment_lt_succ n)^-1%equiv
         ((equiv_N_segment n)^-1%equiv (inr b)))) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1
         (inl
            ((equiv_N_segment_lt_succ n)^-1%equiv
               ((equiv_N_segment n)^-1%equiv (inr b)))))))
          -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
(forall mh : {m : N & m < n},
 f (succ_seg n mh) =
 xs (f ((equiv_N_segment n)^-1 (inl mh)))) <~>
(forall a : {m : N & m < n},
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n)
      ((equiv_N_segment_lt_succ n)^-1%equiv
         ((equiv_N_segment n)^-1%equiv (inl a)))) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1
         (inl
            ((equiv_N_segment_lt_succ n)^-1%equiv
               ((equiv_N_segment n)^-1%equiv (inl a))))))) apply equiv_functor_forall_id; intros [m H].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
f (succ_seg n (m; H)) =
xs (f ((equiv_N_segment n)^-1 (inl (m; H)))) <~>
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv (inl (m; H))))) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inl (m; H)))))))
            apply equiv_concat_lr.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv (inl (m; H))))) =
f (succ_seg n (m; H))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
xs (f ((equiv_N_segment n)^-1 (inl (m; H)))) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inl (m; H)))))))
            +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv (inl (m; H))))) =
f (succ_seg n (m; H)) transitivity ((equiv_N_segment_succ_maps n)
                              (f,xsn)
                              (succ m; N_lt_le _ _ (N_succ_lt m n H))).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv (inl (m; H))))) =
equiv_N_segment_succ_maps n (f, xsn)
  (succ m;
  N_lt_le (succ m) (succ n) (N_succ_lt m n H))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ m;
  N_lt_le (succ m) (succ n) (N_succ_lt m n H)) =
f (succ_seg n (m; H))
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv (inl (m; H))))) =
equiv_N_segment_succ_maps n (f, xsn)
  (succ m;
  N_lt_le (succ m) (succ n) (N_succ_lt m n H)) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
succ_seg (succ n)
  ((equiv_N_segment_lt_succ n)^-1%equiv
     ((equiv_N_segment n)^-1%equiv (inl (m; H)))) =
(succ m; N_lt_le (succ m) (succ n) (N_succ_lt m n H)) apply path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
(succ_seg (succ n)
   ((equiv_N_segment_lt_succ n)^-1%equiv
      ((equiv_N_segment n)^-1%equiv (inl (m; H))))).1 =
(succ m; N_lt_le (succ m) (succ n) (N_succ_lt m n H)).1 reflexivity.
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
equiv_N_segment_succ_maps n (f, xsn)
  (succ m;
  N_lt_le (succ m) (succ n) (N_succ_lt m n H)) =
f (succ_seg n (m; H)) rewrite equiv_seg_succ.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
f
  (succ m;
  fst (N_lt_succ_iff_le (succ m) n) (N_succ_lt m n H)) =
f (succ_seg n (m; H))
                apply ap, path_sigma_hprop; reflexivity.
            +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
xs (f ((equiv_N_segment n)^-1 (inl (m; H)))) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inl (m; H))))))) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
f ((equiv_N_segment n)^-1 (inl (m; H))) =
equiv_N_segment_succ_maps n (f, xsn)
  ((equiv_N_segment (succ n))^-1
     (inl
        ((equiv_N_segment_lt_succ n)^-1%equiv
           ((equiv_N_segment n)^-1%equiv (inl (m; H))))))
              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.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match
       N_le_eq_or_lt m (succ n)
         (N_lt_le m (succ n)
            (snd (N_lt_succ_iff_le m n)
               (N_lt_le m n H)))
     with
     | inl _ => inr tt
     | inr n0 => inl (m; n0)
     end)
              match goal with
              | [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
              end.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
forall s : (m = succ n) + (m < succ n),
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match s with
     | inl _ => inr tt
     | inr n0 => inl (m; n0)
     end)
              intros [L|L].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
L: m = succ n
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
L: m < succ n
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (m; L)))
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
L: m = succ n
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) apply Empty_rec; rewrite L in H.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: succ n < n
L: m = succ n
Empty
                exact (N_succ_nlt n H).
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
L: m < succ n
f (m; N_lt_le m n H) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (m; L))) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
m: N
H: m < n
L: m < succ n
f (m; N_lt_le m n H) =
f
  (functor_sigma idmap
     (fun a : N => fst (N_lt_succ_iff_le a n)) (m; L)) apply ap, path_sigma_hprop; reflexivity.
          -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
xsn = xs (f (refl_seg n)) <~>
(forall b : Unit,
 equiv_N_segment_succ_maps n (f, xsn)
   (succ_seg (succ n)
      ((equiv_N_segment_lt_succ n)^-1%equiv
         ((equiv_N_segment n)^-1%equiv (inr b)))) =
 xs
   (equiv_N_segment_succ_maps n (f, xsn)
      ((equiv_N_segment (succ n))^-1
         (inl
            ((equiv_N_segment_lt_succ n)^-1%equiv
               ((equiv_N_segment n)^-1%equiv (inr b))))))) refine ((equiv_contr_forall _)^-1 oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
xsn = xs (f (refl_seg n)) <~>
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv
           (inr (center Unit))))) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inr (center Unit)))))))
            apply equiv_concat_lr.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv
           (inr (center Unit))))) = xsn
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
xs (f (refl_seg n)) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inr (center Unit)))))))
            +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
equiv_N_segment_succ_maps n (f, xsn)
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1%equiv
        ((equiv_N_segment n)^-1%equiv
           (inr (center Unit))))) = xsn cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match
       N_le_eq_or_lt (succ n) (succ n)
         (fst (N_lt_iff_succ_le n (succ n))
            (snd (N_lt_succ_iff_le n n)
               (reflexive_N_le n)))
     with
     | inl _ => inr tt
     | inr n0 => inl (succ n; n0)
     end) = xsn
              match goal with
              | [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
              end.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
forall s : (succ n = succ n) + (succ n < succ n),
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match s with
     | inl _ => inr tt
     | inr n0 => inl (succ n; n0)
     end) = xsn
              intros [L|L].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: succ n = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) = xsn
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: succ n < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (succ n; L))) = xsn
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: succ n = succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) = xsn reflexivity.
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: succ n < succ n
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (succ n; L))) = xsn case (N_lt_irref _ L).
            +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
xs (f (refl_seg n)) =
xs
  (equiv_N_segment_succ_maps n (f, xsn)
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1%equiv
              ((equiv_N_segment n)^-1%equiv
                 (inr (center Unit))))))) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
f (refl_seg n) =
equiv_N_segment_succ_maps n (f, xsn)
  ((equiv_N_segment (succ n))^-1
     (inl
        ((equiv_N_segment_lt_succ n)^-1%equiv
           ((equiv_N_segment n)^-1%equiv
              (inr (center Unit))))))
              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].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match
       N_le_eq_or_lt n (succ n)
         (N_lt_le n (succ n)
            (snd (N_lt_succ_iff_le n n)
               (reflexive_N_le n)))
     with
     | inl _ => inr tt
     | inr n0 => inl (n; n0)
     end)
              match goal with
              | [ |- context[match ?L with | inl _ => inr tt | inr Hs => inl (?k; Hs) end] ] => generalize L
              end.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
forall s : (n = succ n) + (n < succ n),
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap
     match s with
     | inl _ => inr tt
     | inr n0 => inl (n; n0)
     end)
              intros [L|L].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n = succ n
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n < succ n
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (n; L)))
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n = succ n
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inr tt)) case (N_neq_succ n L).
              *
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n < succ n
f (refl_seg n) =
sum_ind_uncurried
  (fun _ : {m : N & m <= n} + Unit => X)
  (functor_prod idmap (Unit_ind (A:=unit_name X))
     (f, xsn))
  (functor_sum
     (functor_sigma idmap
        (fun a : N => fst (N_lt_succ_iff_le a n)))
     idmap (inl (n; L))) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n < succ n
f (refl_seg n) =
f
  (functor_sigma idmap
     (fun a : N => fst (N_lt_succ_iff_le a n)) (n; L))
                apply ap, path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
xsn: X
L: n < succ n
(refl_seg n).1 =
(functor_sigma idmap
   (fun a : N => fst (N_lt_succ_iff_le a n)) (n; L)).1 reflexivity. } }
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{X0 : ({m : N & m <= n} -> X) * X &
(fun (f : {m : N & m <= n} -> X) (xsn : X) =>
 (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))))) (fst X0) (snd X0)}
      {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{X0 : ({m : N & m <= n} -> X) * X &
(fun (f : {m : N & m <= n} -> X) (xsn : X) =>
 (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))))) (fst X0) (snd X0)} refine (equiv_sigma_prod _ oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
{f : {m : N & m <= n} -> X &
(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))))} <~>
{a : {m : N & m <= n} -> X &
{b : X &
(a (zero_seg n) = x0) *
((forall mh : {m : N & m < n},
  a (succ_seg n mh) =
  xs (a ((equiv_N_segment n)^-1 (inl mh)))) *
 (b = xs (a (refl_seg n))))}}
        apply equiv_functor_sigma_id.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
forall a : {m : N & m <= n} -> X,
(a (zero_seg n) = x0) *
(forall mh : {m : N & m < n},
 a (succ_seg n mh) =
 xs (a ((equiv_N_segment n)^-1 (inl mh)))) <~>
{b : X &
(a (zero_seg n) = x0) *
((forall mh : {m : N & m < n},
  a (succ_seg n mh) =
  xs (a ((equiv_N_segment n)^-1 (inl mh)))) *
 (b = xs (a (refl_seg n))))} intros f.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
(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)))) <~>
{b : X &
(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)))) *
 (b = xs (f (refl_seg n))))}
        refine (equiv_functor_sigma_id (fun b:X => equiv_sigma_prod0 _ _) oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
(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)))) <~>
{b : X &
{_ : 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)))) *
(b = xs (f (refl_seg n)))}}
        refine (equiv_sigma_symm _ oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
(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)))) <~>
{_ : f (zero_seg n) = x0 &
{b : X &
(forall mh : {m : N & m < n},
 f (succ_seg n mh) =
 xs (f ((equiv_N_segment n)^-1 (inl mh)))) *
(b = xs (f (refl_seg n)))}}
        refine (_ oE (equiv_sigma_prod0 _ _)^-1).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
{_ : 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)))} <~>
{_ : f (zero_seg n) = x0 &
{b : X &
(forall mh : {m : N & m < n},
 f (succ_seg n mh) =
 xs (f ((equiv_N_segment n)^-1 (inl mh)))) *
(b = xs (f (refl_seg n)))}}
        apply equiv_functor_sigma_id; intros f0.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
f0: 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)))) <~>
{b : X &
(forall mh : {m : N & m < n},
 f (succ_seg n mh) =
 xs (f ((equiv_N_segment n)^-1 (inl mh)))) *
(b = xs (f (refl_seg n)))}
        refine (equiv_functor_sigma_id (fun b:X => equiv_sigma_prod0 _ _) oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
f0: 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)))) <~>
{b : X &
{_
: forall mh : {m : N & m < n},
  f (succ_seg n mh) =
  xs (f ((equiv_N_segment n)^-1 (inl mh))) &
b = xs (f (refl_seg n))}}
        refine (equiv_sigma_symm _ oE _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= n} -> X
f0: 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)))) <~>
{_
: forall mh : {m : N & m < n},
  f (succ_seg n mh) =
  xs (f ((equiv_N_segment n)^-1 (inl mh))) &
{b : X & b = xs (f (refl_seg n))}}
        exact ((equiv_sigma_contr _)^-1%equiv). }
    Defined.
    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).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
Contr (partial_Nrec n)
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
Contr (partial_Nrec n)
      revert n; apply N_propind; try exact _.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
forall n : N,
Contr (partial_Nrec n) ->
Contr (partial_Nrec (succ n))
      intros n H.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
H: Contr (partial_Nrec n)
Contr (partial_Nrec (succ n))
      refine (istrunc_equiv_istrunc _ (partial_Nrec_succ n)).
    Qed.

    (** This will be useful later. *)
    Local Definition partial_Nrec_restr@{} (n : N)
      : partial_Nrec (succ n) -> partial_Nrec n.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
partial_Nrec (succ n) -> partial_Nrec n
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
partial_Nrec (succ n) -> partial_Nrec n
      intros f.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: partial_Nrec (succ n)
partial_Nrec n
      destruct f as [f [f0 fs]].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
partial_Nrec n
      exists (fun mh => f ((equiv_N_segment_succ n)^-1 (inl mh))).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
(f ((equiv_N_segment_succ n)^-1 (inl (zero_seg n))) =
 x0) *
(forall mh : {m : N & m < n},
 f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
 xs
   (f
      ((equiv_N_segment_succ n)^-1
         (inl ((equiv_N_segment n)^-1 (inl mh))))))
      split.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
f ((equiv_N_segment_succ n)^-1 (inl (zero_seg n))) =
x0
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
forall mh : {m : N & m < n},
f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
xs
  (f
     ((equiv_N_segment_succ n)^-1
        (inl ((equiv_N_segment n)^-1 (inl mh)))))
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
f ((equiv_N_segment_succ n)^-1 (inl (zero_seg n))) =
x0 refine (_ @ f0).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
f ((equiv_N_segment_succ n)^-1 (inl (zero_seg n))) =
f (zero_seg (succ n))
        apply ap, path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
((equiv_N_segment_succ n)^-1 (inl (zero_seg n))).1 =
(zero_seg (succ n)).1 reflexivity.
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
forall mh : {m : N & m < n},
f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
xs
  (f
     ((equiv_N_segment_succ n)^-1
        (inl ((equiv_N_segment n)^-1 (inl mh))))) intros mh.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
xs
  (f
     ((equiv_N_segment_succ n)^-1
        (inl ((equiv_N_segment n)^-1 (inl mh)))))
        refine (_ @ fs (((equiv_N_segment_lt_succ n)^-1)
                          ((equiv_N_segment n)^-1 (inl mh))) @ _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
f
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1
        ((equiv_N_segment n)^-1 (inl mh))))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
xs
  (f
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1
              ((equiv_N_segment n)^-1 (inl mh)))))) =
xs
  (f
     ((equiv_N_segment_succ n)^-1
        (inl ((equiv_N_segment n)^-1 (inl mh)))))
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
f ((equiv_N_segment_succ n)^-1 (inl (succ_seg n mh))) =
f
  (succ_seg (succ n)
     ((equiv_N_segment_lt_succ n)^-1
        ((equiv_N_segment n)^-1 (inl mh)))) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
(equiv_N_segment_succ n)^-1 (inl (succ_seg n mh)) =
succ_seg (succ n)
  ((equiv_N_segment_lt_succ n)^-1
     ((equiv_N_segment n)^-1 (inl mh)))
          apply path_sigma_hprop; reflexivity.
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
xs
  (f
     ((equiv_N_segment (succ n))^-1
        (inl
           ((equiv_N_segment_lt_succ n)^-1
              ((equiv_N_segment n)^-1 (inl mh)))))) =
xs
  (f
     ((equiv_N_segment_succ n)^-1
        (inl ((equiv_N_segment n)^-1 (inl mh))))) apply ap, ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: {m : N & m <= succ n} -> X
f0: f (zero_seg (succ n)) = x0
fs: forall mh : {m : N & m < succ n},
f (succ_seg (succ n) mh) =
xs (f ((equiv_N_segment (succ n))^-1 (inl mh)))
mh: {m : N & m < n}
(equiv_N_segment (succ n))^-1
  (inl
     ((equiv_N_segment_lt_succ n)^-1
        ((equiv_N_segment n)^-1 (inl mh)))) =
(equiv_N_segment_succ n)^-1
  (inl ((equiv_N_segment n)^-1 (inl mh)))
          apply path_sigma_hprop; reflexivity.
    Defined.

    (** 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. *)
    Section Partials.
      Context (pf : partials).

      Local Definition N_rec'@{} : N -> X
        := fun n => (pf n).1 (refl_seg n).

      Definition N_rec_beta_zero'@{} : N_rec' zero = x0.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
N_rec' zero = x0
      Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
N_rec' zero = x0
        refine (_ @ fst (pf zero).2).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
N_rec' zero = (pf zero).1 (zero_seg zero)
        unfold N_rec'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
(pf zero).1 (refl_seg zero) =
(pf zero).1 (zero_seg zero)
        apply ap, path_sigma_hprop; reflexivity.
      Defined.

      Definition N_rec_beta_succ'@{} (n : N)
        : N_rec' (succ n) = xs (N_rec' n).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
N_rec' (succ n) = xs (N_rec' n)
      Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
N_rec' (succ n) = xs (N_rec' n)
        unfold N_rec'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1 (refl_seg (succ n)) =
xs ((pf n).1 (refl_seg n))
        refine (_ @ snd (pf (succ n)).2
                  (n ; N_lt_succ n) @ _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1 (refl_seg (succ n)) =
(pf (succ n)).1 (succ_seg (succ n) (n; N_lt_succ n))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
xs
  ((pf (succ n)).1
     ((equiv_N_segment (succ n))^-1
        (inl (n; N_lt_succ n)))) =
xs ((pf n).1 (refl_seg n))
        -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1 (refl_seg (succ n)) =
(pf (succ n)).1 (succ_seg (succ n) (n; N_lt_succ n)) apply ap, path_sigma_hprop; reflexivity.
        -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
xs
  ((pf (succ n)).1
     ((equiv_N_segment (succ n))^-1
        (inl (n; N_lt_succ n)))) =
xs ((pf n).1 (refl_seg n)) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1
  ((equiv_N_segment (succ n))^-1
     (inl (n; N_lt_succ n))) = (pf n).1 (refl_seg n)
          transitivity ((partial_Nrec_restr n (pf (succ n))).1 (refl_seg n)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1
  ((equiv_N_segment (succ n))^-1
     (inl (n; N_lt_succ n))) =
(partial_Nrec_restr n (pf (succ n))).1 (refl_seg n)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(partial_Nrec_restr n (pf (succ n))).1 (refl_seg n) =
(pf n).1 (refl_seg n)
          +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(pf (succ n)).1
  ((equiv_N_segment (succ n))^-1
     (inl (n; N_lt_succ n))) =
(partial_Nrec_restr n (pf (succ n))).1 (refl_seg n) refine (ap (pf (succ n)).1 _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(equiv_N_segment (succ n))^-1 (inl (n; N_lt_succ n)) =
(equiv_N_segment_succ n)^-1 (inl (refl_seg n))
            apply path_sigma_hprop; reflexivity.
          +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(partial_Nrec_restr n (pf (succ n))).1 (refl_seg n) =
(pf n).1 (refl_seg n) apply ap10@{p x nr}.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
n: N
(partial_Nrec_restr n (pf (succ n))).1 = (pf n).1
            apply ap, path_contr.
      Defined.

    End Partials.

    (** 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.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
NRec -> partials
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
NRec -> partials
      intros f n.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
partial_Nrec n
      exists (fun mh => f.1 mh.1).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
(f.1 (zero_seg n).1 = x0) *
(forall mh : {m : N & m < n},
 f.1 (succ_seg n mh).1 =
 xs (f.1 ((equiv_N_segment n)^-1 (inl mh)).1))
      split.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
f.1 (zero_seg n).1 = x0
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
forall mh : {m : N & m < n},
f.1 (succ_seg n mh).1 =
xs (f.1 ((equiv_N_segment n)^-1 (inl mh)).1)
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
f.1 (zero_seg n).1 = x0 exact (fst f.2).
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
forall mh : {m : N & m < n},
f.1 (succ_seg n mh).1 =
xs (f.1 ((equiv_N_segment n)^-1 (inl mh)).1) intros mh.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
n: N
mh: {m : N & m < n}
f.1 (succ_seg n mh).1 =
xs (f.1 ((equiv_N_segment n)^-1 (inl mh)).1)
        exact (snd f.2 mh.1).
    Defined.

    (** 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.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: NRec
partial_Nrec_restr n (nrec_partials f (succ n)) =
nrec_partials f n
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
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)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: NRec
((partial_Nrec_restr n (nrec_partials f (succ n))).1;
(partial_Nrec_restr n (nrec_partials f (succ n))).2) =
((nrec_partials f n).1; (nrec_partials f n).2)
      srefine (path_sigma'@{nr nr nr} _ 1 _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
n: N
f: NRec
transport
  (fun f : {m : N & m <= n} -> X =>
   (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))))) 1
  (partial_Nrec_restr n (nrec_partials f (succ n))).2 =
(nrec_partials f n).2
      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 ]).
    Defined.

    Local Definition partials_nrec@{} : partials -> NRec.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
partials -> NRec
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
partials -> NRec
      intros pf.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
NRec
      exists (N_rec' pf).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
pf: partials
(N_rec' pf zero = x0) *
(forall m : N, N_rec' pf (succ m) = xs (N_rec' pf m))
      exact (N_rec_beta_zero' pf, N_rec_beta_succ' pf).
    Defined.

    Local Definition nrec_partials_sect@{} (f : NRec)
      : partials_nrec (nrec_partials f) = f.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
partials_nrec (nrec_partials f) = f
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: NRec
partials_nrec (nrec_partials f) = f
      destruct f as [f [f0 fs]].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
partials_nrec (nrec_partials (f; (f0, fs))) =
(f; (f0, fs))
      unfold partials_nrec, nrec_partials.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
(N_rec'
   (fun n : N =>
    (fun mh : {m : N & m <= n} => (f; (f0, fs)).1 mh.1;
    (fst (f; (f0, fs)).2,
    fun mh : {m : N & m < n} =>
    snd (f; (f0, fs)).2 mh.1)));
(N_rec_beta_zero'
   (fun n : N =>
    (fun mh : {m : N & m <= n} => (f; (f0, fs)).1 mh.1;
    (fst (f; (f0, fs)).2,
    fun mh : {m : N & m < n} =>
    snd (f; (f0, fs)).2 mh.1))),
N_rec_beta_succ'
  (fun n : N =>
   (fun mh : {m : N & m <= n} => (f; (f0, fs)).1 mh.1;
   (fst (f; (f0, fs)).2,
   fun mh : {m : N & m < n} =>
   snd (f; (f0, fs)).2 mh.1))))) = (f; (f0, fs)) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
(N_rec'
   (fun n : N =>
    (fun mh : {m : N & m <= n} => f mh.1;
    (f0, fun mh : {m : N & m < n} => fs mh.1)));
(N_rec_beta_zero'
   (fun n : N =>
    (fun mh : {m : N & m <= n} => f mh.1;
    (f0, fun mh : {m : N & m < n} => fs mh.1))),
N_rec_beta_succ'
  (fun n : N =>
   (fun mh : {m : N & m <= n} => f mh.1;
   (f0, fun mh : {m : N & m < n} => fs mh.1))))) =
(f; (f0, fs))
      unfold N_rec', N_rec_beta_zero'; cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
(fun n : N => f n;
(ap (fun mh : {m : N & m <= zero} => f mh.1)
   (path_sigma_hprop (refl_seg zero) (zero_seg zero) 1) @
 f0,
N_rec_beta_succ'
  (fun n : N =>
   (fun mh : {m : N & m <= n} => f mh.1;
   (f0, fun mh : {m : N & m < n} => fs mh.1))))) =
(f; (f0, fs))
      apply ap@{nr nr}, path_prod.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
fst
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  N_rec_beta_succ'
    (fun n : N =>
     (fun mh : {m : N & m <= n} => f mh.1;
     (f0, fun mh : {m : N & m < n} => fs mh.1)))) =
fst (f0, fs)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
snd
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  N_rec_beta_succ'
    (fun n : N =>
     (fun mh : {m : N & m <= n} => f mh.1;
     (f0, fun mh : {m : N & m < n} => fs mh.1)))) =
snd (f0, fs)
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
fst
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  N_rec_beta_succ'
    (fun n : N =>
     (fun mh : {m : N & m <= n} => f mh.1;
     (f0, fun mh : {m : N & m < n} => fs mh.1)))) =
fst (f0, fs) cbn.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
ap (fun mh : {m : N & m <= zero} => f mh.1)
  (path_sigma_hprop (refl_seg zero) (zero_seg zero) 1) @
f0 = f0
        rewrite ap_compose.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
ap f
  (ap (fun x : {m : N & m <= zero} => x.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1)) @ f0 = f0
        rewrite ap_pr1_path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
ap f 1 @ f0 = f0
        apply concat_1p.
      -
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
snd
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  N_rec_beta_succ'
    (fun n : N =>
     (fun mh : {m : N & m <= n} => f mh.1;
     (f0, fun mh : {m : N & m < n} => fs mh.1)))) =
snd (f0, fs) apply path_forall; intros n.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
snd
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  N_rec_beta_succ'
    (fun n : N =>
     (fun mh : {m : N & m <= n} => f mh.1;
     (f0, fun mh : {m : N & m < n} => fs mh.1)))) n =
snd (f0, fs) n
        unfold N_rec_beta_succ'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
snd
  (ap (fun mh : {m : N & m <= zero} => f mh.1)
     (path_sigma_hprop (refl_seg zero) (zero_seg zero)
        1) @ f0,
  fun n : N =>
  (ap
     (fun mh : {m : N & m <= succ n} => f mh.1;
     (f0, fun mh : {m : N & m < succ n} => fs mh.1)).1
     (path_sigma_hprop (refl_seg (succ n))
        (succ_seg (succ n) (n; N_lt_succ n)) 1) @
   snd
     (fun mh : {m : N & m <= succ n} => f mh.1;
     (f0, fun mh : {m : N & m < succ n} => fs mh.1)).2
     (n; N_lt_succ n)) @
  ap xs
    (ap
       (fun mh : {m : N & m <= succ n} => f mh.1;
       (f0, fun mh : {m : N & m < succ n} => fs mh.1)).1
       (path_sigma_hprop
          ((equiv_N_segment (succ n))^-1
             (inl (n; N_lt_succ n)))
          ((equiv_N_segment_succ n)^-1
             (inl (refl_seg n))) 1) @
     ap10
       (ap pr1
          (path_contr
             (partial_Nrec_restr n
                (fun mh : {m : N & m <= succ n} =>
                 f mh.1;
                (f0,
                fun mh : {m : N & m < succ n} =>
                fs mh.1)))
             (fun mh : {m : N & m <= n} => f mh.1;
             (f0, fun mh : {m : N & m < n} => fs mh.1))))
       (refl_seg n))) n = snd (f0, fs) 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].
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
(ap (fun mh : {m : N & m <= succ n} => f mh.1)
   (path_sigma_hprop (refl_seg (succ n))
      (succ_seg (succ n) (n; N_lt_succ n)) 1) @ fs n) @
ap xs
  (ap (fun mh : {m : N & m <= succ n} => f mh.1)
     (path_sigma_hprop
        (n; N_lt_le n (succ n) (N_lt_succ n))
        (n;
        N_lt_le n (succ n)
          (snd (N_lt_succ_iff_le n n)
             (reflexive_N_le n))) 1) @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite ap_compose.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
(ap f
   (ap (fun x : {m : N & m <= succ n} => x.1)
      (path_sigma_hprop (refl_seg (succ n))
         (succ_seg (succ n) (n; N_lt_succ n)) 1)) @
 fs n) @
ap xs
  (ap (fun mh : {m : N & m <= succ n} => f mh.1)
     (path_sigma_hprop
        (n; N_lt_le n (succ n) (N_lt_succ n))
        (n;
        N_lt_le n (succ n)
          (snd (N_lt_succ_iff_le n n)
             (reflexive_N_le n))) 1) @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite ap_pr1_path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
(ap f 1 @ fs n) @
ap xs
  (ap (fun mh : {m : N & m <= succ n} => f mh.1)
     (path_sigma_hprop
        (n; N_lt_le n (succ n) (N_lt_succ n))
        (n;
        N_lt_le n (succ n)
          (snd (N_lt_succ_iff_le n n)
             (reflexive_N_le n))) 1) @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite ap_1, concat_1p.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
fs n @
ap xs
  (ap (fun mh : {m : N & m <= succ n} => f mh.1)
     (path_sigma_hprop
        (n; N_lt_le n (succ n) (N_lt_succ n))
        (n;
        N_lt_le n (succ n)
          (snd (N_lt_succ_iff_le n n)
             (reflexive_N_le n))) 1) @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite (ap_compose pr1 f).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
fs n @
ap xs
  (ap f
     (ap pr1
        (path_sigma_hprop
           (n; N_lt_le n (succ n) (N_lt_succ n))
           (n;
           N_lt_le n (succ n)
             (snd (N_lt_succ_iff_le n n)
                (reflexive_N_le n))) 1)) @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite ap_pr1_path_sigma_hprop.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
fs n @
ap xs
  (ap f 1 @
   ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        rewrite ap_1, concat_1p.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
fs n @
ap xs
  (ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = fs n
        refine (_ @ (concat_p1 _)); apply whiskerL.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
ap xs
  (ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     (refl_seg n)) = 1
        set (refl_seg_n := refl_seg n).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     refl_seg_n) = 1
        (** 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)).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     refl_seg_n) =
ap xs
  (ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
     refl_seg_n)
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
     refl_seg_n) = 1
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10
     (ap pr1
        (path_contr
           (partial_Nrec_restr n
              (fun mh : {m : N & m <= succ n} =>
               f mh.1;
              (f0,
              fun mh : {m : N & m < succ n} => fs mh.1)))
           (fun mh : {m : N & m <= n} => f mh.1;
           (f0, fun mh : {m : N & m < n} => fs mh.1))))
     refl_seg_n) =
ap xs
  (ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
     refl_seg_n) apply ap.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap10
  (ap pr1
     (path_contr
        (partial_Nrec_restr n
           (fun mh : {m : N & m <= succ n} => f mh.1;
           (f0,
           fun mh : {m : N & m < succ n} => fs mh.1)))
        (fun mh : {m : N & m <= n} => f mh.1;
        (f0, fun mh : {m : N & m < n} => fs mh.1))))
  refl_seg_n =
ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
  refl_seg_n
          assert (p : path_contr _ _ =  nrec_partials_succ n (f; (f0, fs))).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
path_contr
  (partial_Nrec_restr n
     (nrec_partials (f; (f0, fs)) (succ n)))
  (nrec_partials (f; (f0, fs)) n) =
nrec_partials_succ n (f; (f0, fs))
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
p: path_contr
  (partial_Nrec_restr n
     (nrec_partials (f; (f0, fs)) (succ n)))
  (nrec_partials (f; (f0, fs)) n) =
nrec_partials_succ n (f; (f0, fs))
ap10
  (ap pr1
     (path_contr
        (partial_Nrec_restr n
           (fun mh : {m : N & m <= succ n} => f mh.1;
           (f0,
           fun mh : {m : N & m < succ n} => fs mh.1)))
        (fun mh : {m : N & m <= n} => f mh.1;
        (f0, fun mh : {m : N & m < n} => fs mh.1))))
  refl_seg_n =
ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
  refl_seg_n
          {
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
path_contr
  (partial_Nrec_restr n
     (nrec_partials (f; (f0, fs)) (succ n)))
  (nrec_partials (f; (f0, fs)) n) =
nrec_partials_succ n (f; (f0, fs)) apply path_contr. }
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
p: path_contr
  (partial_Nrec_restr n
     (nrec_partials (f; (f0, fs)) (succ n)))
  (nrec_partials (f; (f0, fs)) n) =
nrec_partials_succ n (f; (f0, fs))
ap10
  (ap pr1
     (path_contr
        (partial_Nrec_restr n
           (fun mh : {m : N & m <= succ n} => f mh.1;
           (f0,
           fun mh : {m : N & m < succ n} => fs mh.1)))
        (fun mh : {m : N & m <= n} => f mh.1;
        (f0, fun mh : {m : N & m < n} => fs mh.1))))
  refl_seg_n =
ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
  refl_seg_n
          exact (ap (fun h => ap10 (ap pr1 h) refl_seg_n) p).
        +
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10 (ap pr1 (nrec_partials_succ n (f; (f0, fs))))
     refl_seg_n) = 1 unfold nrec_partials_succ.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10
     (ap pr1
        (path_sigma'
           (fun f : {m : N & m <= n} -> X =>
            (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)))))
           1
           (nrec_partials_succ_subproof n
              (f; (f0, fs))))) refl_seg_n) = 1
          unfold path_sigma'.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs
  (ap10
     (ap pr1
        (path_sigma
           (fun f : {m : N & m <= n} -> X =>
            (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)))))
           ((partial_Nrec_restr n
               (nrec_partials (f; (f0, fs)) (succ n))).1;
           (partial_Nrec_restr n
              (nrec_partials (f; (f0, fs)) (succ n))).2)
           ((partial_Nrec_restr n
               (nrec_partials (f; (f0, fs)) (succ n))).1;
           (nrec_partials (f; (f0, fs)) n).2) 1
           (nrec_partials_succ_subproof n
              (f; (f0, fs))))) refl_seg_n) = 1
          rewrite ap_pr1_path_sigma.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
f: N -> X
f0: f zero = x0
fs: forall m : N, f (succ m) = xs (f m)
n: N
refl_seg_n:= refl_seg n: {m : N & m <= n}
ap xs (ap10 1 refl_seg_n) = 1
          reflexivity.
    Qed.

    (** And we're done! *)
    #[export] Instance contr_NRec@{} : Contr NRec.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr NRec
    Proof.
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
Contr NRec
      refine (istrunc_isequiv_istrunc partials partials_nrec).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
IsEquiv partials_nrec
      refine (isequiv_adjointify _ nrec_partials nrec_partials_sect _).
UA: Univalence
PR: PropResizing
X: Type
x0: X
xs: X -> X
(fun x : partials => nrec_partials (partials_nrec x)) ==
idmap
      intros x; apply path_contr.
    Defined.

  End NRec.

End AssumeStuff.