Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- open function
- variables {α β : Type}
- def inverse (g : β → α) (f : α → β) := left_inverse g f ∧ right_inverse g f
- def inverse_comp (f : α → β) (g : β → α) (gf_inv : inverse g f)
- : (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
- ⟨gf_inv.left, gf_inv.right⟩
- def inverse_comp_id {f : α → β} {g : β → α} (gf_inv : inverse g f)
- : (g ∘ f = id) ∧ (f ∘ g = id)
- := ⟨funext (λ a, by rw [(inverse_comp f g gf_inv).left, id]),
- funext (λ b, by rw [(inverse_comp f g gf_inv).right, id])⟩
- /- A dumb example, if inverse (f ∘ g) (f ∘ g)
- and (f ∘ g) = id,
- and id = (g ∘ f)
- why not transitively, inverse (f ∘ g) (g ∘ f)
- -/
- def inverse_comp_inv {α : Type*} {β : Type*}
- : ∀ (f : α → β) (g : β → α), inverse f g → inverse (f ∘ g) (f ∘ g)
- := (λ f g, λ inv,
- /- because the types differ, -/
- have comp_fg : β → β, from f ∘ g,
- have comp_gf : α → α, from g ∘ f,
- -- where as for id we have something like:
- have id' : ∀(z : Type), z → z, from @id,
- have fog_eq_id : (f ∘ g = id), from (inverse_comp_id inv).left,
- have gof_eq_id : (id = g ∘ f), from eq.symm ((inverse_comp_id inv).right),
- -- So this eq.trans isn't going to type check, even though we have proofs of the necessary arguments.
- -- have fog_eq_gof : (f ∘ g) = g ∘ f, from eq.trans fog_eq_id gof_eq_id,
- have fog_comp_id : ∀ x, (f ∘ g)((f ∘ g) x) = x,
- from (λ x, calc (f ∘ g) ((f ∘ g) x) = (id (id x)) : by rw (inverse_comp_id inv).left
- ... = id x : by refl
- ... = x : by refl),
- and.intro fog_comp_id fog_comp_id)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement