Smallness.v

Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics
  Basics.Nat Types.Unit Types.Sigma Types.Universe Types.Equiv HFiber.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Set Universe Minimization ToSet.

(** * Facts about "small" types  *)

(** This closely follows Section 2 of the paper "Non-accessible localizations", by Dan Christensen, https://arxiv.org/abs/2109.06670 *)

(** Universe variables:  we most often use a subset of [i j k u].  We think of [Type@{i}] as containing the "small" types and [Type@{j}] the "large" types.  In some early results, there are no constraints between [i] and [j], and in others we require that [i <= j], as expected.  While the case [i = j] isn't particularly interesting, we put some effort into ensuring that it is permitted as well, as there is no semantic reason to exclude it.  The universe variable [k] should be thought of as max(i+1,j), and it is generally required to satisfy [i < k] and [j <= k].  If we assume that [i < j], then we can take [k = j], but we include [k] so that we also allow the case [i = j].  The universe variable [u] is only present because we occasionally use Univalence in [Type@{k}], so the equality types need a larger universe to live in.  Because of this, most results require [k < u].

Summary of the most common situation:  [i < k < u, j <= k], where [i] is for the small types, [j] is for the large types, [k = max(i+1,j)] and [u] is an ambient universe for Univalence.

We include universe annotations when they clarify the meaning (e.g. in [IsSmall] and when using [PropResizing]), and also when it is required in order to keep control of the universe variables.

Note that [IsSmall] is defined in Overture.v. *)

Instance ishprop_issmall@{i j k | i < k, j <= k}
  `{Univalence} (X : Type@{j})
  : IsHProp (IsSmall@{i j} X).H: Univalence
X: Type
IsHProp (IsSmall X)
Proof.H: Univalence
X: Type
IsHProp (IsSmall X)
  apply hprop_inhabited_contr.H: Univalence
X: Type
IsSmall X -> Contr (IsSmall X)
  intros [Z e].H: Univalence
X, Z: Type
e: Z <~> X
Contr (IsSmall X)
  (* [IsSmall X] is equivalent to [IsSmall Z], which is contractible since it is a based path space. *)
  rapply (istrunc_equiv_istrunc { Y : Type@{i} & Y <~> Z } _).H: Univalence
X, Z: Type
e: Z <~> X
{Y : Type & Y <~> Z} <~> IsSmall X
  equiv_via (sig@{k k} (fun Y : Type@{i} => Y <~> X)).H: Univalence
X, Z: Type
e: Z <~> X
{Y : Type & Y <~> Z} <~> {Y : Type & Y <~> X}
H: Univalence
X, Z: Type
e: Z <~> X
{Y : Type & Y <~> X} <~> IsSmall X
  2: issig.H: Univalence
X, Z: Type
e: Z <~> X
{Y : Type & Y <~> Z} <~> {Y : Type & Y <~> X}
  apply equiv_functor_sigma_id.H: Univalence
X, Z: Type
e: Z <~> X
forall a : Type, (a <~> Z) <~> (a <~> X)
  intro Y.H: Univalence
X, Z: Type
e: Z <~> X
Y: Type
(Y <~> Z) <~> (Y <~> X)
  exact (equiv_functor_postcompose_equiv Y e).
Defined.

(** A type in [Type@{i}] is clearly small. *)
Instance issmall_in@{i j | i <= j} (X : Type@{i}) : IsSmall@{i j} X | 10
  := Build_IsSmall X X equiv_idmap.

(** The small types are closed under equivalence. *)
Definition issmall_equiv_issmall@{i1 j1 i2 j2 | i1 <= i2} {A : Type@{j1}} {B : Type@{j2}}
  (e : A <~> B) (sA : IsSmall@{i1 j1} A)
  : IsSmall@{i2 j2} B.A, B: Type
e: A <~> B
sA: IsSmall A
IsSmall B
Proof.A, B: Type
e: A <~> B
sA: IsSmall A
IsSmall B
  exists (smalltype A).A, B: Type
e: A <~> B
sA: IsSmall A
smalltype A <~> B
  exact (e oE (equiv_smalltype A)).
Defined.

(** The small types are closed under dependent sums. *)
Definition sigma_closed_issmall@{i j | } {A : Type@{j}}
  (B : A -> Type@{j}) (sA : IsSmall@{i j} A)
  (sB : forall a, IsSmall@{i j} (B a))
  : IsSmall@{i j} { a : A & B a }.A: Type
B: A -> Type
sA: IsSmall A
sB: forall a : A, IsSmall (B a)
IsSmall {a : A & B a}
Proof.A: Type
B: A -> Type
sA: IsSmall A
sB: forall a : A, IsSmall (B a)
IsSmall {a : A & B a}
  exists { a : (smalltype A) & (smalltype (B (equiv_smalltype A a))) }.A: Type
B: A -> Type
sA: IsSmall A
sB: forall a : A, IsSmall (B a)
{a : smalltype A &
smalltype (B (equiv_smalltype A a))} <~> {a : A & B a}
  snapply equiv_functor_sigma'; intros; apply equiv_smalltype.
Defined.

(** If a map has small codomain and fibers, then the domain is small. *)
Definition issmall_issmall_codomain_fibers@{i j | } {X Y : Type@{j}}
  (f : X -> Y)
  (sY : IsSmall@{i j} Y)
  (sF : forall y : Y, IsSmall@{i j} (hfiber f y))
  : IsSmall@{i j} X.X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
IsSmall X
Proof.X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
IsSmall X
  napply issmall_equiv_issmall.X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
?Goal <~> X
X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
IsSmall ?Goal
  -X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
?Goal <~> X exact (equiv_fibration_replacement f)^-1%equiv.
  -X, Y: Type
f: X -> Y
sY: IsSmall Y
sF: forall y : Y, IsSmall (hfiber f y)
IsSmall {y : Y & hfiber f y} apply sigma_closed_issmall; assumption.
Defined.

(** Every contractible type is small. *)
Definition issmall_contr@{i j| } (X : Type@{j}) (T : Contr X)
  : IsSmall@{i j} X
  := issmall_equiv_issmall (equiv_contr_unit)^-1 _.

(** If we can show that [X] is small when it is inhabited, then it is in fact small. This is Remark 2.9 in the paper. It lets us simplify the statement of Proposition 2.8. Note that this implies propositional resizing, so the [PropResizing] assumption is necessary. *)
Definition issmall_inhabited_issmall@{i j k | i < k, j <= k} `{PropResizing} `{Univalence}
  (X : Type@{j})
  (isX : X -> IsSmall@{i j} X)
  : IsSmall@{i j} X.H: PropResizing
H0: Univalence
X: Type
isX: X -> IsSmall X
IsSmall X
Proof.H: PropResizing
H0: Univalence
X: Type
isX: X -> IsSmall X
IsSmall X
  (* Since [IsSmall] is cumulative in the universe [j], it suffices to prove [IsSmall@{i k} X] for [k] the universe that [IsSmall@{i j}] lives in.  We think of [k] as max(i+1,j). *)
  rapply (issmall_issmall_codomain_fibers@{i k} isX).H: PropResizing
H0: Univalence
X: Type
isX: X -> IsSmall X
forall y : IsSmall X, IsSmall (hfiber isX y)
  intro sX.H: PropResizing
H0: Univalence
X: Type
isX: X -> IsSmall X
sX: IsSmall X
IsSmall (hfiber isX sX)
  rapply sigma_closed_issmall.
Defined.

(** If a type [X] is truncated, then so is [smalltype X]. *)
Instance istrunc_smalltype@{i j | } (X : Type@{j}) (n : trunc_index)
  `{IsSmall@{i j} X, IsTrunc n X}
  : IsTrunc n (smalltype X)
  := istrunc_equiv_istrunc X (equiv_smalltype@{i j} X)^-1%equiv.

(** * Locally small types *)

(** We say that a type [X] is 0-locally small if it is small, and (n+1)-locally small if its identity types are n-locally small. *)
(* TODO: Can we make this an inductive type and avoid the extra universe variable [k]? *)
Fixpoint IsLocallySmall@{i j k | i < k, j <= k} (n : nat) (X : Type@{j}) : Type@{k}
  := match n with
    | 0%nat => IsSmall@{i j} X
    | S m => forall x y : X, IsLocallySmall m (x = y)
    end.
Existing Class IsLocallySmall.
Hint Unfold IsLocallySmall : typeclass_instances.

Instance ishprop_islocallysmall@{i j k | i < k, j <= k} `{Univalence}
  (n : nat) (X : Type@{j})
  : IsHProp@{k} (IsLocallySmall@{i j k} n X).H: Univalence
n: nat
X: Type
IsHProp (IsLocallySmall n X)
Proof.H: Univalence
n: nat
X: Type
IsHProp (IsLocallySmall n X)
  (* Here and later we use [simple_induction] to control the universe variable. *)
  revert X; simple_induction n n IHn; exact _.
Defined.

(** A small type is n-locally small for all [n]. *)
Instance islocallysmall_in@{i j k | i <= j, j <= k, i < k}
  (n : nat) (X : Type@{i})
  : IsLocallySmall@{i j k} n X.n: nat
X: Type
IsLocallySmall n X
Proof.n: nat
X: Type
IsLocallySmall n X
  revert X.n: nat
forall X : Type, IsLocallySmall n X
  induction n; intro X.X: Type
IsLocallySmall 0 X
n: nat
IHn: forall X : Type, IsLocallySmall n X
X: Type
IsLocallySmall n.+1 X
  -X: Type
IsLocallySmall 0 X apply issmall_in.
  -n: nat
IHn: forall X : Type, IsLocallySmall n X
X: Type
IsLocallySmall n.+1 X intros x y.n: nat
IHn: forall X : Type, IsLocallySmall n X
X: Type
x, y: X
IsLocallySmall n (x = y)
    exact (IHn (x = y)).
Defined.

(** The n-locally small types are closed under equivalence. *)
Definition islocallysmall_equiv_islocallysmall
  @{i j1 j2 k | i < k, j1 <= k, j2 <= k}
  (n : nat) {A : Type@{j1}} {B : Type@{j2}}
  (e : A <~> B) (lsA : IsLocallySmall@{i j1 k} n A)
  : IsLocallySmall@{i j2 k} n B.n: nat
A, B: Type
e: A <~> B
lsA: IsLocallySmall n A
IsLocallySmall n B
Proof.n: nat
A, B: Type
e: A <~> B
lsA: IsLocallySmall n A
IsLocallySmall n B
  revert A B e lsA.n: nat
forall A B : Type,
A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
  simple_induction n n IHn.forall A B : Type,
A <~> B -> IsLocallySmall 0 A -> IsLocallySmall 0 B
n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
forall A B : Type,
A <~> B ->
IsLocallySmall n.+1 A -> IsLocallySmall n.+1 B
  -forall A B : Type,
A <~> B -> IsLocallySmall 0 A -> IsLocallySmall 0 B exact @issmall_equiv_issmall.
  -n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
forall A B : Type,
A <~> B ->
IsLocallySmall n.+1 A -> IsLocallySmall n.+1 B intros A B e lsA b b'.n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
A, B: Type
e: A <~> B
lsA: IsLocallySmall n.+1 A
b, b': B
IsLocallySmall n (b = b')
    napply IHn.n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
A, B: Type
e: A <~> B
lsA: IsLocallySmall n.+1 A
b, b': B
?Goal <~> b = b'
n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
A, B: Type
e: A <~> B
lsA: IsLocallySmall n.+1 A
b, b': B
IsLocallySmall n ?Goal
    *n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
A, B: Type
e: A <~> B
lsA: IsLocallySmall n.+1 A
b, b': B
?Goal <~> b = b' exact (equiv_ap' (e^-1%equiv) b b')^-1%equiv.
    *n: nat
IHn: forall A B : Type, A <~> B -> IsLocallySmall n A -> IsLocallySmall n B
A, B: Type
e: A <~> B
lsA: IsLocallySmall n.+1 A
b, b': B
IsLocallySmall n (e^-1%equiv b = e^-1%equiv b') apply lsA.
Defined.

(** A small type is n-locally small for all n. *)
Instance islocallysmall_issmall@{i j k | i < k, j <= k} (n : nat)
  (X : Type@{j}) (sX : IsSmall@{i j} X)
  : IsLocallySmall@{i j k} n X
  := islocallysmall_equiv_islocallysmall n (equiv_smalltype X) _.

(** If a type is n-locally small, then it is (n+1)-locally small. *)
Instance islocallysmall_succ@{i j k | i < k, j <= k} (n : nat)
  (X : Type@{j}) (lsX : IsLocallySmall@{i j k} n X)
  : IsLocallySmall@{i j k} n.+1 X.n: nat
X: Type
lsX: IsLocallySmall n X
IsLocallySmall n.+1 X
Proof.n: nat
X: Type
lsX: IsLocallySmall n X
IsLocallySmall n.+1 X
  revert X lsX; simple_induction n n IHn; intros X.X: Type
IsLocallySmall 0 X -> IsLocallySmall 1 X
n: nat
IHn: forall X : Type, IsLocallySmall n X -> IsLocallySmall n.+1 X
X: Type
IsLocallySmall n.+1 X -> IsLocallySmall n.+2 X
  -X: Type
IsLocallySmall 0 X -> IsLocallySmall 1 X apply islocallysmall_issmall.
  -n: nat
IHn: forall X : Type, IsLocallySmall n X -> IsLocallySmall n.+1 X
X: Type
IsLocallySmall n.+1 X -> IsLocallySmall n.+2 X intro lsX.n: nat
IHn: forall X : Type, IsLocallySmall n X -> IsLocallySmall n.+1 X
X: Type
lsX: IsLocallySmall n.+1 X
IsLocallySmall n.+2 X
    intros x y.n: nat
IHn: forall X : Type, IsLocallySmall n X -> IsLocallySmall n.+1 X
X: Type
lsX: IsLocallySmall n.+1 X
x, y: X
IsLocallySmall n.+1 (x = y)
    apply IHn, lsX.
Defined.

(** The n-locally small types are closed under dependent sums. *)
Instance sigma_closed_islocallysmall@{i j k | i < k, j <= k}
  (n : nat) {A : Type@{j}} (B : A -> Type@{j})
  (lsA : IsLocallySmall@{i j k} n A)
  (lsB : forall a, IsLocallySmall@{i j k} n (B a))
  : IsLocallySmall@{i j k} n { a : A & B a }.n: nat
A: Type
B: A -> Type
lsA: IsLocallySmall n A
lsB: forall a : A, IsLocallySmall n (B a)
IsLocallySmall n {a : A & B a}
Proof.n: nat
A: Type
B: A -> Type
lsA: IsLocallySmall n A
lsB: forall a : A, IsLocallySmall n (B a)
IsLocallySmall n {a : A & B a}
  revert A B lsA lsB.n: nat
forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) ->
IsLocallySmall n {a : A & B a}
  simple_induction n n IHn.forall (A : Type) (B : A -> Type),
IsLocallySmall 0 A ->
(forall a : A, IsLocallySmall 0 (B a)) ->
IsLocallySmall 0 {a : A & B a}
n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
forall (A : Type) (B : A -> Type),
IsLocallySmall n.+1 A ->
(forall a : A, IsLocallySmall n.+1 (B a)) ->
IsLocallySmall n.+1 {a : A & B a}
  -forall (A : Type) (B : A -> Type),
IsLocallySmall 0 A ->
(forall a : A, IsLocallySmall 0 (B a)) ->
IsLocallySmall 0 {a : A & B a} exact @sigma_closed_issmall.
  -n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
forall (A : Type) (B : A -> Type),
IsLocallySmall n.+1 A ->
(forall a : A, IsLocallySmall n.+1 (B a)) ->
IsLocallySmall n.+1 {a : A & B a} intros A B lsA lsB x y.n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
IsLocallySmall n (x = y)
    apply (islocallysmall_equiv_islocallysmall n (equiv_path_sigma _ x y)).n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
IsLocallySmall n
  {p : x.1 = y.1 &
  transport (fun a : A => B a) p x.2 = y.2}
    apply IHn.n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
IsLocallySmall n (x.1 = y.1)
n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
forall a : x.1 = y.1,
IsLocallySmall n
  (transport (fun a0 : A => B a0) a x.2 = y.2)
    *n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
IsLocallySmall n (x.1 = y.1) apply lsA.
    *n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
forall a : x.1 = y.1,
IsLocallySmall n
  (transport (fun a0 : A => B a0) a x.2 = y.2) intro p.n: nat
IHn: forall (A : Type) (B : A -> Type),
IsLocallySmall n A ->
(forall a : A, IsLocallySmall n (B a)) -> IsLocallySmall n {a : A & B a}
A: Type
B: A -> Type
lsA: IsLocallySmall n.+1 A
lsB: forall a : A, IsLocallySmall n.+1 (B a)
x, y: {a : A & B a}
p: x.1 = y.1
IsLocallySmall n
  (transport (fun a : A => B a) p x.2 = y.2)
      apply lsB.
Defined.

(** If a map has n-locally small codomain and fibers, then the domain is n-locally small. *)
Definition islocallysmall_islocallysmall_codomain_fibers@{i j k | i < k, j <= k}
  (n : nat) {X Y : Type@{j}} (f : X -> Y)
  (sY : IsLocallySmall@{i j k} n Y)
  (sF : forall y : Y, IsLocallySmall@{i j k} n (hfiber f y))
  : IsLocallySmall@{i j k} n X.n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
IsLocallySmall n X
Proof.n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
IsLocallySmall n X
  napply islocallysmall_equiv_islocallysmall.n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
?Goal <~> X
n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
IsLocallySmall n ?Goal
  -n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
?Goal <~> X exact (equiv_fibration_replacement f)^-1%equiv.
  -n: nat
X, Y: Type
f: X -> Y
sY: IsLocallySmall n Y
sF: forall y : Y, IsLocallySmall n (hfiber f y)
IsLocallySmall n {y : Y & hfiber f y} apply sigma_closed_islocallysmall; assumption.
Defined.

(** Under propositional resizing, every (n+1)-truncated type is (n+2)-locally small. This is Lemma 2.3 in the paper. *)
Instance islocallysmall_trunc@{i j k | i < k, j <= k} `{PropResizing}
  (n : trunc_index) (X : Type@{j}) (T : IsTrunc n.+1 X)
  : IsLocallySmall@{i j k} (trunc_index_to_nat n) X.H: PropResizing
n: trunc_index
X: Type
T: IsTrunc n.+1 X
IsLocallySmall (trunc_index_to_nat n) X
Proof.H: PropResizing
n: trunc_index
X: Type
T: IsTrunc n.+1 X
IsLocallySmall (trunc_index_to_nat n) X
  revert n X T.H: PropResizing
forall (n : trunc_index) (X : Type),
IsTrunc n.+1 X ->
IsLocallySmall (trunc_index_to_nat n) X
  simple_induction n n IHn; cbn.H: PropResizing
forall X : Type, IsHProp X -> IsSmall X
H: PropResizing
n: trunc_index
IHn: forall X : Type, IsTrunc n.+1 X -> IsLocallySmall (trunc_index_to_nat n) X
forall X : Type,
IsTrunc n.+2 X ->
forall x y : X,
IsLocallySmall (trunc_index_to_nat n) (x = y)
  -H: PropResizing
forall X : Type, IsHProp X -> IsSmall X exact issmall_hprop@{i j}.
  -H: PropResizing
n: trunc_index
IHn: forall X : Type, IsTrunc n.+1 X -> IsLocallySmall (trunc_index_to_nat n) X
forall X : Type,
IsTrunc n.+2 X ->
forall x y : X,
IsLocallySmall (trunc_index_to_nat n) (x = y) intros X T x y.H: PropResizing
n: trunc_index
IHn: forall X : Type, IsTrunc n.+1 X -> IsLocallySmall (trunc_index_to_nat n) X
X: Type
T: IsTrunc n.+2 X
x, y: X
IsLocallySmall (trunc_index_to_nat n) (x = y)
    rapply IHn.
Defined.