Functions
composition
Definition fcompose{X Y Z : Type}(f : Y → Z)(g : X → Y)(x : X) : Z :=
f(g(x)).
Hint Unfold fcompose.
Notation " f ∘ g " := (fcompose f g)
(at level 40, left associativity) : feq_scope.
Definition function_equal {X Y : Type}(f g : X → Y) :=
∀ x : X, f x = g x.
Notation " g ≡ f " := (function_equal g f)
(at level 70) : feq_scope.
Open Scope feq_scope.
Lemma feq_reflexive : ∀ (X Y : Type)(f : X → Y), f ≡ f.
Lemma feq_transitive :
∀ (X Y : Type)(f g h : X → Y), f ≡ g → g ≡ h → f ≡ h.
Lemma feq_symmetric : ∀ (X Y : Type)(f g : X → Y), f ≡ g → g ≡ f.
Lemma feq_eq : ∀(X Y : Type)(f g : X → Y), f = g → f ≡ g.
Lemma feq_rw_r : ∀ (X Y : Type)(f g h : X → Y),
g ≡ h → f ≡ h → f ≡ g.
Definition id {X : Type} : X → X := fun x ⇒ x.
Lemma feq_id_left : ∀ (X Y : Type)(f : X → Y), (id ∘ f) ≡ f.
Lemma feq_id_right : ∀ (X Y : Type)(f : X → Y), (f ∘ id) ≡ f.
Lemma feq_compose_associative :
∀ (U V X Y : Type)(f : X → Y)(g : V → X)(h : U → V),
(f ∘ (g ∘ h)) ≡ (f ∘ g ∘ h).
Lemma feq_compose_associative_reverse :
∀ (U V X Y : Type)(f : X → Y)(g : V → X)(h : U → V),
(f ∘ g ∘ h) ≡ (f ∘ (g ∘ h)).
Lemma feq_compose_both :
∀ (X Y Z : Type)(f1 f2: Y → Z)(g1 g2 : X → Y),
f1 ≡ f2 → g1 ≡ g2 → (f1 ∘ g1) ≡ (f2 ∘ g2).
Lemma feq_compose_left_both :
∀ (X Y Z : Type)(f : Y → Z)(g1 g2 : X → Y),
g1 ≡ g2 → (f ∘ g1) ≡ (f ∘ g2).
Lemma feq_compose_right_both :
∀ (X Y Z : Type)(f1 f2 : Y → Z)(g : X → Y),
f1 ≡ f2 → (f1 ∘ g) ≡ (f2 ∘ g).
Lemma feq_left_compose_left :
∀(X Y Z : Type)(f1 f2 : Y → Z)(g : X → Y)(h : X → Z),
f1 ≡ f2 → f2 ∘ g ≡ h → f1 ∘ g ≡ h.
Lemma feq_left_compose_right :
∀(X Y Z : Type)(f1 f2 : Y → Z)(g : X → Z)(h : X → Y),
f1 ≡ f2 → g ≡ f2 ∘ h → g ≡ f1 ∘ h.
Lemma feq_right_compose_left :
∀(X Y Z : Type)(f : Y → Z)(g1 g2 : X → Y)(h : X → Z),
g1 ≡ g2 → f ∘ g2 ≡ h → f ∘ g1 ≡ h.
Lemma feq_right_compose_right :
∀(X Y Z : Type)(f1 f2 : X → Y)(g : X → Z)(h : Y → Z),
f1 ≡ f2 → g ≡ h ∘ f2 → g ≡ h ∘ f1.
Definition final_map(X : Type) : X → unit := fun _ ⇒ tt.
Lemma final_map_prop : ∀(X : Type)(f : X → unit),
f ≡ final_map X.
Definition pair{U X Y : Type}(f : U → X)(g : U → Y) : U → X × Y :=
fun(u : U) ⇒ (f u, g u).
Lemma pair_proj_left :
∀(U X Y : Type)(f : U → X)(g : U → Y),
(@fst X Y) ∘ (pair f g) = f.
Lemma pair_proj_right :
∀(U X Y : Type)(f : U → X)(g : U → Y),
(@snd X Y) ∘ (pair f g) = g.
Lemma pair_compose_right :
∀(U V X Y : Type)(h : U → V)(f : V → X)(g : V → Y),
(pair f g) ∘ h = pair (f ∘ h) (g ∘ h).
Lemma feq_pair_proj : ∀(U X Y : Type)(f : U → X × Y),
f ≡ pair ((fst (B := Y)) ∘ f) ((snd (B := Y)) ∘ f).
Lemma feq_pair_both :
∀(X Y Z : Type)(f1 f2 : X → Y)(g1 g2 : X → Z),
f1 ≡ f2 → g1 ≡ g2 → pair f1 g1 ≡ pair f2 g2.
Lemma feq_pair_left :
∀(X Y Z : Type)(f1 f2 : X → Y)(g : X → Z),
f1 ≡ f2 → pair f1 g ≡ pair f2 g.
Lemma feq_pair_right :
∀(X Y Z : Type)(f : X → Y)(g1 g2 : X → Z),
g1 ≡ g2 → pair f g1 ≡ pair f g2.
Definition ftimes{U V X Y : Type}(f : U → X)(g : V → Y) : U × V → X × Y :=
fun(uv : U × V) ⇒ (f (fst uv), g (snd uv)).
Lemma ftimes_def :
∀(U V X Y : Type)(f : U → X)(g : V → Y),
pair (f ∘ (fst (B := V))) (g ∘ (snd (B := V))) = ftimes f g.
Lemma feq_ftimes_id : ∀(X Y : Type),
ftimes (@id X) (@id Y) ≡ @id (X × Y).
Lemma feq_ftimes_compose :
∀(XL XR YL YR ZL ZR : Type)
(fl : XL → YL)(fr : XR → YR)(gl : YL → ZL)(gr : YR → ZR),
(ftimes gl gr) ∘ (ftimes fl fr) ≡ ftimes (gl ∘ fl) (gr ∘ fr).
Lemma feq_ftimes_compose_pair :
∀(X YL YR ZL ZR : Type)
(fl : X → YL)(fr : X → YR)(gl : YL → ZL)(gr : YR → ZR),
(ftimes gl gr) ∘ (pair fl fr) ≡ pair (gl ∘ fl) (gr ∘ fr).
Lemma feq_ftimes_both :
∀(U V X Y : Type)(f1 f2 : U → X)(g1 g2 : V → Y),
f1 ≡ f2 → g1 ≡ g2 → ftimes f1 g1 ≡ ftimes f2 g2.
Lemma feq_ftimes_left :
∀(U V X Y : Type)(f1 f2 : U → X)(g : V → Y),
f1 ≡ f2 → ftimes f1 g ≡ ftimes f2 g.
Lemma feq_ftimes_right :
∀(U V X Y : Type)(f : U → X)(g1 g2 : V → Y),
g1 ≡ g2 → ftimes f g1 ≡ ftimes f g2.