hcongr_fun

Stream: general

[Bhavik Mehta]

Here's my example; I struggled to minimise it but I got a version which only depends on mathlib, so: https://gist.github.com/b-mehta/6853a5d1ec83c33f9b7181532fa445c8. I think I'd like some sort of hcongr_fun, where I have a heq of functions (or really, pi types) and I can apply to one argument. Alternatively I could use heq_iff_eq but by equality of types is in scope and I can't subst it

[Bhavik Mehta]

Essentially I'm struggling with using these sigma types and help would be appreciated!

[Chris Hughes]

One way to deal with this is to extract your goal into a lemma, but replace some of the complicated types involved with variables. In this case the types are probably Y and (w.a ((w.a a).snd Y.unop f.unop)).fst, which should be replaced with Y and X in some extracted lemma which can then be applied to your goal. The extracted lemma will be easier to prove because subst (h : X = Y) will work. It's probably better to change something earlier in your proof, but I'd need to understand the category theory library to know how.

[Bhavik Mehta]

I see what you mean, I'll try

[Chris Hughes]

I got pretty close. For some reason I can't use heq_eq_to_hom

lemma blah {α α' : Sort*} {β : α → Sort*} {β' : α' → Sort*} {γ : Sort*}
  {f : Π a, β a → γ} {f' : Π a, β' a → γ} {a : α} {a' : α'} {b : β a} {b' : β' a'}
  (hf : f == f')
  (hα : α = α') (hβ : β == β') (ha : a == a') (hb : b == b') :
  f a b = f' a' b' :=
by { subst α, simp at *, subst β, subst ha, simp at *, subst f, subst b }

lemma heq_eq_to_hom {X Y Z : C} (hYZ : Y = Z) (g : X ⟶ Y) : g == g ≫ eq_to_hom hYZ :=
by subst hYZ; simp [eq_to_hom]

def coalgebra_to_presheaf : coalgebra (W C) ⥤ Cᵒᵖ ⥤ Type u :=
{ obj := λ w,
  { obj := λ X, {i : _ // (w.a i).1 = X},
    map := λ X Y f a,
    begin
      refine ⟨_, _⟩,
      apply (w.a a.1).2 _ (f.unop ≫ eq_to_hom sorry),
      have t := congr_fun w.coassoc a.1,
      dsimp [comonad.δ, W] at t,
      injection t with t₁ t₂,
      rw heq_iff_eq at t₂,
      replace t₂ := congr_fun t₂ Y.unop,
      replace t₂ := congr_fun t₂ (f.unop ≫ eq_to_hom sorry),
      replace t₂ := congr_arg sigma.fst t₂,
      apply t₂.symm
    end,
    map_id' := λ X,
    begin
      ext1 ⟨a, ha⟩,
      dsimp,
      congr' 1,
      cases ha,
      rw id_comp,
      exact congr_fun w.counit a,
    end,
    map_comp' := λ X Y Z f g,
    begin
      ext1 ⟨a, ha⟩,
      subst ha,
      dsimp,
      rw comp_id,
      rw comp_id,
      congr' 1,
      have t := congr_fun w.coassoc a,
      dsimp [comonad.δ, W] at t,
      injection t with t₁ t₂,
      rw heq_iff_eq at t₂,
      replace t₂ := congr_fun t₂ Y.unop,
      replace t₂ := congr_fun t₂ f.unop,
      dsimp at t₂,
      rw ← sigma.eta (w.a ((w.a a).snd Y.unop f.unop)) at t₂,

      have := sigma.mk.inj t₂,
      rcases this with ⟨t₃, t₄⟩,
      refine blah t₄ rfl (heq_of_eq (by conv_lhs { rw t₃ })) (heq.refl _) _,

      -- by using t₄, we get the result pretty easily

    end,

  }

[Chris Hughes]

If I make it a lemma then I can apply heq_eq_to_hom

[Bhavik Mehta]

Your blah looks like the sort of hcongr_pi I thought should already exist

[Chris Hughes]

I think it's probably worth having these lemmas. But it's also probably a sign of a bad interface that they're needed, and I imagine the best way of doing it would be to extract some category theory lemmas that don't mention heq anywhere.

[Bhavik Mehta]

I think the use of heq here isn't due to category theory at all though - it's due to the sigma type in W

[Chris Hughes]

Is W something to do with W types?

[Bhavik Mehta]

Not particularly, it's unimaginatively called that because people sometimes use W for comonads :P

[Bhavik Mehta]

Or at least - I don't know of any connection between that W and W types

[Bhavik Mehta]

Actually I think it might be possible to get to a similar point with the heq without any category theory whatsoever

[Chris Hughes]

There might be some lemmas about W you could extract, I'm not really sure.

[Bhavik Mehta]

Chris Hughes said:

If I make it a lemma then I can apply heq_eq_to_hom

I'm not entirely sure what you meant here - your proof works for me!

[Bhavik Mehta]

I just had to pull the obj field out - which I'd done in the meantime anyway - and it works perfectly, thanks :)

[Mario Carneiro]

Bhavik Mehta said:

Not particularly, it's unimaginatively called that because people sometimes use W for comonads :P

Amusingly, the coinductive version of W types are called M types. Great minds think alike :upside_down:

[Mario Carneiro]

I believe the W in W-type stands for well-founded tree

[Kevin Buzzard]

I thought it was going to be Mario and Wario

[Bhavik Mehta]

Next time I need a variable name for a monad or comonad I'm definitely using mario or wario

[Jannis Limperg]

blah is essentially a characterisation of equality of sigmas:

universes u v

lemma eq_sigma {α : Sort u} {β : α → Sort v} (a a' : α) (b : β a) (b' : β a')
  : (psigma.mk a b = psigma.mk a' b') ↔ (a = a' ∧ b == b') :=
  begin
    split; intro h; cases h; cc
  end

If you find yourself equating dependent structures more often, I would prove the equivalent of this lemma for each structure (should be automatable in theory) and use that.

We can also play this game without heterogeneous equality, but this doesn't really improve anything (in Lean). It does bring out a nice symmetry: equality of sigmas is a sigma of equalities.

structure relevant_iff (α : Sort u) (β : Sort v) : Sort* :=
(forward : α → β)
(backward : β → α)

inductive relevant_eq {α : Sort u} (a : α) : α → Sort u
| refl [] : relevant_eq a

lemma eq_sigma' {α : Sort u} {β : α → Sort v} (a a' : α) (b : β a) (b' : β a')
  : relevant_iff
      (psigma.mk a b = psigma.mk a' b')
      (Σ' (eqa : relevant_eq a a'), @relevant_eq.rec _ _ (λ a _, β a) b _ eqa = b') :=
  begin
    split; intro h; cases h,
    { exact psigma.mk (@relevant_eq.refl α a) rfl },
    { cases h_fst, cases h_snd, refl }
  end