structures with dependent fields

Stream: new members

[Tsvi Benson-Tilsen]

Hi. (I'm new to Lean. Working in Lean 3.4.2, just for fun.)

---

Basic question:

I'm trying to work with structures, e.g. proving two instances are equal by proving their fields are equal. For simple structures this is easy with ext. But what about if some of the fields have types which depend on previous fields? It seems like I can't even state equality of such structures. My guess is that what people do is to define an equivalence on structures and then work with that instead of equality; is that right / is that a reasonably good way of doing things?

Minimum non-working example:

import tactic.ext

@[ext]
structure thingy {A : Type} :=
(tp : Type)
(dependent_field : tp → Type)

theorem thingy_eq {A : Type} (T1 T2 : @thingy A) (tp_eq : T1.tp = T2.tp) (df_eq : T1.dependent_field = T2.dependent_field) : T1 = T2 := sorry

This gives the error:

type mismatch at application
  T1.dependent_field = T2.dependent_field
term
  T2.dependent_field
has type
  T2.tp → Type
but is expected to have type
  T1.tp → Type

Which makes sense to me: the typechecker doesn't know that these types are equal, and they aren't equal a priori. So I'm guessing that in Lean / DTT, a theorem like this just can't be stated. Is that right? How is equality / equivalence of structures with dependent fields dealt with?

---

More detail:

There's a good chance there's an XY problem here, since I tried to boil out a minimal thing I don't understand. What I'm actually trying to do is work with this (hand-rolled, maybe not-done-the-right-way) definition of category:

import tactic.ext

universe u

@[ext]
structure cat :=
(obj : Type u)
(hom : obj → obj → Type u)
(seq {a b c : obj} : hom a b → hom b c → hom a c)
(Id : Π (a : obj), hom a a)
(id_before : ∀ (a b : obj) (f : hom a b), seq (Id a) f = f)
(id_after : ∀ (a b : obj) (f : hom a b), seq f (Id b) = f)
(assoc {a b c d : obj}: ∀  (f : hom a b) (g : hom b c) (h : hom c d), seq (seq f g) h = seq f (seq g h))

def Opp (C : cat) : cat := cat.mk
C.obj
(λ a b, C.hom b a)
(λ {a b c} f g, C.seq g f)
(λ a, C.Id a)
(λ a b f, C.id_after b a f)
(λ a b f, C.id_before b a f)
(λ a b c d f g h, eq.symm ( C.assoc h g f ))

theorem opp_opp (C : cat) : Opp (Opp C) = C :=
begin
   have xx : (Opp (Opp C)).obj = C.obj, from by simp [Opp],
   ext,
   assumption, assumption, sorry, assumption, sorry, assumption, sorry,
end

What's a good way to work with equality / equivalence of cats?

(Should opp_opp be provable as stated?)

Other context:

With ext it's easy to (state and) show extensionality for structures with multiple fields (ding) or with a field with type a Prop that depends on another field (thing):

import tactic.ext

@[ext]
structure ding {A : Type} :=
(e : A)
(z : A)

theorem ding_ext {A : Type} (T1 T2 : @ding A) (e_eq : T1.e = T2.e) (b_eq : T1.z = T2.z) : T1 = T2 :=
begin ext, assumption, assumption end

def single {A : Type} (e : A) : Prop := ∀ a : A, a = e

@[ext]
structure thing {A : Type} :=
(e : A)
(single : single e)

theorem thing_eq {A : Type} (T1 T2 : @thing A) (e_eq : T1.e = T2.e) : T1 = T2 :=
begin ext, assumption end

This is sort of weird to me, given that single T1.e and single T2.e aren't definitionally the same Prop (right?). So what's going on with ext and how is equality of things working here? It seems like in the special case of dependent Props we're somehow getting around the obstruction?

Maybe related, though I don't really follow:
https://github.com/leanprover/lean/issues/550

An example of proving that equality of structures that I assume have fields that are dependently typed, though I don't follow what's happening (search "are equal"): https://github.com/groupoid/ground.zero/blob/master/ground_zero/algebra/group.lean

[Andrew Yang]

Equality (eq, =) are for terms of the same type. If the arguments are of different type, you can use heterogeneous equality (heq, ==) to state the equality between them. But heq are not pleasant to work with, and in your case the answer should be "equality between categories are evil and you should not talk about them".

[Andrew Yang]

You can see how mathlib defines equivalences in docs#category_theory.equivalence

[Andrew Yang]

Regarding the other question, lean has proof irrelevance, that is two props of the same type are considered (definitionally?) equal regardless of their definition.

[Tsvi Benson-Tilsen]

Thanks. I guess that mostly answers my question, though I'd want to know why equality between categories is evil (it seems fine mathematically).

I know about proof irrelevance, but I don't follow. What do you mean "two props of the same type"? Do you mean two proofs of the same Prop? What I'm confused about is that it seems like we have a proof T1.single : single T1.e and another proof T2.single : single T2.e, and the Props single T1.eand single T2.e aren't equal a priori / definitionally
.

[Andrew Yang]

I think equality of categories are also evil mathematically? You should always talk in terms of equivalences.

[Andrew Yang]

You can look at the type of the ext lemma generated (thing.ext). You can see that it only requires you to prove T1.e = T2.e. This suffices since lean can prove that T1.single == T2.single (via proof irrelevance) using this equality.

[Tsvi Benson-Tilsen]

Ok, so if I understand heterogeneous equality maybe I'll know why this makes sense. (For others's reference: 6.7 of https://leanprover.github.io/tutorial/tutorial.pdf)
Thanks.

[Kevin Buzzard]

Equality of categories is evil because the predicate "I am equal to C" is not isomorphism-invariant: you can have two isomorphic categories C and D and the predicate can be true for C but not D.

[Reid Barton]

This particular equality of categories is not that problematic, and you can prove it like this:
theorem opp_opp (C : cat) : Opp (Opp C) = C := by { cases C, refl }

[Reid Barton]

However, I think you would have trouble making use of this theorem anyways.