fact: Definition encode_decode (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.
imports: Basics Pointed Truncations.Core