/- Clara L"oh 2021 -/

import tactic

import maps

open classical


/- Exercise 1 -/

-- the identity map
def id_map 
    (X : Type*)
  : X → X
:= λ x, x

lemma id_bijective 
    (X : Type*)
  : is_bijective X X (id_map X) 
:=
begin
  let f : X → X := id_map X,

  -- injectivity
  have id_inj : is_injective X X f, from
  begin
    sorry,
  end,

  -- surjectivity
  have id_surj : is_surjective X X f, from
  begin
    sorry,
  end,

  show _, 
       by {exact surj_inj_bij X X f id_surj id_inj},
end  

/- Exercise 2 -/

lemma comp_inj_is_inj 
      (X : Type*)
      (Y : Type*)
      (Z : Type*)
      (f : X → Y)
      (g : Y → Z)
      (f_injective : is_injective X Y f)
      (g_injective : is_injective Y Z g)
    : is_injective X Z (g ∘ f)
:=
begin
 
  sorry,

end      

/- Exercise 3 -/

lemma inj_from_examples 
      (X : Type*)
      (Y : Type*)
      (f : X → Y)
      (x : X)
      (x' : X)
      (x_neq_x' : x ≠ x')
      (f_xx' : f x = f x')
    : ¬ is_injective X  Y f  
:= 
begin

  sorry,

end

-- redoing the first example
lemma not_inj_f_alt 
    : ¬ is_injective A A f
:=
begin

  sorry,

end

/- Exercise 4 -/

-- redoing the second example
lemma gg_id 
    : g ∘ g = id_map B
:=
begin

  sorry,

end    

lemma bij_g_alt
    : is_bijective B B g
:=
begin

  sorry,

end