From Companion Require Import prelim companion companion_mu.
Require Import sysf.

Definition TyN n := iter n Fty bot.
Definition STy R := \sup_(n | TyN n <= R) TyN n.

Lemma T_TyN n :
  T (Fty : _^r -> _^r) (TyN n).
Proof.
  elim: n => /=[|n ih]. rewrite suplat_bot. exact: T_lim. exact: T_step.
Qed.

Lemma TyN_inc n :
  TyN n <= Fty (TyN n).
Proof.
  elim: n => [|n ih] /=. exact: botE. exact: mono.
Qed.

Global Instance TyN_mono : monotone TyN.
Proof.
  move=> m n /leP. elim=> // k _ -> /=. exact: TyN_inc.
Qed.

Global Instance STy_mono : monotone STy.
Proof.
  move=> R S le_r_s. apply: supEc => n h. apply: supIc _ le_refl. by rewrite h.
Qed.

Lemma ty_sty :
  Ty <= STy.
Proof.
  apply: ind_upto_above => /= R. apply: ind_upto R => /= R ih.
  rewrite {1}ih => {ih}. move=> Gamma s A []{s A}.
  - move=> x ltn. exists 1. split. apply: Fty_mono. exact: botE.
    rewrite/=. by constructor.
  - move=> A B s [n [p q]]. exists n.+1. split. by rewrite -p.
    move=> /=. by constructor.
  - move=> A B s t [m [p1 q1]] [n [p2 q2]]. case/orP: (leq_total m n) => h.
    + exists n.+1; split. exact: Fty_mono. apply: Fty_app q2. exact: (TyN_mono h).
    + exists m.+1; split. exact: Fty_mono. apply: Fty_app q1 _. exact: (TyN_mono h).
  - move=> A s [m [p q]]. exists m.+1; split. exact: Fty_mono. by constructor.
  - move=> A B s [m [p q]]. exists m.+1; split. exact: Fty_mono. by constructor.
Qed.

Lemma sty_ty :
  STy <= Ty.
Proof.
  move=>/=R. apply: supEc => i h. apply: supIc (TyN i) _ _. split.
  - exact: T_TyN.
  - exact: h.
  - reflexivity.
Qed.

Theorem correspondence :
  Ty = STy.
Proof.
  apply: le_eq. exact: ty_sty. exact: sty_ty.
Qed.