Library UniMath.MoreFoundations.Subtypes

Require Export UniMath.MoreFoundations.Notations.
Require Export UniMath.MoreFoundations.Propositions.

Declare Scope subtype.
Delimit Scope subtype with subtype.

Local Open Scope subtype.

Local Open Scope logic.
Local Open Scope type.

The powerset, or set of all subsets, of a set.
Definition subtype_set X : hSet := make_hSet (hsubtype X) (isasethsubtype X).

Definition subtype_isIn {X:UU} {S:hsubtype X} (s:S) (T:hsubtype X) : hProp := T (pr1 s).

Notation " s ∈ T " := (subtype_isIn s T) (at level 70) : subtype.

Notation " s ∉ T " := (¬ (subtype_isIn s T) : hProp) (at level 70) : subtype.

Definition subtype_containedIn {X:UU} : hrel (subtype_set X) := λ S T, ∀ x:X, S x ⇒ T x.

Notation " S ⊆ T " := (subtype_containedIn S T) (at level 70) : subtype.

Definition subtype_notContainedIn {X:UU} (S T : hsubtype X) : hProp := ∃ x:X, S x ∧ ¬ (T x).

Definition subtype_inc {X:UU} {S T : hsubtype X} : S ⊆ T -> S -> T.
Proof.
  intros le s. exact (pr1 s,, le (pr1 s) (pr2 s)).

Notation " S ⊈ T " := (subtype_notContainedIn S T) (at level 70) : subtype.

Definition subtype_smallerThan {X:UU} (S T : hsubtype X) : hProp := (S ⊆ T) ∧ (T ⊈ S).

Notation " S ⊊ T " := (subtype_smallerThan S T) (at level 70) : subtype.

Definition subtype_equal {X:UU} (S T : hsubtype X) : hProp := ∀ x, S x ⇔ T x.

Notation " S ≡ T " := (subtype_equal S T) (at level 70) : subtype.

Definition subtype_notEqual {X:UU} (S T : hsubtype X) : hProp := (S ⊈ T) ∨ (T ⊈ S).

Notation " S ≢ T " := (subtype_notEqual S T) (at level 70) : subtype.

Lemma subtype_notEqual_containedIn {X:UU} (S T : hsubtype X) : S ⊆ T -> S ≢ T -> T ⊈ S.
Show proof.
  intros ci ne. apply (squash_to_hProp ne); clear ne; intros [n|n].
  - apply (squash_to_hProp n); clear n; intros [x [p q]]. apply fromempty.
    change (neg (T x)) in q. apply q; clear q. apply (ci x). exact p.
  - exact n.

Lemma subtype_notEqual_to_negEqual {X:UU} (S T : hsubtype X) : S ≢ T -> ¬ (S ≡ T).
Show proof.
  intros n. apply (squash_to_prop n).
  + apply isapropneg.   + intros [c|c].
    * apply (squash_to_prop c).
      ** apply isapropneg.       ** intros [x [Sx nTx]] e. use nTx; clear nTx. exact (pr1 (e x) Sx).
    * apply (squash_to_prop c).
      ** apply isapropneg.       ** intros [x [Tx nSx]] e. use nSx; clear nSx. exact (pr2 (e x) Tx).

Lemma subtype_notEqual_from_negEqual {X:UU} (S T : hsubtype X) : LEM -> (S ≢ T <- ¬ (S ≡ T)).
Show proof.
  intros lem ne. unfold subtype_equal in ne.
  assert (q := negforall_to_existsneg _ lem ne); clear ne.
  apply (squash_to_hProp q); clear q; intros [x n].
  unfold subtype_notEqual.
  assert (r := weak_fromnegdirprod _ _ n); clear n. unfold dneg in r.
  assert (s := proof_by_contradiction lem r); clear r.
  apply (squash_to_hProp s); clear s. intros s. apply hinhpr. induction s as [s|s].
  + apply ii1, hinhpr. exists x. now apply negimpl_to_conj.
  + apply ii2, hinhpr. exists x. now apply negimpl_to_conj.

Definition emptysubtype (X : UU) : hsubtype X
  := λ x, hfalse.

Definition subtype_difference {X:UU} (S T : hsubtype X) : hsubtype X := λ x, S x ∧ ¬ (T x).

Notation " S - T " := (subtype_difference S T) : subtype.

Definition subtype_difference_containedIn {X:UU} (S T : hsubtype X) : (S - T) ⊆ S.
Show proof.
  intros x u. exact (pr1 u).

Lemma subtype_equal_cond {X:UU} (S T : hsubtype X) : S ⊆ T ∧ T ⊆ S ⇔ S ≡ T.
Show proof.
  split.
  - intros c x. induction c as [st ts].
    split.
    + intro s. exact (st x s).
    + intro t. exact (ts x t).
  - intro e. split.
    + intros x s. exact (pr1 (e x) s).
    + intros x t. exact (pr2 (e x) t).

Definition subtype_union {X I:UU} (S : I -> hsubtype X) : hsubtype X := λ x, ∃ i, S i x.

Notation "⋃ S" := (subtype_union S) (at level 100, no associativity) : subtype.

Definition subtype_binaryunion {X} (A B : hsubtype X) : hsubtype X
  := fun x => A x ∨ B x.

Notation "A ∪ B" := (subtype_binaryunion A B)
                              (at level 40, left associativity) : subtype.

Definition subtype_binaryunion_leq1 {X} (A B : hsubtype X) : A ⊆ (A ∪ B)
  := fun x => hdisj_in1.

Definition subtype_binaryunion_leq2 {X} (A B : hsubtype X) : B ⊆ (A ∪ B)
  := fun x => hdisj_in2.

Definition subtype_union_containedIn {X:hSet} {I:UU} (S : I -> hsubtype X) i : S i ⊆ ⋃ S
  := λ x s, hinhpr (i,,s).

Given a family of subtypes of X indexed by a type I, an element x : X is in their intersection if it is an element of each subtype.

Definition subtype_intersection {X I:UU} (S : I -> hsubtype X) : hsubtype X := λ x, ∀ i, S i x.

Notation "⋂ S" := (subtype_intersection S) (at level 100, no associativity) : subtype.

Theorem hsubtype_univalence {X:UU} (S T : hsubtype X) : (S = T) ≃ (S ≡ T).
Show proof.
  intros. intermediate_weq (∏ x, S x = T x).
  - apply weqtoforallpaths.
  - unfold subtype_equal. apply weqonsecfibers; intro x.
    apply weqlogeq.

Theorem hsubtype_rect {X:UU} (S T : hsubtype X) (P : S ≡ T -> UU) :
  (∏ e : S=T, P (hsubtype_univalence S T e)) ≃ ∏ f, P f.
Show proof.
  intros. apply weqinvweq, weqonsecbase.

Ltac hsubtype_induction f e := generalize f; apply hsubtype_rect; intro e; clear f.

Lemma subtype_containment_istrans X : istrans (@subtype_containedIn X).
Show proof.
  intros S T U i j x. exact (j x ∘ i x).

Lemma subtype_containment_isrefl X : isrefl (@subtype_containedIn X).
Show proof.
  intros S x s. exact s.

Lemma subtype_containment_ispreorder X : ispreorder (@subtype_containedIn X).
Show proof.
  use make_dirprod.
  - apply subtype_containment_istrans.
  - apply subtype_containment_isrefl.

Lemma subtype_containment_isantisymm X : isantisymm (@subtype_containedIn X).
Show proof.
  intros S T i j. apply (invmap (hsubtype_univalence S T)). apply subtype_equal_cond.
  split; assumption.

Lemma subtype_containment_isPartialOrder X : isPartialOrder (@subtype_containedIn X).
Show proof.
  use make_dirprod.
  - apply subtype_containment_ispreorder.
  - apply subtype_containment_isantisymm.

Lemma subtype_inc_comp {X:UU} {S T U : hsubtype X} (i:S⊆T) (j:T⊆U) (s:S) :
  subtype_inc j (subtype_inc i s) = subtype_inc (λ x, j x ∘ i x) s.
Show proof.
  reflexivity.

Lemma subtype_deceq {X} (S:hsubtype X) : isdeceq X -> isdeceq (carrier S).
Show proof.
  intro i. intros s t. induction (i (pr1 s) (pr1 t)) as [eq|ne].
  - apply ii1, subtypePath_prop, eq.
  - apply ii2. intro eq. apply ne. apply maponpaths. exact eq.

Definition isDecidablePredicate {X} (S:X->hProp) := ∏ x, decidable (S x).

Definition subtype_plus {X} (S:hsubtype X) (z:X) : hsubtype X := λ x, S x ∨ z = x.

Definition subtype_plus_incl {X} (S:hsubtype X) (z:X) : S ⊆ subtype_plus S z.
Show proof.
  intros s Ss. now apply hinhpr,ii1.

Definition subtype_plus_has_point {X} (S:hsubtype X) (z:X) : subtype_plus S z z.
Show proof.
  now apply hinhpr, ii2.

Definition subtype_plus_in {X} {S:hsubtype X} {z:X} {T:hsubtype X} :
  S ⊆ T -> T z -> subtype_plus S z ⊆ T.
Show proof.
  intros le Tz x S'x. apply (squash_to_hProp S'x). intros [Sx|e].
  - exact (le x Sx).
  - induction e. exact Tz.

Section Complement.

  Context {X : UU}.

  Definition subtype_complement (S : hsubtype X) : hsubtype X := fun x => hneg (S x).

Something can't be in a subtype and its complement.
  Lemma not_in_subtype_and_complement (S : hsubtype X) :
    ∏ x, S x -> subtype_complement S x -> empty.
  Show proof.
    intros x in_S in_neg_S; exact (in_neg_S in_S).

The intersection of a family containing a set and its complement is empty.
  Lemma subtype_complement_intersection_empty {S} {I : UU} {f : I -> hsubtype X} :
    (∑ i : I, f i = S) ->
    (∑ j : I, f j = subtype_complement S) ->
    subtype_intersection f ≡ emptysubtype _.
  Show proof.
    intros has_S has_neg_S x; use make_dirprod.
    - intros in_intersection.
      pose (in_S := in_intersection (pr1 has_S)).
      pose (in_neg_S := in_intersection (pr1 has_neg_S)).
      cbn in *.

      pose (in_S' := (eqtohomot (pr2 has_S)) x).
      pose (in_neg_S' := (eqtohomot (pr2 has_neg_S)) x).

      apply (not_in_subtype_and_complement S x).
      + abstract (induction in_S'; assumption).
      + abstract (induction in_neg_S'; assumption).

    - intros empt; induction empt.

The union of a family containing a set and its complement is the whole set (assuming LEM).
  Lemma subtype_complement_union {S} (lem : LEM) {I : UU} {f : I -> hsubtype X} :
    (∑ i : I, f i = S) ->
    (∑ j : I, f j = subtype_complement S) ->
    subtype_union f ≡ totalsubtype _.
  Show proof.
    intros has_S has_neg_S x; use make_dirprod.
    - intro; exact tt.
    - intro.
      induction (lem (S x)).
      + apply hinhpr.
        exists (pr1 has_S).
        abstract (rewrite (pr2 has_S); assumption).
      + apply hinhpr.
        exists (pr1 has_neg_S).
        abstract (rewrite (pr2 has_neg_S); assumption).

End Complement.

Definition binary_intersection' {X : UU} (U V : hsubtype X) : hsubtype X
  := subtype_intersection (λ b, bool_rect (λ _ : bool, hsubtype X) U V b).

Definition binary_intersection {X : UU} (U V : hsubtype X) : hsubtype X
  := λ x, U x ∧ V x.

Lemma binary_intersection_commutative {X : UU} (U V : hsubtype X)
  : ∏ x : X, (binary_intersection U V) x -> (binary_intersection V U) x.
Show proof.
  intros ? p.
  exact (transportf _ (iscomm_hconj (U x) (V x)) p).

Definition intersection_contained_l {X : UU} (U V : hsubtype X)
  : subtype_containedIn (binary_intersection U V) U.
Show proof.
  intros ? xinUV.
  apply xinUV.

Definition intersection_contained_r {X : UU} (U V : hsubtype X)
  : subtype_containedIn (binary_intersection U V) V.
Show proof.
  intros ? xinUV.
  apply xinUV.

Definition intersection_contained {X : UU} {U U' V V' : hsubtype X}
           (uu : subtype_containedIn U U')
           (vv : subtype_containedIn V V')
  : subtype_containedIn (binary_intersection U V) (binary_intersection U' V').
Show proof.
  intros x p.
  cbn.
  split.
  - apply (uu x).
    exact ((intersection_contained_l U V) x p).
  - apply (vv x).
    exact ((intersection_contained_r U V) x p).

Lemma isaprop_subtype_containedIn {X : UU} (U V : hsubtype X)
  : isaprop (subtype_containedIn U V).
Show proof.
  apply impred_isaprop ; intro.
  apply isapropimpl.
  apply V.

Definition image_hsubtype {X Y : UU} (U : hsubtype X) (f : X → Y)
  : hsubtype Y := λ y : Y, (∃ x : X, f x = y × U x).

Lemma image_hsubtype_emptyhsubtype {X Y : UU} (f : X → Y)
  : image_hsubtype (emptysubtype X) f = emptysubtype Y.
Show proof.
  apply funextsec ; intro y.
  apply hPropUnivalence.
  - intro yinfEmpty.
    use (factor_through_squash _ _ yinfEmpty).
    { apply emptysubtype. }
    intro x.
    apply (pr22 x).
  - intro yinEmpty.
    apply fromempty.
    exact (yinEmpty).

Definition image_hsubtype_id {X : UU} (U : hsubtype X)
  : image_hsubtype U (idfun X) = U.
Show proof.
  apply funextsec ; intro x.
  apply hPropUnivalence.
  - intro xinIdU.
    use (factor_through_squash _ _ xinIdU).
    { apply U. }
    intro u0.
    assert (p0 : U (pr1 u0) = U x).
    {
      apply maponpaths.
      apply (pr12 u0).
    }
    induction p0.
    apply (pr22 u0).
  - intro xinU.
    apply hinhpr.
    exact (x,, idpath x,, xinU).

Definition image_hsubtype_comp {X Y Z : UU} (U : hsubtype X)
           (f : X → Y) (g : Y → Z)
  : image_hsubtype U (funcomp f g) = image_hsubtype (image_hsubtype U f) g.
Show proof.
  apply funextsec ; intro z.
  apply hPropUnivalence.
  - intro zinCompU.
    use (factor_through_squash _ _ zinCompU).
    { apply ishinh. }
    intro x.
    apply hinhpr.
    exists (f (pr1 x)).
    exists (pr12 x).
    apply hinhpr.
    exact (pr1 x,, maponpaths f (idpath (pr1 x)),, pr22 x).
  - intro zinCompU.
    use (factor_through_squash _ _ zinCompU).
    { apply ishinh. }
    intro y.
    use (factor_through_squash _ _ (pr22 y)).
    { apply ishinh. }
    intro x.
    apply hinhpr.
    exists (pr1 x).
    split.
    + refine (_ @ (pr12 y)).
      unfold funcomp.
      unfold funcomp.
      apply maponpaths.
      exact (pr12 x).
    + exact (pr22 x).

Definition hsubtype_preserving {X Y : UU} (U : hsubtype X) (V : hsubtype Y) (f : X → Y)
  : UU := subtype_containedIn (image_hsubtype U f) V.

Lemma isaprop_hsubtype_preserving {X Y : UU} (U : hsubtype X) (V : hsubtype Y) (f : X → Y)
  : isaprop (hsubtype_preserving U V f).
Show proof.
  apply impred_isaprop ; intro.
  apply isapropimpl.
  apply V.

Lemma id_hsubtype_preserving {X : UU} (U : hsubtype X) : hsubtype_preserving U U (idfun X).
Show proof.
  intros x xinU.
  rewrite image_hsubtype_id in xinU.
  exact xinU.

Lemma comp_hsubtype_preserving {X Y Z : UU}
      {U : hsubtype X} {V : hsubtype Y} {W : hsubtype Z}
      {f : X → Y} {g : Y → Z}
      (fsp : hsubtype_preserving U V f) (gsp : hsubtype_preserving V W g)
  : hsubtype_preserving U W (funcomp f g).
Show proof.
  intros z zinU.
  rewrite image_hsubtype_comp in zinU.
  apply (gsp _).
  unfold image_hsubtype.
  use (factor_through_squash _ _ zinU).
  { apply ishinh. }
  intro y.
  apply hinhpr.
  exists (pr1 y).
  exists (pr12 y).
  apply (fsp _).
  exact (pr22 y).

Lemma empty_hsubtype_preserving {X Y : UU} (f : X → Y)
  : hsubtype_preserving (emptysubtype X) (emptysubtype Y) f.
Show proof.
  unfold hsubtype_preserving.
  rewrite image_hsubtype_emptyhsubtype.
  apply subtype_containment_isrefl.

Lemma total_hsubtype_preserving {X Y : UU} (f : X → Y)
  : hsubtype_preserving (totalsubtype X) (totalsubtype Y) f.
Show proof.
  exact (λ _ _, tt).

Section singletons.
  Definition singleton {X : UU} (x : X) : hsubtype X
    := λ (a : X), ∥ a = x ∥.

  Definition singleton_point {X : UU} {x : X} : singleton x
    := (x ,, hinhpr (idpath x)).

  Definition iscontr_singleton {X : hSet} (x : X) : iscontr (singleton x).
  Show proof.
    use make_iscontr.
    - exact singleton_point.
    - intros t.
      apply subtypePath_prop.
      apply(squash_to_prop (pr2 t)).
      apply setproperty.
      intro ; assumption.

  Definition singleton_is_in {X : UU} (A : hsubtype X) (a : A)
    : (singleton (pr1 a)) ⊆ A.
  Show proof.
    intro y.
    use hinhuniv.
    exact(λ (p : y = (pr1 a)), transportb A p (pr2 a)).
End singletons.

Definition coprod_carrier_binary_union {X}
  (A B : hsubtype X)
  : A ⨿ B -> A ∪ B.
Show proof.
  apply sumofmaps; apply subtype_inc.
  - apply subtype_binaryunion_leq1.
  - apply subtype_binaryunion_leq2.

Lemma issurjective_coprod_carrier_binary_union {X}
  (A B : hsubtype X)
  : issurjective (coprod_carrier_binary_union A B).
Show proof.
  intros [x aub].
  use(hinhfun _ aub).
  apply sumofmaps
  ; (intro y; use make_hfiber)
  ; try (apply subtypePath_prop).
  - exact(inl (x ,, y)).
  - apply idpath.
  - exact(inr (x ,, y)).
  - apply idpath.