Played with quantifiers a bit.

logic.v

(* I'm experimenting with axiomizing a fragment of IZF using higher
 order abstract syntax and a tagless final style.

I'm completely lost with a lot of dark details of Coq's notations
unfortunately.
 *)
Require Import Coq.Unicode.Utf8.
Require Coq.Program.Basics.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.SetoidClass.
Require Coq.Logic.FunctionalExtensionality.

From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".

Import IfNotations.

Declare Scope entail.
Declare Scope prop.

Delimit Scope entail with entail.
Delimit Scope prop with prop.

Reserved Notation "P ⊢ Q" (at level 90).
Reserved Infix "∘" (at level 30, right associativity).

Module Type PropSymbols.
  Axiom prop: Type.
  Axiom entail: prop → prop → Prop.

  Bind Scope entail with entail.
  Bind Scope prop with prop.

  #[export]
  Declare Instance id: Reflexive entail.
  #[export]
  Declare Instance compose: Transitive entail.

  Axiom true: prop.
  Axiom false: prop.

  Axiom and: prop → prop → prop.
  Axiom or: prop → prop → prop.
  Axiom impl: prop → prop → prop.
End PropSymbols.

Module PropNotations (Import P: PropSymbols).
  Definition equiv P Q := Logic.and (entail P Q) (entail Q P).

  #[export]
   Instance equiv_Equivalence: Equivalence equiv.
  Proof.
    unfold equiv.
    exists.
    all: split.
    - reflexivity.
    - reflexivity.
    - destruct H.
      auto.
    - destruct H.
      auto.
    - destruct H, H0.
      rewrite H, H0.
      reflexivity.
    - destruct H, H0.
      rewrite H2, H1.
      reflexivity.
  Qed.

  #[export]
  Instance prop_Setoid: Setoid prop := { equiv := equiv }.

  Module PropNotations.
    Notation "P ⊢ Q" := (entail (P%prop) (Q%prop))  : type_scope.

    Notation "⊤" := true : prop.
    Notation "⊥" := false : prop.

    Notation "P ∧ Q" := (and (P%prop) (Q%prop)) : prop.
    Notation "P ∨ Q" := (or (P%prop) (Q%prop)) : prop.

    Notation "P → Q" := (impl (P%prop) (Q%prop)) : prop.

    Notation "¬ P" := (impl (P%prop) false) : prop.
    Notation "P ↔ Q" := (and (impl (P%prop) (Q%prop)) (impl (Q%prop) (P%prop))): prop.
  End PropNotations.
End PropNotations.

(* Define basic constructive propositional logic *)
Module Type PropositionalLogic.
  Include PropSymbols.
  Include PropNotations.
  Import PropNotations.

  Axiom tt: ∀ P, P ⊢ ⊤.
  Axiom absurd: ∀ P, ⊥ ⊢ P.

  Axiom fanout: ∀ {P Q R}, P ⊢ Q → P ⊢ R → P ⊢ Q ∧ R.
  Axiom π1: ∀ {P Q}, P ∧ Q ⊢ P.
  Axiom π2: ∀ {P Q}, P ∧ Q ⊢ Q.

  Axiom fanin: ∀ {P Q R}, P ⊢ R → Q ⊢ R → P ∨ Q ⊢ R.
  Axiom i1: ∀ {P Q}, P ⊢ P ∨ Q.
  Axiom i2: ∀ {P Q}, Q ⊢ P ∨ Q.

  Axiom Λ: ∀ {P Q R},
    Q ∧ P ⊢ R →
    P ⊢ (Q → R).
  Axiom eval: ∀ {P Q}, P ∧ (P → Q) ⊢ Q .
End PropositionalLogic.

Module EntailNotations (Import P: PropositionalLogic).
  Import P.PropNotations.

  Lemma uncurry {P Q R}: P ⊢ (Q → R) → Q ∧ P ⊢ R .
  Proof.
    intros f.
    eassert (f' := fanout π1 (compose _ _ _ π2 f)).
    rewrite f'.
    apply eval.
  Defined.

  Lemma yo {P Q}: (∀ R, R ⊢ P → R ⊢ Q) → P ⊢ Q.
  Proof.
    intro f.
    apply f.
    reflexivity.
  Defined.

  Module EntailNotations.
    Notation "f ∘ g" := (compose _ _ _ (g%entail) (f%entail)) : entail.
    Notation "⟨ x , y , .. , z ⟩" := (fanout .. (fanout (x%entail) (y%entail)) .. (z%entail)) : entail.
    Notation "[ x ; y ; .. ; z ]" := (fanin .. (fanin (x%entail) (y%entail)) .. (z%entail)) : entail.

    Open Scope entail.

    Ltac xyo R f := refine (yo (λ R f, _)).
    Ltac xdestruct x y z :=
      assert (y := π1 ∘ x) ;
      assert (z := π2 ∘ x) ;
      clear x.

    Ltac xtaut := refine (_ ∘ tt _).
    Ltac xabsurd := refine (absurd _ ∘ _).

    Ltac xsplit := refine ⟨ _, _ ⟩.
    Ltac xcase := refine [ _; _ ].

    Ltac xleft := refine (i1 ∘ _).
    Ltac xright := refine (i2 ∘ _).

    Ltac xfirst := refine (_ ∘ π1).
    Ltac xsecond := refine (_ ∘ π2).

    Ltac xcurry := refine (Λ _).
    Ltac xuncurry := refine (uncurry _).

    Tactic Notation "xyo" ident(R) ident(f) := xyo R f.
    Tactic Notation "xdestruct" hyp(x) ident(y) ident(z) := xdestruct x y z.
  End EntailNotations.
End EntailNotations.

Reserved Notation "'∃' x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "∀ x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "! x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "'∃!' x .. y , P" (at level 200, x binder, y binder, right associativity).

Reserved Notation "'ι' x , P" (at level 200, x name, right associativity).

Reserved Infix "≅" (at level 80).
Reserved Infix "∈" (at level 30, right associativity).
Reserved Infix "∉" (at level 30, right associativity).

Declare Scope term.
Delimit Scope term with term.

Reserved Notation "∅".
Reserved Notation "⋃ A" (at level 1).

Module Type FolSymbols.
  Include PropositionalLogic.
  Include EntailNotations.
End FolSymbols.

Module FolNotations (Import P: FolSymbols).
  Import PropNotations.
  Import EntailNotations.

  Class sort := {
      term: Type ;
      lim: (term → prop) → prop ;
      colim: (term → prop) → prop ;
      cong: term → term → prop ;
      definite: (term → prop) → term ;

      colim_intro: ∀ {P y}, P y ⊢ colim P ;
      colim_elim: ∀ {P Q},
        (∀ y, P y ⊢ Q) →
        colim P ⊢ Q ;

      lim_intro: ∀ {P Q},
        (∀ y, P ⊢ Q y) →
        P ⊢ lim Q ;
      lim_elim: ∀ P y,
        lim P ⊢ P y ;

      refl: ∀ x, ⊤ ⊢ cong x x ;
      subst: ∀ P x y, P x ∧ cong x y ⊢ P y ;

      unique P := lim (λ x, lim (λ y, impl (P x) (impl (P y) (cong x y)))) ;
      exists_unique P := and (colim P) (unique P) ;

      describe: ∀ (P: term → prop), exists_unique P == P (definite P)
  }.

  Coercion term: sort >-> Sortclass.

  Bind Scope term with term.

  Module Combinators.
    #[refine]
    Instance unit: sort := {
        term := Datatypes.unit ;
        lim P := P Datatypes.tt ;
        colim P := P Datatypes.tt ;
        cong _ _ := true ;
        definite _ := Datatypes.tt ;
    }.
    Proof.
      all: eauto.
      - intros ? [].
        reflexivity.
      - intros ? [].
        reflexivity.
      - intros.
        reflexivity.
      - intros ? [] [].
        rewrite π1.
        reflexivity.
      - intros ?.
        split.
        + rewrite π1.
          reflexivity.
        + refine ⟨id _, _⟩.
          xcurry.
          xcurry.
          xtaut.
          reflexivity.
    Qed.

    #[refine]
    Instance prod (A B: sort): sort := {
        term := A * B ;
        lim P := lim (λ a, lim (λ b, P (a, b))) ;
        colim P := colim (λ a, colim (λ b, P (a, b))) ;
        cong a b := (cong (fst a) (fst b) ∧ cong (snd a) (snd b)) %prop;
        definite P := (definite (λ a, exists_unique (λ b, P (a, b))),
                       definite (λ b, exists_unique (λ a, P (a, b))) ) ;
    }.
    Proof.
      - intros ? [].
        erewrite <- colim_intro.
        erewrite <- colim_intro.
        reflexivity.
      - intros ? ? ?.
        apply colim_elim.
        intro.
        apply colim_elim.
        intro.
        eauto.
      - intros ? ? p.
        apply lim_intro.
        intro.
        apply lim_intro.
        intro.
        apply p.
      - intros ? [].
        rewrite lim_elim.
        rewrite lim_elim.
        reflexivity.
      - intros [].
        cbn.
        xsplit.
        all: apply refl.
      - intros ? [] [].
        cbn.
        admit.
    Admitted.

    #[refine]
    Instance sum (A B: sort): sort := {
        term := A + B ;
        lim P := (lim (λ a, P (inl a)) ∧ lim (λ b, P (inr b)))%prop ;
        colim P := (colim (λ a, P (inl a)) ∨ colim (λ b, P (inr b)))%prop ;
        cong a b :=
        match a, b with
        | inl a, inl b => cong a b
        | inr a, inr b => cong a b
        | _, _ => false
        end ;
        definite P := inl (definite (λ a: A, P (inl a))) ;
    }.
    Proof.
    Admitted.
  End Combinators.

  Module FolNotations.
    Notation "P ≅ Q" := (cong (P%term) (Q%term)) : prop.

    Notation "'∃' x .. y , P" := (colim (λ x, .. (colim (λ y, P%prop)) .. )) : prop.
    Notation "'∀' x .. y , P" := (lim (λ x, .. (lim (λ y, P%prop)) .. )) : prop.

    Notation "'!' x .. y , P" := (unique (λ x, .. (unique (λ y, P%prop)) .. )) : prop.
    Notation "'∃!' x .. y , P" := (exists_unique (λ x, .. (exists_unique (λ y, P%prop)) .. )) : prop.

    Notation "'ι' x , P" := (definite (λ x, P%prop)) : term.
  End FolNotations.
End FolNotations.

(* Use a tagless final style to support higher order abstract syntax
in first order logic *)
Module Type FirstOrderLogic.
  Include FolSymbols.

  Include FolNotations.
  Import PropNotations.
  Include EntailNotations.

  Import FolNotations.
End FirstOrderLogic.

Reserved Notation "'XELIM' x .. y , P" (x binder, y binder, at level 200).
Reserved Notation "'XINTRO' x .. y , P" (x binder, y binder, at level 200).

Module FolEntailNotations (Import P: FirstOrderLogic).
  Import P.PropNotations.
  Import P.EntailNotations.
  Import P.FolNotations.

  Lemma lim_app `{sort} {P Q}: P ⊢ (∀ x, Q x) → ∀ y, P ⊢ Q y.
  Proof.
    intros f y.
    rewrite f.
    apply lim_elim.
  Defined.

  Lemma colim_app `{sort} {P Q}: (∃ x, P x) ⊢ Q → ∀ x, P x ⊢ Q.
  Proof.
    intros f y.
    rewrite colim_intro.
    apply f.
  Defined.

  Module FolEntailNotations.
    Notation "'XELIM' x .. y , P" := (colim_elim (λ x, .. (colim_elim (λ y, P%entail)) ..)): entail.
    Notation "'XINTRO' x .. y , P" := (lim_intro (λ x, .. (lim_intro (λ y, P%entail)) ..)): entail.

    Ltac xapp := refine (_ ∘ lim_elim _ _).
    Ltac xcointro := refine (colim_intro ∘ _).

    Ltac xelim x := refine (XELIM x, _).
    Ltac xintro x := refine (XINTRO x, _).

    Tactic Notation "xelim" ident(x) := xelim x.
    Tactic Notation "xintro" ident(x) := xintro x.
  End FolEntailNotations.
End FolEntailNotations.

Module Type DCatSymbols.
  Include FirstOrderLogic.

  Axiom cell: sort.

  (* north, south, west, east edges *)
  Axiom N: cell → cell.
  Axiom S: cell → cell.
  Axiom W: cell → cell.
  Axiom E: cell → cell.

  (* horiziontal/vertical composition *)
  Axiom hcomps: cell → cell → cell → prop.
  Axiom vcomps: cell → cell → cell → prop.
End DCatSymbols.

Module DCatNotations (Import P: DCatSymbols).
  Include FolNotations.
  Import PropNotations.
  Import FolNotations.

  Definition hcomp f g: cell := definite (hcomps f g).
  Definition vcomp f g: cell := definite (vcomps f g).

  Definition hmor c: prop := N c ≅ S c.
  Definition vmor c: prop := W c ≅ E c.
  Definition obj c: prop := hmor c ∧ vmor c.

  Module DCatNotations.
    Infix "-" := vcomp : term.
    Infix "||" := hcomp : term.
  End DCatNotations.
End DCatNotations.

Module Type DCat.
  Include DCatSymbols.
  Include PropNotations.
  Import FolNotations.
  Include DCatNotations.

  Import DCatNotations.

  (* See https://ncatlab.org/nlab/show/theory+of+categories and
  https://ncatlab.org/nlab/show/single-sorted+definition+of+a+category
  for inspiration *)
  Axiom NN: ⊤ ⊢ ∀ c, N (N c) ≅ N c.
  Axiom WW: ⊤ ⊢ ∀ c, W (W c) ≅ W c.
  Axiom SS: ⊤ ⊢ ∀ c, S (S c) ≅ S c.
  Axiom EE: ⊤ ⊢ ∀ c, E (E c) ≅ E c.

  Axiom hcomp_exists_unique: ⊤ ⊢ ∀ f g, W g ≅ E f ↔ ∃! h, hcomps f g h.
  Axiom vcomp_exists_unique: ⊤ ⊢ ∀ f g, N g ≅ S f ↔ ∃! h, vcomps f g h.

  Axiom W_hcomp: ⊤ ⊢ ∀ f g, W (f || g) ≅ W f.
  Axiom E_hcomp: ⊤ ⊢ ∀ f g, E (f || g) ≅ E g.

  Axiom N_vcomp: ⊤ ⊢ ∀ f g, N (f - g) ≅ N f.
  Axiom S_vcomp: ⊤ ⊢ ∀ f g, S (f - g) ≅ S f.

  Axiom hcomp_W: ⊤ ⊢ ∀ f, W f || f ≅ f.
  Axiom hcomp_E: ⊤ ⊢ ∀ f, f || E f ≅ f.
  Axiom vcomp_N: ⊤ ⊢ ∀ f, N f - f ≅ f.
  Axiom vcomp_S: ⊤ ⊢ ∀ f, f - S f ≅ f.
End DCat.

Module DCatEntailNotations (Import P: DCat).
  Import PropNotations.
  Import EntailNotations.
  Import FolNotations.
  Import DCatNotations.

  (* A vertical contravariant functor *)

End DCatEntailNotations.

Module Type Span.
  Include DCat.

  Import PropNotations.
  Import FolNotations.
  Import DCatNotations.

  (* Set (the horizontal edge)

    Assert a point exists.

    Next assert that Set is locally cartesian closed?
   *)

  Axiom unit_exists_unique:
    ⊤ ⊢ ∃! c, obj c
              ∧ ∀ a, obj a →
                     ∃! b, hmor b ∧ W b ≅ a ∧ E b ≅ c.

  (* Span (the vertical edge)

     Not really sure what to put here.
   *)

  (* forall vertical morphisms f there exists a unique vertical morphism g
     such that
     - source/targets are flipped
     - identity maps to identity
     - transpose of composition is contravariant

     FIXME define functors first
   *)
  Axiom transpose_exists_unique:
    ⊤ ⊢ ∀ f, vmor f →
        ∃! g, vmor g
        ∧ (N f ≅ S g ∧ S f ≅ N g)
        ∧ (obj f → g ≅ f)
  .

End Span.

Module Type IzfSymbols.
  Include FirstOrderLogic.

  Axiom set: sort.

  Axiom mem: set → set → prop.
End IzfSymbols.

Module IzfNotations (Import P: IzfSymbols).
  Include FolNotations.
  Import PropNotations.
  Import FolNotations.

  Definition empty_spec X: prop := ∀ x, (mem x X → ⊥)%prop.
  Definition pair_spec x y Z: prop := ∀ D, (D ≅ x ∨ D ≅ y) ↔ mem D Z.
  Definition unionall_spec R S: prop := ∀ z, (∃ w, mem w R ∧ mem z w) ↔ mem z S.

  Definition empty: set := ι X, empty_spec X.
  Definition pair x y: set := ι Z, pair_spec x y Z.
  Definition unionall A: set := ι S, unionall_spec A S.

  Definition union A B: set := unionall (pair A B).
  Definition sing X: set := pair X X.
  Definition suc X: set := union X (sing X).

  Module IzfNotations.
    Notation "x ∈ X" := (mem (x%term) (X%term)) : prop.
    Notation "x ∉ X" := (impl (mem (x%term) (X%term)) false) : prop.

    Notation "∅" := empty : term.
    Notation "⋃ A" := (unionall (A%term)) : term.
    Notation "A ∪ B" := (union (A%term) (B%term)) (at level 30) : term.
  End IzfNotations.
End IzfNotations.

(* Start on formalizing a fragment of intuitionistic ZF *)
Module Type IZF.
  Include IzfSymbols.
  Include PropNotations.
  Import FolNotations.

  Include IzfNotations.
  Import IzfNotations.

  (* See
     https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html

     for reference axioms
   *)
  (* Axiom 1, Extensionality *)
  Axiom ext: ∀ R S, (∀ x y, x ∈ R ↔ y ∈ S) ⊢ R ≅ S.
  (* Axiom 2: Pairs *)
  Axiom pair_exists: ∀ x y, ⊤ ⊢ ∃ z, pair_spec x y z.
  (* Axiom 3: Unions exist *)
  Axiom unionall_exists: ∀ R, ⊤ ⊢ ∃ S, unionall_spec R S.
  (* Axiom 4: Empty set exists *)
  Axiom empty_exists: ⊤ ⊢ ∃ x, empty_spec x.
  (* Axiom 5: An infinity set exists *)
  Axiom infinity_exists: ⊤ ⊢ ∃ x, ∅ ∈ x ∧ ∀ y, y ∈ x → suc y ∈ x.
  (* Axiom 6: Separation Schema *)
  Axiom separation: ∀ P, ⊤ ⊢ ∀ a, ∃ x, ∀ y, y ∈ x ↔ y ∈ a ∧ P y.
  (* Axiom 7: Collection Schema *)
  Axiom collection: ∀ P, ⊤ ⊢ ∀ a, (∀ x, x ∈ a → (∃ y, P x y)) → ∃ b, ∀ x, x ∈ a → ∃ y, y ∈ b ∧ P x y.
  (* Axiom 8: Powerset *)
  Axiom powerset: ⊤ ⊢ ∀ x, ∃ y, ∀ z, z ∈ y ↔ ∀ w, w ∈ z → w ∈ x.
  (* Axiom 9: Induction *)
  Axiom ind: ∀ P, ⊤ ⊢ ∀ a, (∀ y, y ∈ a → P y → P a) → ∀ a, P a.
End IZF.

Module PropFacts (Import P: PropositionalLogic).
  Import PropNotations.

  Include EntailNotations(P).
  Import EntailNotations.

  Open Scope entail.

  #[export]
  Instance equiv_entail: subrelation equiv entail.
  Proof.
    intros ? ? [p q].
    auto.
  Qed.

  #[export]
  Instance and_Proper: Proper (entail ==> entail ==> entail) and.
  Proof.
    intros ? ? f ? ? g.
    xsplit.
    - xfirst.
      auto.
    - xsecond.
      auto.
  Defined.

  #[export]
  Instance or_Proper : Proper (entail ==> entail ==> entail) or.
  Proof.
    intros ? ? f ? ? g.
    xcase.
    - xleft.
      auto.
    - xright.
      auto.
  Defined.

  #[export]
  Instance impl_Proper : Proper (entail --> entail ==> entail) impl.
  Proof.
    unfold Basics.flip.
    intros ? ? f ? ? g.
    xcurry.
    rewrite <- g.
    rewrite f.
    exact eval.
  Defined.

  Lemma and_commute {P Q}: P ∧ Q ⊢ Q ∧ P.
  Proof.
    xsplit.
    - xsecond.
      reflexivity.
    - xfirst.
      reflexivity.
  Qed.

  Lemma or_commute {P Q}: P ∨ Q ⊢ Q ∨ P.
  Proof.
    xcase.
    - xright.
      reflexivity.
    - xleft.
      reflexivity.
  Qed.

  Lemma distribute {P Q R}: R ∧ (P ∨ Q) ⊢ (R ∧ P) ∨ (R ∧ Q).
  Proof.
    xuncurry.
    xcase.
    - xcurry.
      xleft.
      reflexivity.
    - xcurry.
      xright.
      reflexivity.
  Qed.

  Lemma undistribute {P Q R}: (R ∧ P) ∨ (R ∧ Q) ⊢ R ∧ (P ∨ Q).
  Proof.
    xcase.
    - rewrite <- i1.
      reflexivity.
    - rewrite <- i2.
      reflexivity.
  Qed.

  Lemma app {P Q R}: P ⊢ (Q → R) → P ⊢ Q → P ⊢ R .
  Proof.
    intros f g.
    exact (eval ∘ ⟨g , f⟩).
  Defined.
End PropFacts.

Module FolFacts (Import P: FirstOrderLogic).
  Include PropFacts(P).

  Import PropNotations.
  Import EntailNotations.
  Import FolNotations.

  Include FolEntailNotations(P).
  Import FolEntailNotations.

  Open Scope entail.

  #[export]
  Instance colim_Proper `{sort} : Proper (pointwise_relation _ entail ==> entail) colim.
  Proof.
    intros ? ? f.
    xelim z.
    xcointro.
    apply f.
  Defined.

  #[export]
  Instance lim_Proper `{sort} : Proper (pointwise_relation _ entail ==> entail) lim.
  Proof.
    intros ? ? f.
    xintro z.
    xapp.
    apply f.
  Defined.

  #[export]
  Instance unique_Proper `{sort} : Proper (pointwise_relation _ entail --> entail) unique.
  Proof.
    intros ? ? f.
    xintro x.
    xintro y.
    xapp.
    xapp.
    rewrite (f x), (f y).
    xcurry.
    rewrite eval.
    xcurry.
    rewrite eval.
    reflexivity.
  Qed.

  #[export]
  Instance exists_unique_Proper `{sort} : Proper (pointwise_relation _ equiv ==> entail) exists_unique.
  Proof.
    intros ? ? f.
    unfold exists_unique.
    xsplit.
    - rewrite π1.
      xelim z.
      xcointro.
      rewrite f.
      reflexivity.
    - rewrite π2.
      xintro x.
      xintro y.
      xapp.
      xapp.
      destruct (f x) as [? fx].
      destruct (f y) as [? fy].
      rewrite fx, fy.
      xcurry.
      rewrite eval.
      xcurry.
      rewrite eval.
      reflexivity.
  Qed.

  Lemma colim_commute  `{sort} {P}: (∃ x y, P x y) ⊢ ∃ y x, P x y.
  Proof.
    xelim x.
    xelim y.
    xcointro.
    xcointro.
    reflexivity.
  Qed.

  Lemma lim_commute `{sort} {P}: (∀ x y, P x y) ⊢ ∀ y x, P x y.
  Proof.
    xintro x.
    xintro y.
    xapp.
    xapp.
    reflexivity.
  Qed.

  Lemma colim_distribute `{sort} {P R}: R ∧ (∃ x, P x) ⊢ ∃ x, R ∧ P x.
  Proof.
    xuncurry.
    xelim x.
    xcurry.
    xcointro.
    reflexivity.
  Qed.

  Lemma unique_distribute `{sort} {P R}: R ∧ (! x, P x) ⊢ ! x, R ∧ P x.
  Proof.
    xintro x.
    xintro y.
    xcurry.
    xcurry.
    rewrite ⟨π1 ∘ π1, ⟨π2 ∘ π1, ⟨π2 ∘ π1 ∘ π2, π2 ∘ π2 ∘ π2⟩⟩⟩.
    xuncurry.
    xuncurry.
    xuncurry.
    unfold unique.
    xapp.
    xapp.
    xcurry.
    rewrite eval.
    xcurry.
    rewrite eval.
    xcurry.
    rewrite π2.
    reflexivity.
  Qed.

  Lemma exists_unique_distribute `{sort} {P R}: R ∧ (∃! x, P x) ⊢ ∃! x, R ∧ P x.
  Proof.
    unfold exists_unique.
    xsplit.
    - rewrite ⟨π1, π1 ∘ π2⟩.
      apply colim_distribute.
    - rewrite ⟨π1, π2 ∘ π2⟩.
      apply unique_distribute.
  Qed.

  Lemma leib_intro  `{sort}P {x y}:
    (∀ Q, Q x ∧ P ⊢ Q y) →
    P ⊢ x ≅ y.
  Proof.
    intro f.
    rewrite ⟨tt _, id _⟩.
    rewrite refl.
    apply f.
  Qed.

  Lemma invleib_intro  `{sort} P {x y}:
    (∀ Q, Q y ∧ P ⊢ Q x) →
    P ⊢ x ≅ y.
  Proof.
    intro f.
    rewrite ⟨tt _, id _⟩.
    rewrite refl.
    apply (f (λ x, (x ≅ y)%prop)).
  Qed.

  Lemma trans  `{sort} {x y z}: x ≅ y ∧ y ≅ z ⊢ x ≅ z.
  Proof.
    rewrite (subst (λ y, (x ≅ y)%prop)).
    reflexivity.
  Qed.

  Lemma sym  `{sort} {x y}: x ≅ y ⊢ y ≅ x.
  Proof.
    apply invleib_intro.
    intro.
    apply subst.
  Qed.

  Lemma invsubst `{sort} P {x y}: P y ∧ x ≅ y ⊢ P x.
  Proof.
    rewrite sym.
    rewrite subst.
    reflexivity.
  Qed.


  (* FIXME must be "respectful" functors? *)
  Definition leib `{sort} e e':= (∀ P: term → prop, (P e ⊢ P e')).

  #[export]
   Instance leib_Reflexive `{sort}: Reflexive leib.
  Proof.
    intros ? ?.
    reflexivity.
  Qed.

  #[export]
  Instance leib_Transitive `{sort}: Transitive leib.
  Proof.
    unfold leib.
    intros ? ? ? p q ?.
    rewrite p, q.
    reflexivity.
  Qed.

  #[export]
  Instance leib_Symmetric `{sort}: Symmetric leib.
  Proof.
    unfold leib.
    intros ? ? p ?.
    erewrite ⟨id _, invleib_intro _ _ ∘ tt _⟩.
    apply subst.
    Unshelve.
    intro.
    rewrite π1.
    apply p.
  Qed.

  #[export]
   Instance leib_Equivalence `{sort}: Equivalence leib := {
      Equivalence_Reflexive := _ ;
   }.

  #[export]
   Instance term_Setoid `{sort}: Setoid term := {
      equiv := leib ;
    }.


  #[export]
  Instance cong_Proper `{sort}: Proper (leib ==> leib ==> entail) cong.
  Proof.
    unfold leib.
    intros ? ? p ? ? q.
    assert (p': ⊤ ⊢ x ≅ y).
    1: {
      apply leib_intro.
      intro.
      rewrite π1.
      apply p.
    }
    assert (q': ⊤ ⊢ x0 ≅ y0).
    1: {
      apply leib_intro.
      intro.
      rewrite π1.
      apply q.
    }
    rewrite ⟨id _, q' ∘ tt _⟩.
    rewrite trans.
    rewrite ⟨id _, p' ∘ tt _⟩.
    rewrite sym.
    rewrite trans.
    apply sym.
  Qed.

End FolFacts.

Module IzfFacts (Import P: IZF).
  Include FolFacts(P).

  Import PropNotations.
  Import EntailNotations.
  Import FolNotations.
  Import IzfNotations.

  Include FolEntailNotations.
  Import FolEntailNotations.

  Lemma empty_unique: ⊤ ⊢ ! X, empty_spec X.
  Proof.
    Open Scope entail.
    xintro x.
    xintro y.
    xcurry.
    xfirst.
    xcurry.
    unfold empty_spec.
    rewrite <- ext.
    xintro z.
    xintro w.
    xsplit.
    - xcurry.
      xabsurd.
      rewrite ⟨π1, π2 ∘ π2⟩.
      xuncurry.
      xapp.
      reflexivity.
    - xcurry.
      xabsurd.
      rewrite ⟨π1, π1 ∘ π2⟩.
      xuncurry.
      xapp.
      reflexivity.
  Defined.

  Definition empty_exists_unique: ⊤ ⊢ ∃! X, empty_spec X :=
    ⟨empty_exists, empty_unique⟩.

  Lemma empty_is_empty: ⊤ ⊢ empty_spec ∅.
  Proof.
    unfold empty.
    cbn.
    assert (d := describe empty_spec).
    destruct d as [d ?].
    rewrite <- d.
    apply empty_exists_unique.
  Qed.

  Lemma empty_absurd x: x ∈ ∅ ⊢ ⊥.
  Proof.
    eassert (f := empty_is_empty).
    unfold empty_spec in f.
    rewrite (lim_elim _ x) in f.
    rewrite <- (uncurry f).
    xsplit.
    1: reflexivity.
    xtaut.
    reflexivity.
  Qed.

  Lemma pair_unique x y: ⊤ ⊢ ! Z, pair_spec x y Z.
  Proof.
  Admitted.

  Definition pair_exists_unique A B: ⊤ ⊢ ∃! X, pair_spec A B X :=
    ⟨pair_exists A B, pair_unique A B⟩.

  Lemma pair_is_pair A B: ⊤ ⊢ pair_spec A B (pair A B).
  Proof.
    unfold pair.
    cbn.
    assert (d := describe (pair_spec A B)).
    destruct d as [d ?].
    rewrite <- (pair_exists_unique A B) in d.
    apply d.
  Defined.

  Lemma unionall_unique R: ⊤ ⊢ ! X, unionall_spec R X.
  Proof.
    xintro x.
    xintro y.
    xcurry.
    xcurry.
    rewrite ⟨π1, π1 ∘ π2⟩.
    rewrite <- ext.
    xintro z.
    xintro w.
    unfold unionall_spec.
    xsplit.
    - xcurry.
      xyo r f.
      xdestruct f l u.
      xdestruct u v s.
      rewrite (lim_elim _ z) in s.
      rewrite π2 in s.
      rewrite <- l in s.
      assert (s' := uncurry s).
      rewrite <- ⟨id _, id _⟩ in s'.
      rewrite ⟨id _, s'⟩.
      rewrite colim_distribute.
      xelim z'.
      rewrite (lim_elim _ w) in v.
      rewrite π1 in v.
      rewrite <- (uncurry v).
      xsplit.
      2: xfirst;reflexivity.
      xsecond.
      xcointro.
      xsplit.
      1: xfirst;reflexivity.
  Admitted.

  Definition unionall_exists_unique R: ⊤ ⊢ ∃! X, unionall_spec R X :=
    ⟨unionall_exists R, unionall_unique R⟩.

  Lemma unionall_is_unionall R: ⊤ ⊢ unionall_spec R (⋃ R).
  Proof.
    unfold unionall.
    cbn.
    assert (d := describe (unionall_spec R)).
    destruct d as [d ?].
    rewrite <- (unionall_exists_unique R) in d.
    apply d.
  Defined.

  Lemma unionall_empty: ⊤ ⊢ ⋃ ∅ ≅ ∅.
  Proof.
    rewrite <- ext.
    xintro x.
    xintro y.
    xsplit.
    - xcurry.
      xabsurd.
      rewrite (unionall_is_unionall ∅).
      unfold unionall_spec.
      rewrite (lim_elim _ x).
      xuncurry.
      rewrite π2.
      xcurry.
      rewrite eval.
      xelim z.
      xfirst.
      rewrite empty_absurd.
      reflexivity.
    - xcurry.
      xfirst.
      rewrite (app (lim_app empty_is_empty y ∘ tt _) (id _)).
      xabsurd.
      reflexivity.
  Qed.

  Lemma pass {P Q}: ⊤ ⊢ P → (P → Q) ⊢ Q.
  Proof.
    intro f.
    rewrite <- f.
    rewrite ⟨tt _, id _⟩.
    apply eval.
  Qed.

  Lemma in_sing X: ⊤ ⊢ X ∈ sing X.
  Proof.
    unfold sing.
    rewrite (pair_is_pair X X).
    unfold pair_spec.
    rewrite (lim_elim _ X).
    rewrite π1.
    apply pass.
    xleft.
    apply refl.
  Qed.
End IzfFacts.

Module DCatFacts (Import P: DCat).
  Include FolFacts (P).

  Import PropNotations.
  Import EntailNotations.
  Import FolNotations.
  Import DCatNotations.

  Import FolEntailNotations.

  Lemma vcomp_vcomps f g: (N g ≅ S f)%prop == vcomps f g (f - g).
  Proof.
    unfold vcomp.
    split.
    - assert (d := describe (vcomps f g)).
      destruct d as [d ?].
      rewrite <- d.
      assert (v := vcomp_exists_unique).
      rewrite lim_elim in v.
      rewrite lim_elim in v.
      rewrite π1 in v.
      assert (v' := uncurry v).
      rewrite <- ⟨id _, tt _⟩ in v'.
      rewrite v'.
      reflexivity.
    - assert (d := describe (vcomps f g)).
      destruct d as [? d].
      rewrite d.
      assert (v := vcomp_exists_unique).
      rewrite lim_elim in v.
      rewrite lim_elim in v.
      rewrite π2 in v.
      assert (v' := uncurry v).
      rewrite <- ⟨id _, tt _⟩ in v'.
      rewrite v'.
      reflexivity.
  Qed.

  Lemma hcomp_hcomps f g: (W g ≅ E f)%prop == hcomps f g (f || g).
  Proof.
    unfold hcomp.
    split.
    - assert (d := describe (hcomps f g)).
      destruct d as [d ?].
      rewrite <- d.
      assert (v := hcomp_exists_unique).
      rewrite lim_elim in v.
      rewrite lim_elim in v.
      rewrite π1 in v.
      assert (v' := uncurry v).
      rewrite <- ⟨id _, tt _⟩ in v'.
      rewrite v'.
      reflexivity.
    - assert (d := describe (hcomps f g)).
      destruct d as [? d].
      rewrite d.
      assert (v := hcomp_exists_unique).
      rewrite lim_elim in v.
      rewrite lim_elim in v.
      rewrite π2 in v.
      assert (v' := uncurry v).
      rewrite <- ⟨id _, tt _⟩ in v'.
      rewrite v'.
      reflexivity.
  Qed.

End DCatFacts.

Module SpanFacts (Import P: Span).
  Import PropNotations.
  Import EntailNotations.
  Import FolNotations.
  Import DCatNotations.

  Include DCatFacts (P).

  Definition unit: cell := ι c, obj c ∧ ∀ A, obj A → ∃! b, hmor b ∧ W b ≅ A ∧ E b ≅ c.
  Definition bang A: cell := ι b, hmor b ∧ W b ≅ A ∧ E b ≅ unit.

  Lemma unit_is_obj: ⊤ ⊢ obj unit.
  Proof.
    assert (d := describe (λ c, (obj c ∧ ∀ A, obj A → ∃! b, hmor b ∧ W b ≅ A ∧ E b ≅ c)%prop)).
    destruct d as [d d'].
    clear d'.
    rewrite π1 in d.
    rewrite <- d.
    clear d.
    assert (u := unit_exists_unique).
    rewrite u.
    reflexivity.
  Qed.

  Lemma unit_has_bang A: obj A ⊢ ∃! b, hmor b ∧ W b ≅ A ∧ E b ≅ unit.
  Proof.
    assert (d := describe (λ c, (obj c ∧ ∀ A, obj A → ∃! b, hmor b ∧ W b ≅ A ∧ E b ≅ c)%prop)).
    destruct d as [d d'].
    clear d'.
    rewrite π2 in d.
    assert (u := unit_exists_unique).
    rewrite <- u in d.
    rewrite lim_elim in d.
    rewrite <- (uncurry d).
    refine ⟨id _, tt _⟩.
  Qed.

  Lemma bang_hmor A: obj A ⊢ hmor (bang A).
  Proof.
    assert (d := describe (λ b, hmor b ∧ W b ≅ A ∧ E b ≅ unit)%prop).
    destruct d as [d d'].
    clear d'.
    rewrite π1 in d.
    rewrite <- d.
    rewrite unit_has_bang.
    reflexivity.
  Qed.

  Lemma bang_W A: obj A ⊢ W (bang A) ≅ A.
  Proof.
    assert (d := describe (λ b, hmor b ∧ W b ≅ A ∧ E b ≅ unit)%prop).
    destruct d as [d d'].
    clear d'.
    rewrite π2 in d.
    rewrite π1 in d.
    rewrite <- d.
    rewrite unit_has_bang.
    reflexivity.
  Qed.

  Lemma bang_E A: obj A ⊢ E (bang A) ≅ unit.
  Proof.
    assert (d := describe (λ b, hmor b ∧ W b ≅ A ∧ E b ≅ unit)%prop).
    destruct d as [d d'].
    clear d'.
    rewrite π2 in d.
    rewrite π2 in d.
    rewrite <- d.
    rewrite unit_has_bang.
    reflexivity.
  Qed.

  Lemma bang_f A f: ⊤ ⊢ f || bang A ≅ bang A.
  Proof.
  Admitted.
  (* a monad in span is a category *)
End SpanFacts.

Module PropModel <: PropositionalLogic.
  Definition prop := Prop.
  Definition entail (p q: prop) := p → q.

  #[export]
  Instance id: Reflexive entail.
  Proof.
    intro.
    unfold entail.
    auto.
  Qed.

  #[export]
  Instance compose: Transitive entail.
  Proof.
    intro.
    unfold entail.
    auto.
  Qed.

  Definition true := True.
  Definition false := False.

  Definition and := Logic.and.
  Definition or := Logic.or.
  Definition impl (P Q: prop): prop := P -> Q.

  Include PropNotations.
  Import PropNotations.

  Lemma tt P: P ⊢ ⊤.
  Proof.
    unfold entail, true.
    auto.
  Qed.

  Lemma absurd P: ⊥ ⊢ P.
  Proof.
    unfold entail, false.
    contradiction.
  Qed.

  Lemma fanout {P Q R}: P ⊢ Q → P ⊢ R → P ⊢ Q ∧ R.
  Proof.
    unfold entail, and.
    auto.
  Qed.

  Lemma π1 {P Q}: P ∧ Q ⊢ P.
  Proof.
    unfold entail, and.
    intros [].
    auto.
  Qed.

  Lemma π2 {P Q}: P ∧ Q ⊢ Q.
  Proof.
    unfold entail, and.
    intros [].
    auto.
  Qed.

  Lemma fanin {P Q R}: P ⊢ R → Q ⊢ R → P ∨ Q ⊢ R.
  Proof.
    unfold entail, or.
    intros ? ? [].
    all: auto.
  Qed.

  Lemma i1 {P Q}: P ⊢ (P ∨ Q).
  Proof.
    unfold entail, or.
    auto.
  Qed.

  Lemma i2 {P Q}: Q ⊢ (P ∨ Q).
  Proof.
    unfold entail, or.
    auto.
  Qed.

  Lemma Λ {P Q R}: Q ∧ P ⊢ R →
                   P ⊢ (Q → R).
  Proof.
    unfold entail, and, impl.
    auto.
  Qed.

  Lemma eval {P Q: prop}: (P ∧ (P → Q)) ⊢ Q.
  Proof.
    unfold entail, and, impl.
    intros [].
    auto.
  Qed.
End PropModel.

Module IzfModel <: IZF.
  Include PropModel.

  Import PropNotations.
  Include EntailNotations.

  Inductive SET := image {
                      s: Type ;
                      π: s → SET ;
                    }.
  Arguments image {s}.


  Definition emptyimpl := image (λ e: Empty_set, match e with end).

  Definition pairimpl (P Q: SET): SET := image (λ e: bool, if e then P else Q).

  Definition unionallimpl (P: SET): SET.
  Proof.
    refine (image (λ e: { e': s P & s (π P e') }, _)).
    exact (π (π P (projT1 e)) (projT2 e)).
  Defined.

 
  (* Really unsure how to handle definite description *)
  Definition definite' (P: SET → prop): SET.
  Proof.
  Admitted.

  Lemma describe' (P: SET → prop) : ((exists x, P x)%type ∧ (∀ x x0 : SET, (P x → P x0 → x = x0)%prop)%type)%prop == P (definite' P).
  Admitted.

  Include FolNotations.
  #[refine]
  #[export]
  Instance set: sort := {
      term := SET ;
      lim P := forall x, P x ;
      colim P := exists x, P x ;
      cong P Q := P = Q ;
      definite := definite' ;
    }.
  Proof.
    all: unfold entail, equiv.
    all: intros.
    all: eauto.
    - destruct H0.
      eauto.
    - destruct H.
      subst.
      auto.
    - apply describe'.
  Defined.

  Definition mem (X Y: set): Prop :=
    exists x, π Y x = X.

  Include IzfNotations.
  Import IzfNotations.

  Open Scope prop.

  Lemma ext R S: (∀ x y, x ∈ R ↔ y ∈ S) ⊢ R ≅ S.
  Proof.
    unfold entail, lim, impl, and, cong.
    intros f.
    cbn.
  Admitted.

  Lemma empty_exists: ⊤ ⊢ ∃ x, empty_spec x.
  Proof.
    unfold entail, colim, empty_spec, lim, impl, false.
    exists emptyimpl.
    intros ? [s].
    destruct s.
  Qed.

  Lemma pair_exists x y: ⊤ ⊢ ∃ z, pair_spec x y z.
  Proof.
    unfold entail, colim, pair_spec, lim, impl, and, or.
    intros ?.
    exists (pairimpl x y).
    intros.
    split.
    - admit.
    - intros [p].
      subst.
      destruct p.
      all: cbn.
      1: left.
      2: right.
      all: reflexivity.
  Admitted.

  Lemma unionall_exists R: ⊤ ⊢ ∃ S, unionall_spec R S.
  Proof.
    unfold entail, lim, colim, unionall_spec, exists_unique, unique, lim, impl, and, colim.
    intros.
    exists (unionallimpl R).
    intro.
    cbn.
    split.
    - intros [? [[] []]].
      auto.
      subst.
      eexists.
      Unshelve.
      2: {
        eexists.
        eauto.
      }
      cbn.
      reflexivity.
    - intros [?].
      subst.
      destruct x0.
      cbn.
      exists (π R x).
      cbn.
      split.
      + exists x.
        reflexivity.
      + exists s0.
        reflexivity.
  Qed.
  Axiom infinity_exists: ⊤ ⊢ ∃ x, ∅ ∈ x ∧ ∀ y, y ∈ x → suc y ∈ x.
  (* Axiom 6: Separation Schema *)
  Axiom separation: ∀ P, ⊤ ⊢ ∀ a, ∃ x, ∀ y, y ∈ x ↔ y ∈ a ∧ P y.
  (* Axiom 7: Collection Schema *)
  Axiom collection: ∀ P, ⊤ ⊢ ∀ a, (∀ x, x ∈ a → (∃ y, P x y)) → ∃ b, ∀ x, x ∈ a → ∃ y, y ∈ b ∧ P x y.
  (* Axiom 8: Powerset *)
  Axiom powerset: ⊤ ⊢ ∀ x, ∃ y, ∀ z, z ∈ y ↔ ∀ w, w ∈ z → w ∈ x.
  (* Axiom 9: Induction *)
  Axiom ind: ∀ P, ⊤ ⊢ ∀ a, (∀ y, y ∈ a → P y → P a) → ∀ a, P a.
End IzfModel.