From a95ddea6ca4e568921a533782df94ce7a588eec2 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Tue, 20 Jun 2017 11:33:13 +0200
Subject: [PATCH] FSet is a strong powerset monad

---
 FiniteSets/_CoqProject |  1 +
 FiniteSets/monad.v     | 67 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+)
 create mode 100644 FiniteSets/monad.v

diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index 3d1de57..85d0935 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -8,3 +8,4 @@ empty_set.v
 ordered.v
 cons_repr.v
 Lattice.v
+monad.v
diff --git a/FiniteSets/monad.v b/FiniteSets/monad.v
new file mode 100644
index 0000000..b63f376
--- /dev/null
+++ b/FiniteSets/monad.v
@@ -0,0 +1,67 @@
+(* [FSet] is a (strong and stable) finite powerset monad *)
+Require Import definition properties.
+Require Import HoTT HitTactics.
+
+Definition fmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
+Proof.
+  intro f.
+  hrecursion.
+  - exact ∅.
+  - intro a. exact {| f a |}.
+  - exact U.
+  - apply assoc.
+  - apply comm.
+  - apply nl.
+  - apply nr.
+  - simpl. intro x. apply idem.
+Defined.
+
+Lemma fmap_1 {A : Type} `{Funext} : @fmap A A idmap = idmap.
+Proof.
+  apply path_forall.
+  intro x. hinduction x; try (cbn; intros; f_ap);
+             try (intros; apply set_path2).
+Defined.
+
+Lemma fmap_compose {A B C : Type} `{Funext} (f : A -> B) (g : B -> C) :
+  fmap (g o f) = fmap g o fmap f.
+Proof.
+  apply path_forall. intro x.
+  hrecursion x; try (cbn; intros; f_ap);
+    try (intros; apply set_path2).
+Defined.
+
+Definition join {A : Type} : FSet (FSet A) -> FSet A.
+Proof.
+hrecursion.
+- exact ∅.
+- exact idmap.
+- exact U.
+- apply assoc.
+- apply comm.
+- apply nl.
+- apply nr.
+- simpl. apply union_idem.
+Defined.
+
+Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) :
+  join (fmap join X) = join (join X).
+Proof.
+  hrecursion X; try (cbn; intros; f_ap);
+    try (intros; apply set_path2).
+Defined.
+
+Lemma join_return_1 {A : Type} (X : FSet A) :
+  join ({| X |}) = X.
+Proof. reflexivity. Defined.
+
+Lemma join_return_fmap {A : Type} (X : FSet A) :
+  join ({| X |}) = join (fmap (fun x => {|x|}) X).
+Proof.
+  hrecursion X; try (cbn; intros; f_ap);
+    try (intros; apply set_path2).
+Defined.
+
+Lemma join_fmap_return_1 {A : Type} (X : FSet A) :
+  join (fmap (fun x => {|x|}) X) = X.
+Proof. refine ((join_return_fmap _)^ @ join_return_1 _). Defined.