An isomorphism of types involving truncation.

InhabitedIso.v

Record T { A B : Type } : Type :=
  { to      : A -> B
  ; from    : B -> A
  ; from_to : forall (a : A), from (to a) = a
  ; to_from : forall (b : B), to (from b) = b
  }.

Arguments T : clear implicits.

Inductive inhabited {A : Type} : Prop :=
  | elem (a : A) : inhabited.

Arguments inhabited : clear implicits.

Require Import ProofIrrelevance.

Theorem inhabited_idempotent {A : Type} :
  T A (inhabited A * A).
Proof.
refine (
  {| to := fun a => (elem a, a)
   ; from := fun p => snd p
  |}
).
- intros. reflexivity.
- intros. destruct b. simpl.
  replace (elem a) with i by apply proof_irrelevance.
  reflexivity.
Defined.