SHARE
TWEET

Untitled

a guest Apr 22nd, 2019 98 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. open function
  2.  
  3. variables {α β : Type}
  4. def inverse (g : β → α) (f : α → β) := left_inverse g f ∧ right_inverse g f
  5. def inverse_comp (f : α → β) (g : β → α) (gf_inv : inverse g f)
  6.   : (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
  7.     ⟨gf_inv.left, gf_inv.right⟩
  8.  
  9.   def inverse_comp_id {f : α → β} {g : β → α} (gf_inv  : inverse g f)
  10.   : (g ∘ f = id) ∧ (f ∘ g = id)
  11.   := ⟨funext (λ a, by rw [(inverse_comp f g gf_inv).left, id]),
  12.       funext (λ b, by rw [(inverse_comp f g gf_inv).right, id])⟩
  13.      
  14.   /- A dumb example, if inverse (f ∘ g) (f ∘ g)
  15.      and (f ∘ g) = id,
  16.      and id = (g ∘ f)
  17.      why not transitively, inverse (f ∘ g) (g ∘ f)
  18.   -/
  19.   def inverse_comp_inv {α : Type*} {β : Type*}
  20.   : ∀ (f : α → β) (g : β → α), inverse f g → inverse (f ∘ g) (f ∘ g)
  21.   := (λ f g, λ inv,
  22.       /- because the types differ, -/
  23.       have comp_fg : β → β, from f ∘ g,
  24.       have comp_gf : α → α, from g ∘ f,
  25.       -- where as for id we have something like:
  26.       have id' : ∀(z : Type), z → z, from @id,
  27.       have fog_eq_id : (f ∘ g = id), from (inverse_comp_id inv).left,
  28.       have gof_eq_id : (id = g ∘ f), from eq.symm ((inverse_comp_id inv).right),
  29.       -- So this eq.trans isn't going to type check, even though we have proofs of the necessary arguments.      
  30.       -- have fog_eq_gof : (f ∘ g) = g ∘ f, from eq.trans fog_eq_id gof_eq_id,
  31.       have fog_comp_id : ∀ x, (f ∘ g)((f ∘ g) x) = x,
  32.         from (λ x, calc (f ∘ g) ((f ∘ g) x) = (id (id x)) : by rw (inverse_comp_id inv).left
  33.                           ... = id x : by refl
  34.                           ... = x : by refl),
  35.       and.intro fog_comp_id fog_comp_id)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top