Library UniMath.Induction.ImpredicativeInductiveSets

Impredicative Construction of Inductive Types that are Sets and Eliminate into Sets

This is based on Sam Speight's master's thesis
A Lean formalization of this had been available at https://github.com/jonas-frey/Impredicative/blob/master/ The aim of this project at the UniMath School 2019 was to have the same results within UniMath - for the time being only binary products, binary coproducts and natural numbers. This has been achieved (with a minor addition afterwards). The Lean code we used is always put into a comment at the end of the sections.
Authors: Ralph Matthes (@rmatthes), Sam Speight (@sspeight93)

Require Import UniMath.Foundations.Init.
Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Structures.

Local Open Scope cat.
Local Open Scope functions.

Section BinaryProduct.

Variable A B: HSET.

Definition pre_prod: UU := ∏ (X: HSET), (pr1hSet A -> pr1hSet B -> pr1hSet X) -> pr1hSet X.

Lemma pre_prod_isaset: isaset pre_prod.
Show proof.
  change (isofhlevel 2 pre_prod).
  do 2 (apply impred; intro).
  apply setproperty.

Definition pre_prod_as_set: HSET := make_hSet pre_prod pre_prod_isaset.

Definition nProduct (α: pre_prod): UU :=
  ∏(X Y : HSET) (f : pr1hSet X → pr1hSet Y) (h : pr1hSet A -> pr1hSet B -> pr1hSet X), f (α X h) = α Y (λ a b, f (h a b)).

Definition nProduct_isaset (α: pre_prod): isaset (nProduct α).
Show proof.
  change (isofhlevel 2 (nProduct α)).
  do 4 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.

Definition nProduct_as_set (α: pre_prod): HSET := make_hSet _ (nProduct_isaset α).

Definition Product: UU := ∑ α: pre_prod, pr1hSet (nProduct_as_set α).

Definition Product_isaset: isaset Product.
Show proof.
  apply (isaset_total2_hSet pre_prod_as_set).

Definition Product_as_set: HSET := make_hSet _ Product_isaset.

Definition Pair (a : pr1hSet A) (b : pr1hSet B) : Product.
Show proof.
  use tpair.
  - exact (λ X f, f a b).
  - cbn. red.
    intros; apply idpath.

Definition Proj1: HSET ⟦Product_as_set, A⟧.
Show proof.
  cbn.
  intro p.
  induction p as [α H].
  apply α.
  exact (fun x y => x).

Definition Proj2: HSET ⟦Product_as_set, B⟧.
Show proof.
  cbn.
  intro p.
  induction p as [α H].
  apply α.
  exact (fun x y => y).

Definition Product_rec {C: HSET} (f: pr1hSet A -> pr1hSet B -> pr1hSet C) (p: Product) : pr1hSet C.
Show proof.
  induction p.
  apply (pr1 C f).

Lemma Product_beta (C: HSET) (f: pr1hSet A -> pr1hSet B -> pr1hSet C) (a: pr1hSet A) (b: pr1hSet B) : Product_rec f (Pair a b) = f a b.
Show proof.
  apply idpath.

Lemma Product_weak_η (x: Product) : Product_rec (C := Product_as_set) Pair x = x.
Show proof.
  induction x as [P H].
  use total2_paths_f.
  - cbn.
    unfold pre_prod in P.
    apply funextsec; intro X.
    apply funextfun; intro f.
    cbn in H; red in H.
    exact (H Product_as_set X (fun x => pr1 x X f) Pair).
  - cbn.
    cbn in H.
    red in H.
    do 4 (apply funextsec; intro).
    apply setproperty.

Lemma Product_com_con {C D : HSET} (f : pr1hSet A → pr1hSet B → pr1hSet C) (g : pr1hSet C → pr1hSet D): Product_rec (λ a b, g (f a b)) = g ∘ Product_rec f.
Show proof.
  apply funextfun.
  intro x.
  induction x as [p H].
  cbn in H. red in H.
  apply pathsinv0.
  exact (H C D g f).

Lemma Product_η {C : HSET} (g : Product → pr1hSet C): Product_rec (λ a b, g (Pair a b)) = g.
Show proof.
  eapply pathscomp0.
  - apply (Product_com_con (C := Product_as_set) Pair).
  - apply funextfun; intro p.
    simpl.
    apply maponpaths.
    apply Product_weak_η.

Lemma Product_classical_η (p: Product) : Pair (Proj1 p) (Proj2 p) = p.
Show proof.
  apply pathsinv0.
  eapply pathscomp0.
  - apply pathsinv0.
    apply Product_weak_η.
  - set (Product_η_inst := Product_η (C := Product_as_set) (fun x => Pair (Proj1 x) (Proj2 x))).
    cbn in Product_η_inst.
    apply toforallpaths in Product_η_inst.
    apply Product_η_inst.

Lemma Product_univ_prop {C : HSET} : isweq (@Product_rec C).
Show proof.
  use isweq_iso.
  - exact (λ f a b, f (Pair a b)).
  - apply idpath.
  - apply Product_η.


End BinaryProduct.

Section BinaryCoproduct.

Variable A B: HSET.

Definition pre_sum: UU := ∏ (X: HSET), (pr1hSet A -> pr1hSet X) -> (pr1hSet B -> pr1hSet X) -> pr1hSet X.

Lemma pre_sum_isaset: isaset pre_sum.
Show proof.
  change (isofhlevel 2 pre_sum).
  do 3 (apply impred; intro).
  apply setproperty.

Definition pre_sum_as_set: HSET := make_hSet pre_sum pre_sum_isaset.

Definition nSum (α: pre_sum): UU :=
  ∏(X Y : HSET) (f : pr1hSet X → pr1hSet Y) (h : pr1hSet A -> pr1hSet X) (k: pr1hSet B -> pr1hSet X), f (α X h k) = α Y (f ∘ h) (f ∘ k).

Definition nSum_isaset (α: pre_sum): isaset (nSum α).
Show proof.
  change (isofhlevel 2 (nSum α)).
  do 5 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.

Definition nSum_as_set (α: pre_sum): HSET := make_hSet _ (nSum_isaset α).

Definition Sum: UU := ∑ α: pre_sum, pr1hSet (nSum_as_set α).

Definition Sum_isaset: isaset Sum.
Show proof.
  apply (isaset_total2_hSet pre_sum_as_set).

Definition Sum_as_set: HSET := make_hSet _ Sum_isaset.

Definition Sum_inl: HSET ⟦A, Sum_as_set⟧.
Show proof.
  cbn.
  intro a.
  use tpair.
  - intros X f g.
    exact (f a).
  - cbn. red.
    intros ? ? ? ? k.
    apply idpath.

Definition Sum_inr: HSET ⟦B, Sum_as_set⟧.
Show proof.
  cbn.
  intro a.
  use tpair.
  - intros X f g.
    exact (g a).
  - cbn. red.
    intros ? ? ? ? k.
    apply idpath.

Definition Sum_rec {C: HSET} (f: pr1hSet A -> pr1hSet C)
  (g: pr1hSet B -> pr1hSet C)(c: Sum) : pr1hSet C
  := pr1 c C f g.

Lemma Sum_β_l {C: HSET} (f: pr1hSet A -> pr1hSet C)
      (g: pr1hSet B -> pr1hSet C): (Sum_rec f g) ∘ Sum_inl = f.
Show proof.
  apply idpath.

Lemma Sum_β_r {C: HSET} (f: pr1hSet A -> pr1hSet C)
      (g: pr1hSet B -> pr1hSet C): (Sum_rec f g) ∘ Sum_inr = g.
Show proof.
  apply idpath.

Lemma Sum_weak_eta (x: Sum) : Sum_rec (C := Sum_as_set) Sum_inl Sum_inr x = x.
Show proof.
  induction x as [c H].
  use total2_paths_f.
  - cbn.
    unfold pre_sum in c.
    apply funextsec; intro X.
    apply funextfun; intro f.
    apply funextfun; intro g.
    cbn in H; red in H.
    apply (H Sum_as_set X (fun x => pr1 x X f g)).
  - cbn.
    cbn in H; red in H.
    do 5 (apply funextsec; intro).
    apply setproperty.

Lemma Sum_com_con {X Y: HSET} (f : pr1hSet A → pr1hSet X) (g : pr1hSet B → pr1hSet X) (h : pr1hSet X → pr1hSet Y): Sum_rec (h ∘ f) (h ∘ g) = h ∘ (Sum_rec f g).
Show proof.
  apply funextfun.
  intro x.
  induction x as [c H].
  cbn in H; red in H.
  cbn.
  apply pathsinv0.
  apply H.

Lemma Sum_η {X : HSET} (h : Sum → pr1hSet X)
  : Sum_rec (h ∘ Sum_inl) (h ∘ Sum_inr) = h.
Show proof.
  eapply pathscomp0.
  apply Sum_com_con.
  apply funextfun; intro s.
  simpl.
  apply maponpaths.
  apply Sum_weak_eta.

Lemma Sum_univ_prop {X: HSET} : (HSET ⟦Sum_as_set, X⟧) ≃ (Product (exponential_functor A X) (exponential_functor B X)).
Show proof.
  use weq_iso.
  - intro h.
    apply Pair.
    + cbn. exact (h ∘ Sum_inl).
    + cbn. exact (h ∘ Sum_inr).
  - intro a. cbn.
    apply Sum_rec.
    + exact (Proj1 _ _ a).
    + exact (Proj2 _ _ a).
  - cbn. intro x.
    apply Sum_η.
  - cbn. intro y.
    intermediate_path (Pair _ _ (Proj1 _ _ y) (Proj2 _ _ y)).
    + apply idpath.
    + apply Product_classical_η.


End BinaryCoproduct.

Section NaturalNumbers.

Definition pre_nat: UU := ∏ (X: HSET), (pr1hSet X -> pr1hSet X) -> pr1hSet X -> pr1hSet X.

Lemma pre_nat_isaset: isaset pre_nat.
Show proof.
  change (isofhlevel 2 pre_nat).
  do 3 (apply impred; intro).
  apply setproperty.

Definition pre_nat_as_set: HSET := make_hSet _ pre_nat_isaset.

Definition nNat (α: pre_nat): UU :=
  ∏(X Y : HSET) (x: pr1hSet X) (y: pr1hSet Y)(h: pr1hSet X → pr1hSet X)(k: pr1hSet Y → pr1hSet Y) (f : pr1hSet X -> pr1hSet Y), f x = y -> f ∘ h = k ∘ f -> f (α X h x) = α Y k y.

Definition nNat_isaset (α: pre_nat): isaset (nNat α).
Show proof.
  change (isofhlevel 2 (nNat α)).
  do 9 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.

Definition nNat_as_set (α: pre_nat): HSET := make_hSet _ (nNat_isaset α).

Definition Nat: UU := ∑ α: pre_nat, pr1hSet (nNat_as_set α).

Definition Nat_isaset: isaset Nat.
Show proof.
  apply (isaset_total2_hSet pre_nat_as_set).

Definition Nat_as_set: HSET := make_hSet _ Nat_isaset.

Definition Z: Nat.
Show proof.
  use tpair.
  - exact (λ X f x, x).
  - cbn; red.
    intros; assumption.

Definition S: HSET ⟦Nat_as_set,Nat_as_set⟧.
Show proof.
  cbn.
  intro n.
  use tpair.
  - exact (λ X h x, h (pr1 n X h x)).
  - cbn; red.
    intros ? ? ? ? ? ? ? H1 H2.
    induction n as [n1 n2].
    cbn in n2; red in n2.
    cbn.
    eapply pathscomp0.
    2: { apply maponpaths.
         apply (n2 X Y x y h k f); assumption. }
    apply (toforallpaths _ _ _ H2).

Definition Nat_rec {C: HSET} (h: pr1hSet C -> pr1hSet C)
  (x: pr1hSet C)(n: Nat) : pr1hSet C := pr1 n C h x.

Lemma Nat_β {C: HSET} (h: pr1hSet C -> pr1hSet C)
  (x: pr1hSet C): Nat_rec h x Z = x.
Show proof.
  apply idpath.

Lemma Nat_β' {C: HSET} (h: pr1hSet C -> pr1hSet C)
  (x: pr1hSet C) (n: Nat): Nat_rec h x (S n) = h (Nat_rec h x n).
Show proof.
  apply idpath.

Lemma Nat_weak_eta (n: Nat) : Nat_rec (C := Nat_as_set) S Z n = n.
Show proof.
  induction n as [n0 H].
  use total2_paths_f.
  - cbn.
    unfold pre_nat in n0.
    apply funextsec; intro X.
    apply funextfun; intro h.
    apply funextfun; intro x.
    cbn in H; red in H.
    apply (H Nat_as_set X Z x S h (fun n => pr1 n X h x)); apply idpath.
  - cbn.
    cbn in H; red in H.
    do 7 (apply funextsec; intro).
    do 2 (apply funextfun; intro).
    apply setproperty.

Lemma Nat_η {C: HSET} (h: pr1hSet C -> pr1hSet C)
      (x: pr1hSet C) (f: Nat → pr1hSet C)
      (p : f Z = x) (q: funcomp S f = funcomp f h):
  f = Nat_rec h x.
Show proof.
  apply funextfun.
  intro n.
  eapply pathscomp0.
  - apply maponpaths.
    apply pathsinv0.
    apply Nat_weak_eta.
  - unfold Nat_rec.
    induction n as [n0 H].
    cbn in H; red in H.
    cbn.
    apply H; assumption.


End NaturalNumbers.