(* Definitions of the Kuratowski-finite sets via a HIT *)
Require Import HoTT HitTactics.
Require Export notation.

Module Export FSet.
  Section FSet.
    Private Inductive FSet (A : Type) : Type :=
    | E : FSet A
    | L : A -> FSet A
    | U : FSet A -> FSet A -> FSet A.

    Global Instance fset_empty : forall A, hasEmpty (FSet A) := E.
    Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L.
    Global Instance fset_union : forall A, hasUnion (FSet A) := U.

    Variable A : Type.

    Axiom assoc : forall (x y z : FSet A),
        x ∪ (y ∪ z) = (x ∪ y) ∪ z.

    Axiom comm : forall (x y : FSet A),
        x ∪ y = y ∪ x.

    Axiom nl : forall (x : FSet A),
        ∅ ∪ x = x.

    Axiom nr : forall (x : FSet A),
        x ∪ ∅ = x.

    Axiom idem : forall (x : A),
        {|x|} ∪ {|x|} = {|x|}.

    Axiom trunc : IsHSet (FSet A).

  End FSet.

  Arguments assoc {_} _ _ _.
  Arguments comm {_} _ _.
  Arguments nl {_} _.
  Arguments nr {_} _.
  Arguments idem {_} _.

  Section FSet_induction.
    Variable A: Type.
    Variable  (P : FSet A -> Type).
    Variable  (H :  forall X : FSet A, IsHSet (P X)).
    Variable  (eP : P ∅).
    Variable  (lP : forall a: A, P {|a|}).
    Variable  (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)).
    Variable  (assocP : forall (x y z : FSet A)
                               (px: P x) (py: P y) (pz: P z),
                  assoc x y z #
                        (uP x (y ∪ z) px (uP y z py pz))
                  =
                  (uP (x ∪ y) z (uP x y px py) pz)).
    Variable  (commP : forall (x y: FSet A) (px: P x) (py: P y),
                  comm x y #
                       uP x y px py = uP y x py px).
    Variable  (nlP : forall (x : FSet A) (px: P x),
                  nl x # uP ∅ x eP px = px).
    Variable  (nrP : forall (x : FSet A) (px: P x),
                  nr x # uP x ∅ px eP = px).
    Variable  (idemP : forall (x : A),
                  idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x).

    (* Induction principle *)
    Fixpoint FSet_ind
             (x : FSet A)
             {struct x}
      : P x
      := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
          | E => fun _ _ _ _ _ _ => eP
          | L a => fun _ _ _ _ _ _ => lP a
          | U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
          end) H assocP commP nlP nrP idemP.

  End FSet_induction.

  Section FSet_recursion.

    Variable A : Type.
    Variable P : Type.
    Variable H: IsHSet P.
    Variable e : P.
    Variable l : A -> P.
    Variable u : P -> P -> P.
    Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
    Variable commP : forall (x y : P), u x y = u y x.
    Variable nlP : forall (x : P), u e x = x.
    Variable nrP : forall (x : P), u x e = x.
    Variable idemP : forall (x : A), u (l x) (l x) = l x.

    Definition FSet_rec : FSet A -> P.
    Proof.
      simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _)
      ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
      - apply e.
      - apply l.
      - intros x y ; apply u.
      - apply assocP.
      - apply commP.
      - apply nlP.
      - apply nrP.
      - apply idemP.
    Defined.

  End FSet_recursion.

  Instance FSet_recursion A : HitRecursion (FSet A) :=
    {
      indTy := _; recTy := _;
      H_inductor := FSet_ind A; H_recursor := FSet_rec A
    }.

End FSet.

Lemma union_idem {A : Type} : forall x: FSet A, x ∪ x = x.
Proof.
  hinduction ; try (intros ; apply set_path2).
  - apply nl.
  - apply idem.
  - intros x y P Q.
    rewrite assoc.
    rewrite (comm x y).
    rewrite <- (assoc y x x).
    rewrite P.
    rewrite (comm y x).
    rewrite <- (assoc x y y).
    f_ap.
Defined.