Zulip Chat Archive

Stream: general

Topic: a mutual def question


view this post on Zulip Scott Morrison (Apr 08 2021 at 09:12):

I know the usual answer to questions about mutual def is "don't", but let me try. :-)

Is there any way to get

import category_theory.category

open category_theory

universes v u

variables {C : Type u} [category.{v} C]

variables (O : C  C) (π : Π X, O X  X)
variables (L : Π {X Y : C} (f : X  Y), C) (δ : Π {X Y : C} (f : X  Y), L f  X)

mutual def X, d (Z : C)
with X :   C
| 0 := Z
| 1 := O Z
| (n+2) := L (d n)
with d : Π n, X (n+1)  X n
| 0 := π Z
| (n+1) := δ (d n)

to work?

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:14):

The error messages are ill-formed match/equations expression on the mutual def line, and then

equation type mismatch, term
  π Z
has type
  O Z  Z
but is expected to have type
  X (0 + 1)  X 0

on the d 0 line, and then

equation type mismatch, term
  δ (d n)
has type
  L (d n)  X (n + 1)
but is expected to have type
  X (n + 1 + 1)  X (n + 1)

on the d (n+1) line.

Both errors look like they actually typecheck to me!

view this post on Zulip Gabriel Ebner (Apr 08 2021 at 09:15):

This is not supported. The types need to type check without unfolding the new definitions.

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:15):

Okay!

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:21):

On the other hand

def B (Z : C) :   Σ (X Y : C), X  Y
| 0 := O Z, Z, π Z
| (n+1) := L (B n).2.2, (B n).1, δ (B n).2.2

def X (Z : C) (n : ) : C := (B O π @L @δ Z n).2.1

def d (Z : C) (n : ) : X O π @L @δ Z (n+1)  X O π @L @δ Z n :=
(B O π @L @δ Z n).2.2

seems to do the job.

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:23):

(For those following along at home, this is attempting to construct projective resolutions.)

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:56):

#7111

view this post on Zulip Scott Morrison (Apr 08 2021 at 09:57):

(Particularly here and here.)


Last updated: May 14 2021 at 21:11 UTC