Commit d070e44a authored by Ralf Jung's avatar Ralf Jung

rename lemmas about telescope function space to tele_fun_*

parent 5bcfb8b0
......@@ -106,19 +106,19 @@ Qed.
(** We can define the identity function and composition of the [-t>] function
space. *)
Definition tele_id {TT : tele} : TT -t> TT := tele_bind id.
Definition tele_fun_id {TT : tele} : TT -t> TT := tele_bind id.
Lemma tele_id_eq {TT : tele} (x : TT) :
tele_id x = x.
Proof. unfold tele_id. rewrite tele_app_bind. done. Qed.
Lemma tele_fun_id_eq {TT : tele} (x : TT) :
tele_fun_id x = x.
Proof. unfold tele_fun_id. rewrite tele_app_bind. done. Qed.
Definition tele_compose {TT1 TT2 TT3 : tele} :
Definition tele_fun_compose {TT1 TT2 TT3 : tele} :
(TT2 -t> TT3) (TT1 -t> TT2) (TT1 -t> TT3) :=
λ t1 t2, tele_bind (compose (tele_app t1) (tele_app t2)).
Lemma tele_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x :
tele_compose f g $ x = (f g) x.
Proof. unfold tele_compose. rewrite tele_app_bind. done. Qed.
Lemma tele_fun_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x :
tele_fun_compose f g $ x = (f g) x.
Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
(** Notation *)
Notation "'[tele' x .. z ]" :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment