Notation " [ a ] " := (inhabited a).

Definition join : (A : Type), [[A]][A]
:= fun A mmatch m with inhabits mm end.

Definition map : (A B : Type), (AB) → [A][B]
:= fun A B f mmatch m with inhabits xinhabits (f x) end.

Definition lift : (A : Type), A[A]
:= inhabits.

Definition choice := A (B : AType),
( x, [ B x ]) → [ x, B x ].

Lemma map_composition : A B C (f : BC) (g : AB) (m : [A]),
map A C (fun yf (g y)) m = map B C f (map A B g m).
Proof.
intros A B C f g m.
refine (match m with inhabits x_ end).
reflexivity.
Qed.

Lemma map_id : A (m : [A]),
map A A (fun yy) m = m.
Proof.
intros A m.
refine (match m with inhabits x_ end).
reflexivity.
Qed.

Lemma map_lift : A B (f : AB) (x : A),
map A B f (lift A x) = lift B (f x).
Proof.
auto.
Qed.

Lemma join_map_join : A (m : [[[A]]]),
join A (map [[A]] [A] (join A) m) = join A (join [A] m).
Proof.
intros A m.
refine (match m with inhabits x_ end).
reflexivity.
Qed.

Lemma join_map_lift : A (m : [A]),
join A (map A [A] (lift A) m) = m.
Proof.
intros A m.
refine (match m with inhabits x_ end).
reflexivity.
Qed.

Lemma join_lift : A (m : [A]),
join A (lift [A] m) = m.
Proof.
auto.
Qed.

Lemma join_map_map : A B (f : AB) (m : [[A]]),
join B (map [A] [B] (map A B f) m) = map A B f (join A m).
Proof.
intros A B f mm.
refine (match mm with inhabits x_ end).
reflexivity.
Qed.