fact: Definition encode_decode_loops (A : pType) (code : pFam A) (decode : forall x, code x -> point A = x) (s : forall (c : code (point A)), decode _ c # (dpoint code) = c) (r : decode _ (dpoint code) = idpath) : loops A <~> code (point A) := encode_decode _ _ code (dpoint code) decode s r _.
imports: Basics Pointed Truncations.Core