namespace http://mathhub.info/MitM/core/typedsets 
import base http://mathhub.info/MitM/Foundation 

theory Functions : base:?Logic =
	include ?Relations 
	function_composition: {A : type,B : type, C : type} (A ⟶ B) ⟶ (B ⟶ C)  ⟶ (A ⟶ C)  = [A,B,C][f,g] [x] g (f x)  # 5 ° 4 
	image: {A,B} (A ⟶ B) ⟶ set A ⟶ set B   # im 3 4 
	function_restriction: {A : type,B : type, C : type}{prf : (C <* A)} (A ⟶ B) ⟶ (C ⟶ B)  # function_restriction 5 3 
	preimage : {A,B} (A ⟶ B) ⟶ set B ⟶ set A  # preim 3 4 
	identityFunction : {A : type} (A ⟶ A)  = [A,x] x  # Id 1 
  constantFunction : {A : type,B : type} B ⟶ A ⟶ B  = [A,B,c,x] c 


theory Injective : base:?Logic =

	injective : {A : type,B : type, f: A ⟶ B} prop  
		= [A,B,f] ∀[x:A] ∀[y : A]  f x ≐ f y ⇒ x ≐ y 
		# is_injective 3  
		
	           
theory Surjective : base:?Logic =
	surjective : {A : type, B : type, f: A ⟶ B} prop  
		= [A,B,f]   ∀[y : B] ∃[x: A]  f x ≐ y 
		# is_surjective 3  


theory Bijective : base:?Logic = 
	include ?Surjective
	include ?Injective  

	bijective : {A: type, B: type, f : A ⟶ B} prop 
		=  [A, B, f] is_injective f ∧ is_surjective f
		# is_bijective 3 
          
	bijections : {A : type, B : type} type  = [A, B] (A ⟶ B)  # bijections 1 2
	inverseBijections : {A : type, B : type} bijections A B ⟶ bijections B A  # bijinv 3

	   
theory InverseFunction : base:?Logic =
   include ☞base:?DescriptionOperator 
   inverse : {A : type,B: type, f: A ⟶ B} B ⟶ A  
    = [A,B,f,y]  ι [x] f x ≐ y  
    # 1^-1 


theory Permutation : base:?Logic = 
   include ?Bijective 
   permutation : {A: type, f: A ⟶ A} prop 
     = [A,f] is_bijective f 
     # is_permutation 2