semantics.base.inhab

Propositional Truncation / Squash Types

Squash types form the quotient of a given type under the total relation. We implement squash types with the following quotient inductive type.

Inductive inhab (A : Type) := | tr (x : A) : inhab A | trP x y : tr x = tr y.

As of now, Coq does not have built in support for quotient inductive types, so we use private inductive types and an axiom for the path constructor.

The existence of squash types implies the existence of quotients and functional extensionality.

Require Import overture pext.

Definitions

Unset Elimination Schemes.
Module Export Inhab.
  Private Inductive inhab (A : Type) : Type :=
  | tr (x : A) : inhab A.

  Axiom trP : forall (A : Type) (x y : A), tr x = tr y.

  Section Induction.
    Context {A : Type} (P : inhab A -> Type).

    Definition inhab_rect (f : forall x, P (tr x)) :
      (forall x y, trP x y # f x = f y ) -> forall q, P q :=
      fun h q => match q with tr x => fun _ => f x end h.
  End Induction.
End Inhab.
Set Elimination Schemes.

Arguments tr {A} x.
Arguments trP {A x y}, {A} x y.
Arguments inhab_rect {A} P f h q.

Eliminators

Program Definition inhab_rec {A B : Type} (f : A -> B) :
  (forall x y, f x = f y ) -> inhab A -> B :=
  inhab_rect (fun _ => B) f.
Next Obligation. by rewrite transport_const. Qed.
Arguments inhab_rec {A B} f h q.

Program Definition inhab_ind {A : Type} (P : inhab A -> Prop)
  (f : forall x, P (tr x)) : forall q, P q :=
  inhab_rect P f _.
Next Obligation. exact: pi. Qed.

Program Definition inhab_indP {A : Type} (P : inhab A -> hprop)
  (f : forall x, P (tr x)) : forall q, P q :=
  inhab_rect P f _.
Next Obligation. exact: hpropP. Qed.

Propositionality

Lemma inhab_prop A : is_prop (inhab A).
Proof. apply: inhab_ind => x. apply: inhab_ind => y. exact: trP. Qed.
Canonical Structure inhab_hprop (A : Type) := mk_hprop (inhab A) (@inhab_prop A).

Mere existence and surjectivity

Definition hex (A : Type) (P : A -> Type) := inhab (sigT P).
Notation "'hexists' x .. y , p" := (hex (fun x => .. (hex (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'hexists' '/ ' x .. y , '/ ' p ']'") : type_scope.

Definition surjective {A B} (f : A -> B) := forall y : B, hexists x : A , f x = y.

Definition hex_rect {A : Type} (P : A -> Type) (Q : (hexists x, P x ) -> hprop) :
  (forall x (p : P x), Q (tr (x ;p ))) -> forall p : (hexists x, P x), Q p.
  intros H. apply inhab_indP. destruct 0. apply H.
Defined.

Definition hex_rec {A : Type} (P : A -> Type) (Q : hprop) :
  (forall x, P x -> Q ) -> (hexists x, P x ) -> Q :=
  fun H => inhab_indP (fun p => H p .1 p .2).

Definition hex_ind {A : Type} (P : A -> Prop) (Q : (hexists x, P x ) -> Prop) :
  (forall x (p : P x), Q (tr (x ;p ))) -> forall p : (hexists x, P x), Q p.
  exact: hex_rect.
Defined.

Definition hex_rec_prop {A : Type} (P : A -> Type) (Q : Prop) :
  (forall x, P x -> Q ) -> (hexists x, P x ) -> Q :=
  fun H => inhab_ind (fun p => H p .1 p .2).

Inhabitation elimination tactic

Ltac inhab := nointr repeat (
  match goal with
  | [ |- @hex _ _ -> _ ] =>
     (apply: hex_rec_prop || apply: hex_rec); do 2 intro
  | [ |- forall (_ : @hex _ _), _ ] =>
     (apply: hex_ind || apply: hex_rect); do 2 intro
  | [ |- forall (_ : @inhab _), _ ] =>
     (apply: inhab_ind || apply: inhab_indP); intro
  end).

Bijective functions are equivalences

Section InjectiveSurjective.
  Variables (A B : Type) (f : A -> B).
  Hypothesis f_inj : injective f.
  Hypothesis f_surj : surjective f.

  Program Definition inverse_cand (y : B) : A :=
    inhab_rec tag _ (f_surj y).

  Lemma inverse_cand_section (x : A) :
    inverse_cand (f x) = x.
  Proof.
    rewrite/inverse_cand. move: (f_surj (f x)). inhab=>/= y. exact: f_inj.
  Qed.

  Lemma inverse_cand_retraction (y : B) :
    f (inverse_cand y) = y.
  Proof.
    rewrite/inverse_cand. move: (f_surj y). by inhab.
  Qed.

  Definition bijective_equiv : is_equiv f :=
    mk_is_equiv inverse_cand inverse_cand_section inverse_cand_retraction.
End InjectiveSurjective.