• Sign Up
• Login
• API
• FAQ
• Tools
• Archive
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.

Top