Skip to content

Instantly share code, notes, and snippets.

@skaslev
Last active Dec 6, 2019
Embed
What would you like to do?
Kan extensions
def ran (g h : TypeType) (α : Type) := Π β, (α → g β) → h β
def lan (g h : TypeType) (α : Type) := Σ β, (g β → α) × h β
def mapr {g h} {α β} (s : α → β) (x : ran g h α) : ran g h β :=
λ b t, x b (t ∘ s)
def mapl {g h} {α β} (s : α → β) (x : lan g h α) : lan g h β :=
⟨x.1, ⟨s ∘ x.2.1, x.2.2⟩⟩
attribute [reducible] id
attribute [simp] function.comp
-- @[simp] lemma prod.mk.eta {α β} : Π {p : α × β}, (p.1, p.2) = p
-- | (a, b) := rfl
@[simp] lemma sigma.mk.eta {α} {β : α → Type} : Π {p : Σ α, β α}, sigma.mk p.1 p.2 = p
| ⟨a, b⟩ := rfl
instance {g h} : functor (ran g h) :=
{ map := @mapr g h }
instance {g h} : is_lawful_functor (ran g h) :=
{ id_map := by intros; simp [functor.map, mapr],
comp_map := by intros; simp [functor.map, mapr] }
instance {g h} : functor (lan g h) :=
{ map := @mapl g h }
instance {g h} : is_lawful_functor (lan g h) :=
{ id_map := by intros; simp [functor.map, mapl],
comp_map := by intros; simp [functor.map, mapl] }
def natural {f g} [functor f] [functor g] (t : Π {α}, f α → g α) :=
Π {α β} {x : f α} (s : α → β), s <$> (t x) = t (s <$> x)
axiom free_theorem {f g} [functor f] [functor g] (t : Π α, f α → g α) : natural t
section yoneda
variables {f : TypeType} [functor f] [is_lawful_functor f] {α : Type}
@[reducible] def yoneda := ran id
def check (x : f α) : yoneda f α :=
λ b s, s <$> x
def uncheck (x : yoneda f α) : f α :=
x α id
def uncheck_check (x : f α) : uncheck (check x) = x :=
begin
simp [check, uncheck, is_lawful_functor.id_map]
end
def check_uncheck (x : yoneda f α) : check (uncheck x) = x :=
begin
simp [check, uncheck],
funext,
apply free_theorem (@uncheck f _ _)
end
@[reducible] def coyoneda := lan id
def cocheck (x : f α) : coyoneda f α :=
⟨α, ⟨id, x⟩⟩
def councheck (x : coyoneda f α) : f α :=
x.2.1 <$> x.2.2
def councheck_cocheck (x : f α) : councheck (cocheck x) = x :=
begin
simp [cocheck, councheck, is_lawful_functor.id_map]
end
def cocheck_councheck (x : coyoneda f α) : cocheck (councheck x) = x :=
begin
simp [councheck],
rw ←free_theorem (@cocheck f _ _),
simp [cocheck, functor.map, mapl]
end
end yoneda
structure {u v} iso (α : Type u) (β : Type v) :=
(f : α → β) (g : β → α) (gf : Π x, g (f x) = x) (fg : Π x, f (g x) = x)
namespace iso
def inv {α β} (i : iso α β) : iso β α :=
⟨i.g, i.f, i.fg, i.gf⟩
def comp {α β γ} (i : iso α β) (j : iso β γ) : iso α γ :=
⟨j.f ∘ i.f, i.g ∘ j.g, by simp [j.gf, i.gf], by simp [i.fg, j.fg]⟩
universes u v w
variables {f : Type u → Type v} {g : Type u → Type w} (i : Π {α}, iso (f α) (g α))
def imap [functor f] {α β : Type u} (s : α → β) (x : g α) : g β :=
i.f $ s <$> i.g x
def ipure [applicative f] {α : Type u} (x : α) : g α :=
i.f $ pure x
def iseq [applicative f] {α β : Type u} (s : g (α → β)) (x : g α) : g β :=
i.f $ i.g s <*> i.g x
def ibind [monad f] {α β : Type u} (x : g α) (s : α → g β) : g β :=
i.f $ i.g x >>= i.g ∘ s
@[priority std.priority.default-1]
instance functor [functor f] : functor g :=
{ map := @imap f g @i _ }
-- @[priority std.priority.default-1]
-- instance is_lawful_functor [functor f] : is_lawful_functor g :=
-- { id_map :=
-- begin
-- intros,
-- simp [imap, is_lawful_functor.id_map, i.fg]
-- end,
-- comp_map :=
-- begin
-- intros,
-- simp [imap, i.gf],
-- rw is_lawful_functor.comp_map
-- end }
@[priority std.priority.default-1]
instance applicative [applicative f] : applicative g :=
{ pure := @ipure f g @i _,
seq := @iseq f g @i _ }
-- @[priority std.priority.default-1]
-- instance is_lawful_applicative [is_lawful_applicative f] : is_lawful_applicative g :=
-- { pure_seq_eq_map := by intros; simp,
-- id_map :=
-- begin
-- intros,
-- simp [ipure, iseq, i.gf],
-- simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_functor.id_map, i.fg]
-- end,
-- map_pure :=
-- begin
-- intros,
-- simp [ipure, iseq, i.gf],
-- simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.map_pure]
-- end,
-- seq_pure :=
-- begin
-- intros,
-- simp [ipure, iseq, i.gf],
-- simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.seq_pure]
-- end,
-- seq_assoc :=
-- begin
-- intros,
-- simp [ipure, iseq, i.gf],
-- simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.seq_assoc]
-- end }
@[priority std.priority.default-1]
instance monad [monad f] : monad g :=
{ pure := @ipure f g @i _,
bind := @ibind f g @i _ }
-- @[priority std.priority.default-1]
-- instance is_lawful_monad [is_lawful_monad f] : is_lawful_monad g :=
-- { id_map :=
-- begin
-- intros,
-- simp [ipure, ibind, i.gf],
-- rw monad.bind_pure_comp_eq_map,
-- simp [is_lawful_functor.id_map, i.fg]
-- end,
-- pure_bind :=
-- begin
-- intros,
-- simp [ipure, ibind, i.gf],
-- simp [is_lawful_monad.pure_bind, i.fg]
-- end,
-- bind_assoc :=
-- begin
-- intros,
-- simp [ibind, i.gf],
-- simp [is_lawful_monad.bind_assoc]
-- end }
end iso
section yoneda_iso
variables (f : TypeType) [functor f] [is_lawful_functor f] ⦃α : Type
def yoneda_iso : iso (f α) (yoneda f α) :=
⟨check, uncheck, uncheck_check, check_uncheck⟩
def coyoneda_iso : iso (f α) (coyoneda f α) :=
⟨cocheck, councheck, councheck_cocheck, cocheck_councheck⟩
def yoco_iso : iso (yoneda f α) (coyoneda f α) :=
(@yoneda_iso f _ _ α).inv.comp (@coyoneda_iso f _ _ α)
end yoneda_iso
-- instance {f} [applicative f] : applicative (yoneda f) := iso.applicative (yoneda_iso f)
-- instance {f} [applicative f] : applicative (coyoneda f) := iso.applicative (coyoneda_iso f)
-- instance {f} [monad f] : monad (yoneda f) := iso.monad (yoneda_iso f)
-- instance {f} [monad f] : monad (coyoneda f) := iso.monad (coyoneda_iso f)
section naturality_proofs
variables {f : TypeType} [functor f] [is_lawful_functor f]
def natural_check : natural (@check f _ _) :=
begin
unfold natural, intros,
dsimp [check, functor.map, mapr],
funext,
rw is_lawful_functor.comp_map
end
def natural_uncheck : natural (@uncheck f _ _) :=
begin
unfold natural, intros,
dsimp [uncheck, functor.map, mapr],
admit -- ← stuck here
end
def natural_cocheck : natural (@cocheck f _ _) :=
begin
unfold natural, intros,
dsimp [cocheck, functor.map, mapl],
admit -- ← stuck here
end
def natural_councheck : natural (@councheck f _ _) :=
begin
unfold natural, intros,
dsimp [councheck, functor.map, mapl],
rw ←is_lawful_functor.comp_map
end
end naturality_proofs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment