I still don't understand how to use extends

Stream: maths

[Bhavik Mehta]

import order.preorder_hom

structure subset_system :=
(to_fun : Π (α : Type*) [partial_order α], set (set α))
(sings : ∀ (α : Type*) [partial_order α] (a : α), {a} ∈ to_fun α)
(mono : ∀ {α β : Type*} [partial_order α] [partial_order β] (f : α →ₘ β) {S : set α}, S ∈ to_fun α → f '' S ∈ to_fun β)

instance : has_coe_to_fun subset_system :=
{ F := _, coe := subset_system.to_fun }

variable (Z : subset_system)

set_option old_structure_cmd true

class complete (α : Type*) extends partial_order α :=
(sup : Π (S : set α), S ∈ Z α → α)
(is_sup : ∀ (S : set α), (S ∈ Z α) → is_lub S (sup S ‹_›))

variables {α : Type*} [partial_order α]

def ideal (α : Type*) [partial_order α] : Type* := {S : set α // ∀ (x ∈ S) (y ≤ x), y ∈ S}.

-- TODO: make this a complete lattice
instance : partial_order (ideal α) := subtype.partial_order _

structure union_complete (Z : subset_system) extends complete Z (ideal α) :=
(h : ∀ (S : set (ideal α)) (H : S ∈ Z (ideal α)), complete.sup S H = _)

Here's the error:

type mismatch at application
  complete.sup S H
term
  H
has type
  S ∈ ⇑Z (@ideal α _inst_1) (@ideal.partial_order α _inst_1)
but is expected to have type
  S ∈ ⇑Z (@ideal α _inst_1) (@complete.to_partial_order Z (@ideal α _inst_1) zcomp)

I'm getting errors like this, and they're happening because Lean can't match up the two partial order instances in the last argument of Z.
The only thing I can think of is to change complete to not use extends, but then I can't use bundled to make the category of complete things. I think what I want is for the partial_order instance inside of zcomp to be the one inferred rather than a new one, is there a nice way to fix this?

[Kyle Miller]

Does subset_system need all those partial_order arguments? If you do

structure subset_system :=
(to_fun : Π (α : Type*), set (set α))
(sings : ∀ (α : Type*) (a : α), {a} ∈ to_fun α)
(mono : ∀ {α β : Type*} [partial_order α] [partial_order β] (f : α →ₘ β) {S : set α}, S ∈ to_fun α → f '' S ∈ to_fun β)

the errors go away.

(Should union_complete be a class?)

[Bhavik Mehta]

One of my cases is

open omega_complete_partial_order
def omega_chain : subset_system :=
{ to_fun := λ α I S, by exactI (∃ (c : chain α), set.range c = S),
  sings := λ α I a, by exactI ⟨preorder_hom.const _ a, by { ext, simp [eq_comm] }⟩,
  mono := λ α β Iα Iβ f S hS,
  begin
    rcases hS with ⟨S, rfl⟩,
    exactI ⟨chain.map S f, by { ext, simp }⟩,
  end }
end

where there does need to be the partial_order instance, unless I change it so that to_fun gives junk values if there's no partial order available

[Bhavik Mehta]

As for making union_complete a class; possibly but that doesn't fix any of the problems

[Kyle Miller]

I noticed that removing set_option old_structure_cmd true makes the error go away, too.

[Bhavik Mehta]

Agh that was my first guess of how to fix it but I thought I'd already got rid of them all! Thanks