(motive : (format : Std.Time.Year) → Std.Time.TypeFormat (Std.Time.Modifier.u format) → Sort u_1) →
  (format : Std.Time.Year) →
    (data : Std.Time.TypeFormat (Std.Time.Modifier.u format)) →
      ((data : Std.Time.TypeFormat (Std.Time.Modifier.u Std.Time.Year.any)) → motive Std.Time.Year.any data) →
        ((data : Std.Time.TypeFormat (Std.Time.Modifier.u Std.Time.Year.twoDigit)) →
            motive Std.Time.Year.twoDigit data) →
          ((data : Std.Time.TypeFormat (Std.Time.Modifier.u Std.Time.Year.fourDigit)) →
              motive Std.Time.Year.fourDigit data) →
            ((n : ℕ) →
                (data : Std.Time.TypeFormat (Std.Time.Modifier.u (Std.Time.Year.extended n))) →
                  motive (Std.Time.Year.extended n) data) →
              motive format data