Define sequence of types and functions by induction

Stream: new members

[Gabin Kolly]

What is the usual way to construct a sequence of types and functions between these types, when to construct the (n+1)th term you will sometimes need the whole composition of functions from the m th term to the n th term, for some m?
I can be more precise about the setup of my problem, if it helps (but I think it is probably just confusing). I have:

1. a type T0
2. a function F that takes as input two types A and B and a function A -> B, and outputs a type C
3. a function F' that takes as input two types A and B and a function f : A -> B and outputs a function B -> F A B f
4. a function G that takes as input an integer n and a type B, and outputs a type A.
5. a function G' that takes as input an integer n and a type B, and outputs a function G n B -> A
6. a function H that takes as input a positive integer n, and outputs a positive integer m smaller or equal.
   Now, I want to construct recursively a sequence T0 =: A_0, A_1, A_2, ... and a sequence of functions f_n : A_n -> A_{n+1}, with A_{n+1} := F A_{(H n)} A_n (f_{n-1} ∘ ... ∘ f_{H n} ∘ (G' n A_{(H n})) and f_n := F' A_{(H n)} A_n (f_{n-1} ∘ ... ∘ f_{H n} ∘ (G' n A_{(H n})).

I was thinking that perhaps the best solution was to define the function S that takes as input i : ℕ, and outputs a pair consisting of a type A and a function that takes as input j : ℕ and j <= i, and outputs a function (S j).1 -> (S i).1, such that A_n is given by (S n).1 and the function f_n is given by (S (n+1)).2 n _

[Gabin Kolly]

Ok, here is a simpler question. It seems that the following definition by mutual recursion is not allowed:

mutual
  def growing_sequence : ℕ → Type w := by
    sorry

  def directed_system (i : ℕ) (j : ℕ) (h : i ≤ j) : growing_sequence i → growing_sequence j := by
    sorry
end

Is there a clean way to construct directed system by recursion in general?

[Mario Carneiro]

it would help to have a MWE of the definition you want

[Mario Carneiro]

@Gabin Kolly I started writing your conditions in lean and ran into the issue that step 5 contains an unknown identifier A

[Mario Carneiro]

Here's my attempt at writing the requirements in lean:

import Std
import Mathlib.Init.Data.Nat.Notation

axiom T0 : Type
axiom F (A B : Type) (f : A → B) : Type
axiom F' (A B : Type) (f : A → B) : B → F A B f
axiom G (n : ℕ) (B : Type) : Type
axiom G' (n : ℕ) (B : Type) : B → B
axiom H : ℕ → ℕ
axiom H_le (n : ℕ) : H n ≤ n

def A : ℕ → Type := sorry
def f (n : ℕ) : A n → A (n + 1) := sorry

def fs (m n : ℕ) (h : m ≤ n) : A m → A n :=
  if eq : m = n then
    eq ▸ id
  else
    match n with
    | n + 1 => f n ∘ fs m n (Nat.le_of_lt_succ (Nat.lt_of_le_of_ne h eq))
    | 0 => eq.elim (Nat.le_zero.1 h)

theorem A_zero : A 0 = T0 := sorry
theorem A_succ (n : ℕ) : A (n + 1) = F (A (H n)) (A n) (fs (H n) n (H_le n) ∘ G' n (A (H n))) := sorry
theorem f_def (n : ℕ) : f n = A_succ n ▸ F' (A (H n)) (A n) _ := sorry

[Mario Carneiro]

And here's a construction that works:

import Std
import Mathlib.Init.Data.Nat.Notation

axiom T0 : Type
axiom F (A B : Type) (f : A → B) : Type
axiom F' (A B : Type) (f : A → B) : B → F A B f
axiom G (n : ℕ) (B : Type) : Type
axiom G' (n : ℕ) (B : Type) : B → B
axiom H : ℕ → ℕ
axiom H_le (n : ℕ) : H n ≤ n

noncomputable def system : ℕ → (A : Type) × (ℕ → (B : Type) × (B → A))
  | 0 => ⟨T0, fun _ => ⟨_, id⟩⟩
  | n+1 =>
    let ⟨A, fs⟩ := system n
    let ⟨B, g⟩ := fs (H n)
    let f1 := F' B A (g ∘ G' n B)
    ⟨F B A (g ∘ G' n B), fun m =>
      if m ≤ n then
        let ⟨C, k⟩ := fs m; ⟨C, f1 ∘ k⟩
      else
        ⟨_, id⟩⟩

def A (n : ℕ) : Type := (system n).1

theorem system_eq {m n} (h : m ≤ n) : ((system n).2 m).1 = A m := by
  match n with
  | 0 => cases h; rfl
  | n+1 =>
    simp [system]; split <;> simp <;> rename_i h'
    · apply system_eq h'
    · cases (Nat.le_or_eq_of_le_succ h).resolve_left h'
      rfl

noncomputable def f (n : ℕ) : A n → A (n + 1) := system_eq (Nat.le_succ _) ▸ ((system (n+1)).2 n).2

[Gabin Kolly]

Thank you very much for your help!
Sorry for not giving a MWE, I thought I would get a high-level answer, not an exact one! But it was very useful!
I have some trouble with proving anything about the functions of the system though, for example this simple result:

theorem system_succ (n : ℕ) :
    ((system n).2 n).2.comp
      (system_eq (Nat.le_refl n) ▸ id) =
      id (α := A n) := by
  match n with
  | 0 => rfl
  | n+1 => sorry

I cannot find how to prove it. The state at the sorry is

(Sigma.snd (system (n + 1)) (n + 1)).snd ∘
    Eq.rec (motive := fun x h ↦ x → (Sigma.snd (system (n + 1)) (n + 1)).fst) id _ =
  id

If I try to do simp [system], then the first function is based on an if-then-else that I don't manage to simplify even though the condition is n+1 <= n, which should simplifiable, but I don't know how to do it. The second term is a recursion on an equality, and I'm also at a loss if something can be done.