n (A : Type) (a0 : A) (code : A -> Type) `{forall a, IsTrunc n (code a)} (c0 : code a0) (decode : forall x, code x -> Tr n (a0 = x)) (s : forall (c : code a0), Trunc_rec (fun p => p # c0) (decode _ c) = c) (r : decode _ c0 = tr idpath) (a1 : A) : Tr n (a0 = a1) <~> code a1. Proof. srapply equiv_adjointify. - apply (Trunc_rec (fun p => p # c0)). - apply decode. - intro p. pose (decode _ p) as p'. clearbody p'. strip_truncations. destruct p' in p. apply s. - intros p. strip_truncations. destruct p. exact r. Defined.
Require Import Basics Pointed. Require Import Truncations.Core.