Syntax question about using assumptions

Stream: new members

[Jakob Scholbach]

How can I use assumptions I previously made in order to formulate new conditions? Concretely, I am trying to define something like this:

def closed_under_composition : Prop := ∀ i j : arrow C, i.right = j.left → Z i → Z j → Z (i.hom ≫ j.hom).

Here C is a category and Z : arrow C → Prop. This raises an error since ≫ is only defined whenever i.right = j.left holds. What is the correct syntax to achieve this?

[Scott Morrison]

Don't use equality of objects, it is evil. :-)

[Scott Morrison]

(And when you do really need to use it, use eq_to_hom to lift the equality to a morphism.)

[Jakob Scholbach]

re evil: But surely not to talk about composites of morphisms?

[Scott Morrison]

there we use dependent typing

[Scott Morrison]

{X Y Z : C} (f : X \hom Y) (g : Y \hom Z) --- no equations involved!

[Jakob Scholbach]

Yes, sure. The thing is, I want to build my notions on objects of arrow C.

[Scott Morrison]

Maybe there is an #xy to this?

[David Wärn]

You can curry Z : Arrow C → Prop to Z' : Π {a b : C}, (a ⟶ b) → Prop

[Jakob Scholbach]

@Scott Morrison Possibly! - The question above is really a general syntax question, not specifically about composing morphisms. Phrased more generally: given some function f(x,y) which needs a hypothesis h(x,y) for it to be defined, how do I define a condition on x,y saying something like : assuming h(x,y), I want f(x,y) to hold.

[Scott Morrison]

If you _really_ need to do something directly on arrow you could define a composable predicate on a pair of arrows, and a new composition function which takes two functions and the evidence they are composable.

[Scott Morrison]

Hmm, I'm not sure what your more general statement actually means.

[Scott Morrison]

I'd interpret "given some function f(x,y) which needs a hypothesis h(x,y) for it to be defined" as something like:

variables (X : Type) (P : X -> Prop)
variables (f : { x // P x } -> Prop)
variables (g : \forall x, f x)

[Scott Morrison]

(reducing from two variables x,y to one. Here your h is my P, and then my g says "assuming h, then f"

[Scott Morrison]

But I'm not really sure how that is related to your original closed_under_composition. (Sorry if I'm being daft. It's late here. :-)

[David Wärn]

David Wärn said:

You can curry Z : Arrow C → Prop to Z' : Π {a b : C}, (a ⟶ b) → Prop

Here's how to express a predicate on morphisms being closed under composition in this curried setup

variables {C : Type} [category C]
def closed_under_composition (Z : Π {a b : C}, (a ⟶ b) → Prop) : Prop :=
∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), Z f → Z g → Z (f ≫ g)

[Scott Morrison]

Yeah -- I think what's going on here is that Jakob wants to know why we're not just telling him how to make use of i.right = j.left so that i.hom ≫ j.hom actually makes sense.

[Jakob Scholbach]

@Scott Morrison : It is surely me who is lame! Here is another example, I am sorry for my imprecisions above. I have a function my_fun that is only defined for positive numbers. How do I define another function f that, given an x and the assumption that x is positive, produces an output depending on my_fun x

def hyp (x : ℕ) : Prop := x > 0
def my_fun (x : ℕ) : hyp x → ℕ := begin intro h, exact x end

def f (x : ℕ) : ℕ := hyp x → (my_fun x) + 1

[Scott Morrison]

and that problem is that this is a bit of a subtle thing, precisely because we're using dependent type theory.

[Jakob Scholbach]

Scott Morrison said:

Yeah -- I think what's going on here is that Jakob wants to know why we're not just telling him how to make use of i.right = j.left so that i.hom ≫ j.hom actually makes sense.

Yes, that is my question.

[Scott Morrison]

Just write def f (x : ℕ) (h : hyp x) : ℕ := my_fun x h + 1

[Scott Morrison]

but this is totally orthogonal to your original question. :-)

[Scott Morrison]

The point is that we could use h : i.right = j.left in two ways:

[Scott Morrison]

1. write i.hom \gg eq_to_hom h \gg j.hom

[Scott Morrison]

(however then you'll be talking about Z of some other thing...)

[Scott Morrison]

2. write by { subst h, exact i.hom \gg j.hom }

[Scott Morrison]

but again, this is _not_ i.hom \gg j.hom

[Scott Morrison]

(or we could do some fancier things using eq.rec (think "transport through a type family over a path"), which I won't attempt to write out here)

[Scott Morrison]

But fundamentally, i.hom \gg j.hom itself will just never make sense: the hypothesis h : i.right = j.left is a proposition, not a typing judgement, and unfortunately those are different things in dependent type theory.

[Scott Morrison]

this probably is because i.hom and j.hom live in type families indexed by the source and target, and when you have equations in the indexing type of a type family, you only get canonical functions between the fibres, not actual identifications.

[Scott Morrison]

I fear I am only making things worse. :-)

[Jakob Scholbach]

Aha, would a layman (=for me)-summary be something like this: ? h just knows that i.right and j.left can be identified (somehow), but this is not enough to make them equal (so that the morphisms can be composed)?

[Jakob Scholbach]

Above you commented "you could define a composable predicate on a pair of arrows, and a new composition function which takes two functions and the evidence they are composable". How would that be done then?

[Scott Morrison]

Something like this. This is the price we pay for the wonders of dependent type theory. :-)

[David Wärn]

It is enough but you have to tell Lean how to use h

[David Wärn]

def compose (f g : arrow C) (h : f.right = g.left) : arrow C :=
⟨_, _, f.hom ≫ eq_to_hom h ≫ g.hom⟩

def closed_under_composition (Z : arrow C → Prop) :=
∀ (f g : arrow C) (h : f.right = g.left), Z f → Z g → Z (compose f g h)

[Scott Morrison]

exactly

[Jakob Scholbach]

OK, thanks a lot to both of you. Learned another thing!

[Scott Morrison]

Now if h is actually rfl, then eq_to_hom h will simplify (e.g. via simp) to \b1 f.right, and then f.hom \gg eq_to_hom \gg g.hom will simplify to f.hom \gg h.hom.

[Scott Morrison]

But until you know that it is actually rfl then it doesn't simplify.

[Eric Wieser]

docs#category_theory.eq_to_hom is a category-ified docs#cast, right?

[Johan Commelin]

@Eric Wieser yep

[David Wärn]

It might be more accurate to say that composing a morphism with an eq_to_hom plays the same role as cast (docs#category_theory.congr_arg_mpr_hom_left shows that the two agree)

[Eric Wieser]

That simp lemma worries me a bit - I don't think it can ever fire, as docs#eq_mpr_eq_cast should fire first