Library gaia_hydras.T2Bridge
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
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
hzero ⇒ zero
| hcons a b n c ⇒ cons (h2g a) (h2g b) n (h2g c)
end.
Fixpoint g2h (alpha : T2) : hT2 :=
match alpha with
zero ⇒ hzero
| cons a b n c ⇒ hcons (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 : hT2 ⇒ compare a b).
About T2lt.
#[global] Notation hcons := gcons.
#[global] Notation hzero := hydras.Gamma0.T2.zero.
Fixpoint h2g (alpha : hT2) : T2 :=
match alpha with
hzero ⇒ zero
| hcons a b n c ⇒ cons (h2g a) (h2g b) n (h2g c)
end.
Fixpoint g2h (alpha : T2) : hT2 :=
match alpha with
zero ⇒ hzero
| cons a b n c ⇒ hcons (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 : hT2 ⇒ compare a b).
About T2lt.