(A : Type) (a0 : A) (code : A -> Type) (c0 : code a0) (decode : forall x, code x -> a0 = x) (s : forall (c : code a0), decode _ c # c0 = c) (r : decode _ c0 = idpath) (a1 : A) : a0 = a1 <~> code a1. Proof. srapply equiv_adjointify. - exact (fun p => p # c0). - apply decode. - intro p. destruct (decode _ p) in p. apply s. - intros []. exact r. Defined.
Require Import Basics Pointed. Require Import Truncations.Core.