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.
Proof.
  change (isofhlevel 2 pre_prod).
  do 2 (apply impred; intro).
  apply setproperty.
Defined.

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 α).
Proof.
  change (isofhlevel 2 (nProduct α)).
  do 4 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.
Defined.

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.
Proof.
  apply (isaset_total2_hSet pre_prod_as_set).
Defined.

Definition Product_as_set: HSET := make_hSet _ Product_isaset.

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

Definition Proj1: HSET ⟦Product_as_set , A ⟧.
Proof.
  cbn.
  intro p.
  induction p as [α H].
  apply α.
  exact (fun x y ⇒ x).
Defined.

Definition Proj2: HSET ⟦Product_as_set , B ⟧.
Proof.
  cbn.
  intro p.
  induction p as [α H].
  apply α.
  exact (fun x y ⇒ y).
Defined.

Definition Product_rec {C: HSET} (f: pr1hSet A → pr1hSet B → pr1hSet C) (p: Product) : pr1hSet C.
Proof.
  induction p.
  apply (pr1 C f).
Defined.

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.
Proof.
  apply idpath.
Defined.

Lemma Product_weak_η (x: Product) : Product_rec (C := Product_as_set) Pair x = x.
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.
Defined.

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.
Proof.
  apply funextfun.
  intro x.
  induction x as [p H].
  cbn in H. red in H.
  apply pathsinv0.
  exact (H C D g f).
Defined.

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

Lemma Product_classical_η (p: Product) : Pair (Proj1 p) (Proj2 p) = p.
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.
Defined.

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

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.
Proof.
  change (isofhlevel 2 pre_sum).
  do 3 (apply impred; intro).
  apply setproperty.
Defined.

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 α).
Proof.
  change (isofhlevel 2 (nSum α)).
  do 5 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.
Defined.

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.
Proof.
  apply (isaset_total2_hSet pre_sum_as_set).
Defined.

Definition Sum_as_set: HSET := make_hSet _ Sum_isaset.

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

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

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.
Proof.
  apply idpath.
Defined.

Lemma Sum_β_r {C: HSET} (f: pr1hSet A → pr1hSet C)
      (g: pr1hSet B → pr1hSet C): (Sum_rec f g ) ∘ Sum_inr = g.
Proof.
  apply idpath.
Defined.

Lemma Sum_weak_eta (x: Sum) : Sum_rec (C := Sum_as_set) Sum_inl Sum_inr x = x.
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.
Defined.

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 ).
Proof.
  apply funextfun.
  intro x.
  induction x as [c H].
  cbn in H; red in H.
  cbn.
  apply pathsinv0.
  apply H.
Defined.

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

Lemma Sum_univ_prop {X: HSET} : (HSET ⟦Sum_as_set , X ⟧) ≃ (Product (exponential_functor A X) (exponential_functor B X)).
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_η.
Defined.

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.
Proof.
  change (isofhlevel 2 pre_nat).
  do 3 (apply impred; intro).
  apply setproperty.
Defined.

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 α).
Proof.
  change (isofhlevel 2 (nNat α)).
  do 9 (apply impred; intro).
  apply hlevelntosn.
  apply setproperty.
Defined.

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.
Proof.
  apply (isaset_total2_hSet pre_nat_as_set).
Defined.

Definition Nat_as_set: HSET := make_hSet _ Nat_isaset.

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

Definition S: HSET ⟦Nat_as_set ,Nat_as_set ⟧.
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).
Defined.

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.
Proof.
  apply idpath.
Defined.

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).
Proof.
  apply idpath.
Defined.

Lemma Nat_weak_eta (n: Nat) : Nat_rec (C := Nat_as_set) S Z n = n.
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.
Defined.

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.
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.
Defined.

End NaturalNumbers.