Skip to content

Commit

Permalink
showing off obviously
Browse files Browse the repository at this point in the history
  • Loading branch information
Scott Morrison committed Jun 4, 2018
1 parent 690d11d commit 9d211e5
Showing 1 changed file with 11 additions and 146 deletions.
157 changes: 11 additions & 146 deletions src/categories/universal/types/default.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,178 +10,43 @@ universe u
instance Types_has_Products : has_Products (Type u) :=
{ product := λ I φ, { product := Π i : I, φ i,
projection := λ i x, x i,
map := λ Z f z i, f i z,
factorisation := begin
-- `obviously'` says:
intros,
refl
end,
uniqueness := begin
-- `obviously'` says:
intros,
apply funext,
intros,
apply funext,
intros,
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
end } }
map := λ Z f z i, f i z } }

instance Types_has_Coproducts : has_Coproducts (Type u) :=
{ coproduct := λ I φ, { coproduct := Σ i : I, φ i,
inclusion := λ i x, ⟨ i, x ⟩,
map := λ Z f p, f p.1 p.2,
factorisation := begin
-- `obviously'` says:
intros,
refl
end,
uniqueness := begin
-- `obviously'` says:
intros,
apply funext,
intros,
automatic_induction,
dsimp,
dsimp at *,
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
end } }
map := λ Z f p, f p.1 p.2 } }

-- Even though this can be automatically generated from `Types_has_Products`, this is a cleaner version.
instance Types_has_BinaryProducts : has_BinaryProducts.{u+1 u} (Type u) :=
{ binary_product := λ X Y, { product := X × Y,
left_projection := prod.fst,
right_projection := prod.snd,
map := λ _ f g z, (f z, g z),
left_factorisation := begin
-- `obviously'` says:
intros,
refl
end,
right_factorisation := begin
-- `obviously'` says:
intros,
refl
end,
uniqueness := begin
-- `obviously'` says:
intros,
apply funext,
intros,
apply pairs_equal,
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
end } }
map := λ _ f g z, (f z, g z) } }

instance Types_has_BinaryCoproducts : has_BinaryCoproducts.{u+1 u} (Type u) :=
{ binary_coproduct := λ X Y, { coproduct := X ⊕ Y,
left_inclusion := sum.inl,
right_inclusion := sum.inr,
map := λ _ f g z, sum.cases_on z f g,
left_factorisation := begin
-- `obviously'` says:
intros,
refl
end,
right_factorisation := begin
-- `obviously'` says:
intros,
refl
end,
uniqueness := λ Z f g lw rw, begin
-- `obviously'` says (with a little help!):
apply funext,
intros,
simp only [funext_simp] at *,
cases x,
solve_by_elim {discharger := `[cc]},
solve_by_elim {discharger := `[cc]},
end } }
uniqueness := λ Z f g lw rw, begin tidy, cases x, tidy end } }

instance Types_has_Equalizers : has_Equalizers.{u+1 u} (Type u) :=
{ equalizer := λ α β f g, { equalizer := {x : α // f x = g x},
inclusion := λ x, x.val,
map := λ γ k h g, ⟨ k g, begin
-- `obviously'` says:
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
end ⟩,
factorisation := begin
-- `obviously'` says:
intros,
refl
end,
witness := begin
-- `obviously'` says:
apply funext,
intros,
automatic_induction,
dsimp,
solve_by_elim {discharger := `[cc]},
end,
uniqueness := begin
-- `obviously'` says:
intros,
apply funext,
intros,
apply subtype.eq,
dsimp at *,
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
end } }

map := λ γ k h g, ⟨ k g, by obviously ⟩ } }

@[semiapplicable] lemma constant_on_quotient {α β : Type u} (f g : α → β) {Z : Type u} (k : β → Z) (x y : β) (h : eqv_gen (λ (x y : β), ∃ (a : α), f a = x ∧ g a = y) x y) (w : ∀ (a : α), k (f a) = k (g a)) : k x = k y :=
begin
induction h,
-- obviously' says:
{ cases h_a,
cases h_a_h,
induction h_a_h_right, induction h_a_h_left,
solve_by_elim {discharger := `[cc]} },
{ refl },
{ solve_by_elim {discharger := `[cc]} },
{ solve_by_elim {discharger := `[cc]} },
obviously
end

instance Types_has_Coequalizers : has_Coequalizers.{u+1 u} (Type u) :=
{ coequalizer := λ α β f g, by letI s := eqv_gen.setoid (λ x y, ∃ a : α, f a = x ∧ g a = y);
exact { coequalizer := quotient s,
projection := begin
-- `obviously'` says:
apply quotient.mk
end,
map := λ Z k w, quotient.lift k begin /- `obviously'` says: -/ intros, simp only [funext_simp] at *, apply categories.types.constant_on_quotient ; assumption end,
factorisation := begin
-- `obviously'` says:
intros,
refl
end,
witness := begin
-- `obviously'` says:
apply funext,
intros,
apply quotient.sound,
apply eqv_gen.rel,
fsplit,
solve_by_elim {discharger := `[cc]},
fsplit,
refl,
refl
end,
uniqueness := begin
-- `obviously'` says:
---
intros,
apply funext,
intros,
induction x,
simp only [funext_simp] at *,
solve_by_elim {discharger := `[cc]},
refl
---
end } }
exact
{ coequalizer := quotient s,
projection := by obviously,
map := λ Z k w, quotient.lift k (by obviously),
witness := begin tidy, apply eqv_gen.rel, tidy, end } }
end categories.types

0 comments on commit 9d211e5

Please sign in to comment.