EncodeDecode.v

Require Import Basics Pointed.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.

(** ** Encode-decode method of characterizing identity types *)

(** See PathAny.v for a related characterization of identity types. *)

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.A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
a0 = a1 <~> code a1
Proof.A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
a0 = a1 <~> code a1
  srapply equiv_adjointify.A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
a0 = a1 -> code a1
A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
code a1 -> a0 = a1
A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
?f o ?g == idmap
A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
?g o ?f == idmap
  -A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
a0 = a1 -> code a1 exact (fun p => p # c0).
  -A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
code a1 -> a0 = a1 apply decode.
  -A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
(fun p : a0 = a1 => transport code p c0) o decode a1 ==
idmap intro p.A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
p: code a1
transport code (decode a1 p) c0 = p
    destruct (decode _ p) in p.A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
p: code a0
transport code (decode a0 p) c0 = p
    apply s.
  -A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
decode a1 o (fun p : a0 = a1 => transport code p c0) ==
idmap intros [].A: Type
a0: A
code: A -> Type
c0: code a0
decode: forall x : A, code x -> a0 = x
s: forall c : code a0,
transport code (decode a0 c) c0 = c
r: decode a0 c0 = 1
a1: A
decode a0 (transport code 1 c0) = 1
    exact r.
Defined.

(** Encode-decode for truncated identity-types *)
Definition encode_decode_trunc 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.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
Tr n (a0 = a1) <~> code a1
Proof.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
Tr n (a0 = a1) <~> code a1
  srapply equiv_adjointify.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
Tr n (a0 = a1) -> code a1
n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
code a1 -> Tr n (a0 = a1)
n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
?f o ?g == idmap
n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
?g o ?f == idmap
  -n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
Tr n (a0 = a1) -> code a1 apply (Trunc_rec (fun p => p # c0)).
  -n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
code a1 -> Tr n (a0 = a1) apply decode.
  -n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
Trunc_rec (fun p : a0 = a1 => transport code p c0)
o decode a1 == idmap intro p.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: code a1
Trunc_rec (fun p : a0 = a1 => transport code p c0)
  (decode a1 p) = p
    pose (decode _ p) as p'.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: code a1
p':= decode a1 p: Tr n (a0 = a1)
Trunc_rec (fun p : a0 = a1 => transport code p c0)
  (decode a1 p) = p
    clearbody p'.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: code a1
p': Tr n (a0 = a1)
Trunc_rec (fun p : a0 = a1 => transport code p c0)
  (decode a1 p) = p
    strip_truncations.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: code a1
p': a0 = a1
Trunc_rec (fun p : a0 = a1 => transport code p c0)
  (decode a1 p) = p
    destruct p' in p.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
p: code a0
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 p) = p
    apply s.
  -n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
decode a1
o Trunc_rec (fun p : a0 = a1 => transport code p c0) ==
idmap intros p.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: Tr n (a0 = a1)
decode a1
  (Trunc_rec (fun p : a0 = a1 => transport code p c0)
     p) = p
    strip_truncations.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
a1: A
p: a0 = a1
decode a1
  (Trunc_rec (fun p : a0 = a1 => transport code p c0)
     (tr p)) = tr p
    destruct p.n: trunc_index
A: Type
a0: A
code: A -> Type
H: forall a : A, IsTrunc n (code a)
c0: code a0
decode: forall x : A, code x -> Tr n (a0 = x)
s: forall c : code a0,
Trunc_rec (fun p : a0 = a0 => transport code p c0)
  (decode a0 c) = c
r: decode a0 c0 = tr 1
decode a0
  (Trunc_rec (fun p : a0 = a0 => transport code p c0)
     (tr 1)) = tr 1
    exact r.
Defined.

(** Encode-decode for loop spaces *)
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 _.

(** Encode-decode for truncated loop spaces *)
Definition encode_decode_trunc_loops n
  (A : pType) (code : pFam A) `{forall a, IsTrunc n (code a)}
  (decode : forall x, code x -> Tr n (point A = x))
  (s : forall (c : code (point A)),
    Trunc_rec (fun (p : loops A) => p # (dpoint code)) (decode _ c) = c)
  (r : decode _ (dpoint code) = tr idpath)
  : pTr n (loops A) <~> code (point A)
  := encode_decode_trunc _ _ _ code (dpoint code) decode s r _.