module TypeAlias;

inductive T {
 t : T;
};

inductive T2 {
 t2 : T2;
};

alias : Type;
alias ≔ T;

x : alias;
x ≔ t;

id : Type → Type;
id x ≔ x;

infixr 9 ⊙;
⊙ : (Type → Type) → (Type → Type) → Type → Type;
⊙ f g x ≔ f (g x);

x2 : (id ⊙ id) alias;
x2 ≔ t;

flip : (Type → Type → Type) → id Type → Type → (id ⊙ id) Type;
flip f a b ≔ f b a;

inductive Pair (A : Type) (B : Type) {
 mkPair : id T → id (id A) → B → Pair A B;
};

p : {A : Type} → A → Pair A A;
p a ≔ mkPair t a a;

x' : flip Pair (id _) T2;
x' ≔ mkPair x t2 t;

end;