## Stream: general

### Topic: a mutual def question

#### 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?

#### 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!

#### Gabriel Ebner (Apr 08 2021 at 09:15):

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

Okay!

#### 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.

#### Scott Morrison (Apr 08 2021 at 09:23):

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

#7111

#### Scott Morrison (Apr 08 2021 at 09:57):

(Particularly here and here.)

Last updated: May 14 2021 at 21:11 UTC