a mutual def question

Stream: general

[Scott Morrison]

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]

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]

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

[Scott Morrison]

Okay!

[Scott Morrison]

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]

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

[Scott Morrison]

#7111

[Scott Morrison]

(Particularly here and here.)