Library gaia_hydras.T2Bridge

Bridge between Hydra-battle's and Gaia's T1 (Experimental)


From mathcomp Require Import all_ssreflect zify.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic T2 Gamma0.

From gaia Require Export ssete9.
Import Gamma0.

Set Implicit Arguments.


Hydra-Battles' type for ordinal terms below Gamma00
Check Gamma0.T2.T2.
Print Gamma0.T2.T2.
#[global] Notation hT2 := hydras.Gamma0.T2.T2.

Gaia's type for ordinal terms below epsilon0
#[global] Notation T2 := ssete9.Gamma0.T2.

#[global] Notation hcons := gcons.
#[global] Notation hzero := hydras.Gamma0.T2.zero.

Fixpoint h2g (alpha : hT2) : T2 :=
  match alpha with
    hzerozero
  | hcons a b n ccons (h2g a) (h2g b) n (h2g c)
  end.

Fixpoint g2h (alpha : T2) : hT2 :=
  match alpha with
    zerohzero
  | cons a b n chcons (g2h a)(g2h b) n (g2h c)
  end.

Lemma h2g_g2hK : cancel g2h h2g.

Lemma g2h_h2gK : cancel h2g g2h.

Lemma g2h_eqE (a b: T2) : g2h a = g2h b a = b.

Lemma h2g_eqE (a b :hT2) : h2g a = h2g b a = b.


Check (fun a b : hT2compare a b).

About T2lt.