challenge: constructively generate nerve data

Stream: Infinity-Cosmos

[Emily Riehl]

Here is a challenge I'm hoping some one will take on. The following noncomputable def is fundamental to showing that nerves of categories are strict segal simplicial sets (meaning the data of a simplex is equivalent to the data of the composable path of edges along its spine).

section mkOfObjOfMapSucc

variable (obj : Fin (n + 1) → C) (mapSucc : ∀ (i : Fin n), obj i.castSucc ⟶ obj i.succ)

lemma mkOfObjOfMapSucc_exists : ∃ (F : ComposableArrows C n) (e : ∀ i, F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ =
      (e ⟨i, _⟩).inv ≫ F.map' i (i + 1) ≫ (e ⟨i + 1, _⟩).hom := by
  revert obj mapSucc
  induction' n with n hn
  · intro obj _
    exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  · intro obj mapSucc
    obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp only [← Fin.mk_zero]
      simp
    · exact h i (by valid)

/-- Given `obj : Fin (n + 1) → C` and `mapSucc i : obj i.castSucc ⟶ obj i.succ`
for all `i : Fin n`, this is `F : ComposableArrows C n` such that `F.obj i` is
definitionally equal to `obj i` and such that `F.map' i (i + 1) = mapSucc ⟨i, hi⟩`. -/
noncomputable def mkOfObjOfMapSucc : ComposableArrows C n :=
  (mkOfObjOfMapSucc_exists obj mapSucc).choose.copyObj obj
    (mkOfObjOfMapSucc_exists obj mapSucc).choose_spec.choose

Here is the challenge. Can this be made computable?

[Emily Riehl]

This has cascading non-computability effects for anything that uses the abstraction boundary of Strict Segal simplicial sets in place of nerves of categories (which is essentially the only example).

[Aaron Liu]

Well it's not noncomputable...

import Mathlib

open CategoryTheory

section mkOfObjOfMapSucc

variable {C : Type*} [Category C]

def mkOfObjOfMapSucc_exists {n} (obj : Fin (n + 1) → C) (mapSucc : ∀ (i : Fin n), obj i.castSucc ⟶ obj i.succ) :
    (F : ComposableArrows C n) ×' (e : ∀ i, F.obj i ≅ obj i) ×'
    ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ =
      (e ⟨i, _⟩).inv ≫ F.map' i (i + 1) ≫ (e ⟨i + 1, _⟩).hom :=
  match n with
  | 0 => ⟨.mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  | n + 1 =>
    let hn := mkOfObjOfMapSucc_exists (fun i => obj i.succ) (fun i => mapSucc i.succ)
    ⟨hn.fst.precomp (mapSucc 0 ≫ (hn.snd.fst 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => hn.snd.fst _, fun i hi => by
      obtain _ | i := i
      · simp only [← Fin.mk_zero]
        simp
      · exact hn.snd.snd i (by valid)⟩

/-- Given `obj : Fin (n + 1) → C` and `mapSucc i : obj i.castSucc ⟶ obj i.succ`
for all `i : Fin n`, this is `F : ComposableArrows C n` such that `F.obj i` is
definitionally equal to `obj i` and such that `F.map' i (i + 1) = mapSucc ⟨i, hi⟩`. -/
def mkOfObjOfMapSucc {n} (obj : Fin (n + 1) → C) (mapSucc : ∀ (i : Fin n), obj i.castSucc ⟶ obj i.succ) : ComposableArrows C n :=
  (mkOfObjOfMapSucc_exists obj mapSucc).fst.copyObj obj
    (mkOfObjOfMapSucc_exists obj mapSucc).snd.fst

[Emily Riehl]

@Aaron Liu thank you. This is really great. You've confirmed my instincts that this should be fully constructive.

I've just pushed your code to PR #23848 that attempts to do a bit of golfing of something @Mario Carneiro and I merged into mathlib in March. I'm sure a lot of proofs there could be cleaned up further so if you're interested I can explain more what all of this is about. Or if you're otherwise occupied then feel free to ignore and thanks!