applicative ultrapower

ultra.lean

import order.filter.filter_product 
import category_theory.category.default -- for the `tidy` tactic
open filter filter.filter_product

noncomputable theory

/-- The ultrapower of a `Type`. -/
def upower (α : Type*) := filterprod α (@hyperfilter ℕ)

/-- We think of inhabitants of upower (α → β) as nonstandard functions internal
    to the theory; this definition lets us use them as functions. 
        This is `<*>` but with two distinct universe parameters. -/
def upower.seq ⦃α β : Type*⦄ : upower (α → β) → upower α → upower β :=
λ fs as, quotient.lift_on₂' fs as (λ f a, of_seq $ λ i, (f i) (a i))
    begin
        intros f₁ as₁ f₂ as₂ hf has,
        apply quotient.sound,
        filter_upwards [hf, has],
        intros i hif hias,
        change _ = _ at hias,
        change _ = _ at hif,
        change _ = _,
        simp only [hias, hif],
    end

/-- This is `<$>` but with two distinct universe parameters. -/
def upower.map {α β : Type*} (f : α → β) : upower α → upower β := upower.seq (of f)

instance : applicative upower := { pure := λ _, of, seq := upower.seq }
instance : is_lawful_functor upower := by tidy
instance : is_lawful_applicative upower := by tidy

/-- We can now easily lift functions to ultraproducts.
    But how do we prove things about the lifts? -/
example {α} [has_add α] : has_add (upower α) :=
{ add := λ a b, (+) <$> a <*> b }
/-- This is true, but does not follow from the applicative laws; it fails for `Option`. -/
example {α β} (b : β) (as : upower α) : (λ _, b) <$> as = pure b := sorry

/-- Ultrapowers don't give us any new `Prop`s. -/
lemma prop_equiv : upower Prop ≃ Prop :=
{   to_fun := λ ps, ps = pure true,
    inv_fun := pure,
    left_inv := sorry,
    right_inv := sorry, }
/-- More generally, we don't get new elements in any fintype. -/
example {α} [fintype α] : function.bijective (pure : α → upower α) := sorry

/-- Equipped with `prop_equiv`, we can also lift relations. -/
example {α} [has_le α] : has_le (upower α) :=
{ le := λ x y, prop_equiv $ (≤) <$> x <*> y }

example {α} (x y : upower α) : x = y ↔ prop_equiv ((=) <$> x <*> y) := sorry

universes u v
/-- We can view an inhbaitant of `upower (Type u)` as a geniune type. -/
instance : has_coe_to_sort (upower $ Type u) := 
{   S := Type (u+1),
    coe := λ as, { ps : upower (Σ α : Type u, α) // (λ p : (Σ α, α), p.fst) <$> ps = as } }

/-- There are two equivalent ways of turning a type into a nonstandard type.-/
def hyp_equiv {α : Type u} : upower α ≃ ↥(pure α : upower (Type u)) :=
{   to_fun := λ x, ⟨upower.map (λ a, ⟨α, a⟩) x, sorry⟩,
    inv_fun := λ ⟨ps, h⟩, sorry, -- this should be some eq.rec nonsense
    left_inv := sorry,
    right_inv := sorry, }