ITree.Basics.CategoryRelations
From Coq Require Import
Morphisms.
From ITree Require Import
Basics.Basics
Basics.CategoryOps
Basics.CategoryTheory
Basics.CategoryFunctor
Basics.HeterogeneousRelations
Basics.Function
Basics.Tacs.
(* Structure of the Rel category. Mainly for fun and to understand its
structure for now, we are not using it at the moment. *)
Section Operations.
Import RelNotations.
Local Open Scope relationH_scope.
(* Objects: Type
Arrows : relationH ≜ ∀ A B, A → B → Prop
*)
(* Equivalence of morphisms is extensional equivalence *)
Global Instance Eq2_rel : Eq2 relationH := @eq_rel.
(* Importantly, note that composition of relations R >>> S posits
the existence of an intermediate witness at the intermediate type
(R >>> S) x z ↔ ∃ y, R x y ∧ S y z
*)
Global Instance Cat_rel : Cat relationH := fun _ _ _ f g ⇒ rel_compose g f.
(* Identities are defined by the eq relations *)
Global Instance Id_rel : Id_ relationH := @eq.
(* As usual, void is the initial element *)
Global Instance Initial_rel : Initial relationH void :=
fun _ v ⇒ match v : void with end.
(* sum with its injection functions seen as relations form the coproduct *)
Global Instance Case_rel : Case relationH sum :=
fun _ _ _ l r ⇒ case_sum _ _ _ l r.
Global Instance Inl_rel : Inl relationH sum :=
fun A B ⇒ fun_rel inl.
Global Instance Inr_rel : Inr relationH sum :=
fun _ _ ⇒ fun_rel inr.
(* Interestingly, it is also sum and not prod that forms the product *)
Global Instance Pair_rel : Pair relationH sum :=
fun A B C l r c ⇒ case_sum _ _ _ (l c) (r c).
Global Instance Fst_rel : Fst relationH sum :=
fun _ _ x a ⇒ x = inl a.
Global Instance Snd_rel : Snd relationH sum :=
fun _ _ x a ⇒ x = inr a.
(* My first intuition for the product was indeed to use prod as follows.
However this fails to satisfy the necessary equations: if you think of
pair f g >>> fst ≈ f
This cannot hold since if g is the empty relation, then so is pair f g
*)
(* Global Instance Pair_rel : Pair relationH prod := *)
(* fun _ _ _ l r c '(a,b) => l c a /\ r c b. *)
(* Global Instance Fst_rel : Fst relationH prod := *)
(* fun A B => fun_rel fst. *)
(* Global Instance Snd_rel : Snd relationH prod := *)
(* fun _ _ => fun_rel snd. *)
(* Both ⊕ and ⊗ are bimaps with respect to with relationH forms a monoidal category.
I am not sure if they are isomorphic to the bimaps derived from the product and coproduct?
*)
Global Instance Bimap_sum_rel : Bimap relationH sum :=
fun (a b c d : Type) R S ⇒ R ⊕ S.
Global Instance AssocR_sum : AssocR relationH sum :=
fun A B C ab_c a_bc ⇒
match ab_c, a_bc with
| inl (inl a), inl a' ⇒ a = a'
| inl (inr b), inr (inl b') ⇒ b = b'
| inr c, inr (inr c') ⇒ c = c'
| _, _ ⇒ False
end.
Global Instance AssocL_sum : AssocL relationH sum :=
fun A B C ab_c a_bc ⇒
match ab_c, a_bc with
| inl a, inl (inl a') ⇒ a = a'
| inr (inl b), inl (inr b') ⇒ b = b'
| inr (inr c), inr c' ⇒ c = c'
| _, _ ⇒ False
end.
Global Instance UnitL_sum : UnitL relationH sum void :=
fun _ ma a' ⇒ match ma with
| inl abs ⇒ match abs with end
| inr a ⇒ a = a'
end.
Global Instance UnitR_sum : UnitR relationH sum void :=
fun _ ma a' ⇒ match ma with
| inr abs ⇒ match abs with end
| inl a ⇒ a = a'
end.
Global Instance UnitL'_sum : UnitL' relationH sum void :=
fun _ a ma' ⇒ match ma' with
| inl abs ⇒ match abs with end
| inr a' ⇒ a = a'
end.
Global Instance UnitR'_sum : UnitR' relationH sum void :=
fun _ a ma' ⇒ match ma' with
| inr abs ⇒ match abs with end
| inl a' ⇒ a = a'
end.
Global Instance Bimap_prod_rel : Bimap relationH prod :=
fun (a b c d : Type) R S ⇒ R ⊗ S.
Global Instance AssocR_prod : AssocR relationH prod :=
fun A B C '(a,b,c) '(a',(b',c')) ⇒ a = a' ∧ b = b' ∧ c = c'.
Global Instance AssocL_prod : AssocL relationH prod :=
fun A B C '(a,(b,c)) '(a',b',c') ⇒ a = a' ∧ b = b' ∧ c = c'.
Global Instance UnitL_prod : UnitL relationH prod unit :=
fun _ '(_,a) a' ⇒ a = a'.
Global Instance UnitR_prod : UnitR relationH prod unit :=
fun _ '(a,_) a' ⇒ a = a'.
Global Instance UnitL'_prod : UnitL' relationH prod unit :=
fun _ a '(_,a') ⇒ a = a'.
Global Instance UnitR'_prod : UnitR' relationH prod unit :=
fun _ a '(a',_) ⇒ a = a'.
(* The transpose operation forms a dagger category *)
Global Instance Dagger_rel : Dagger relationH :=
fun a b R ⇒ transpose R.
End Operations.
Morphisms.
From ITree Require Import
Basics.Basics
Basics.CategoryOps
Basics.CategoryTheory
Basics.CategoryFunctor
Basics.HeterogeneousRelations
Basics.Function
Basics.Tacs.
(* Structure of the Rel category. Mainly for fun and to understand its
structure for now, we are not using it at the moment. *)
Section Operations.
Import RelNotations.
Local Open Scope relationH_scope.
(* Objects: Type
Arrows : relationH ≜ ∀ A B, A → B → Prop
*)
(* Equivalence of morphisms is extensional equivalence *)
Global Instance Eq2_rel : Eq2 relationH := @eq_rel.
(* Importantly, note that composition of relations R >>> S posits
the existence of an intermediate witness at the intermediate type
(R >>> S) x z ↔ ∃ y, R x y ∧ S y z
*)
Global Instance Cat_rel : Cat relationH := fun _ _ _ f g ⇒ rel_compose g f.
(* Identities are defined by the eq relations *)
Global Instance Id_rel : Id_ relationH := @eq.
(* As usual, void is the initial element *)
Global Instance Initial_rel : Initial relationH void :=
fun _ v ⇒ match v : void with end.
(* sum with its injection functions seen as relations form the coproduct *)
Global Instance Case_rel : Case relationH sum :=
fun _ _ _ l r ⇒ case_sum _ _ _ l r.
Global Instance Inl_rel : Inl relationH sum :=
fun A B ⇒ fun_rel inl.
Global Instance Inr_rel : Inr relationH sum :=
fun _ _ ⇒ fun_rel inr.
(* Interestingly, it is also sum and not prod that forms the product *)
Global Instance Pair_rel : Pair relationH sum :=
fun A B C l r c ⇒ case_sum _ _ _ (l c) (r c).
Global Instance Fst_rel : Fst relationH sum :=
fun _ _ x a ⇒ x = inl a.
Global Instance Snd_rel : Snd relationH sum :=
fun _ _ x a ⇒ x = inr a.
(* My first intuition for the product was indeed to use prod as follows.
However this fails to satisfy the necessary equations: if you think of
pair f g >>> fst ≈ f
This cannot hold since if g is the empty relation, then so is pair f g
*)
(* Global Instance Pair_rel : Pair relationH prod := *)
(* fun _ _ _ l r c '(a,b) => l c a /\ r c b. *)
(* Global Instance Fst_rel : Fst relationH prod := *)
(* fun A B => fun_rel fst. *)
(* Global Instance Snd_rel : Snd relationH prod := *)
(* fun _ _ => fun_rel snd. *)
(* Both ⊕ and ⊗ are bimaps with respect to with relationH forms a monoidal category.
I am not sure if they are isomorphic to the bimaps derived from the product and coproduct?
*)
Global Instance Bimap_sum_rel : Bimap relationH sum :=
fun (a b c d : Type) R S ⇒ R ⊕ S.
Global Instance AssocR_sum : AssocR relationH sum :=
fun A B C ab_c a_bc ⇒
match ab_c, a_bc with
| inl (inl a), inl a' ⇒ a = a'
| inl (inr b), inr (inl b') ⇒ b = b'
| inr c, inr (inr c') ⇒ c = c'
| _, _ ⇒ False
end.
Global Instance AssocL_sum : AssocL relationH sum :=
fun A B C ab_c a_bc ⇒
match ab_c, a_bc with
| inl a, inl (inl a') ⇒ a = a'
| inr (inl b), inl (inr b') ⇒ b = b'
| inr (inr c), inr c' ⇒ c = c'
| _, _ ⇒ False
end.
Global Instance UnitL_sum : UnitL relationH sum void :=
fun _ ma a' ⇒ match ma with
| inl abs ⇒ match abs with end
| inr a ⇒ a = a'
end.
Global Instance UnitR_sum : UnitR relationH sum void :=
fun _ ma a' ⇒ match ma with
| inr abs ⇒ match abs with end
| inl a ⇒ a = a'
end.
Global Instance UnitL'_sum : UnitL' relationH sum void :=
fun _ a ma' ⇒ match ma' with
| inl abs ⇒ match abs with end
| inr a' ⇒ a = a'
end.
Global Instance UnitR'_sum : UnitR' relationH sum void :=
fun _ a ma' ⇒ match ma' with
| inr abs ⇒ match abs with end
| inl a' ⇒ a = a'
end.
Global Instance Bimap_prod_rel : Bimap relationH prod :=
fun (a b c d : Type) R S ⇒ R ⊗ S.
Global Instance AssocR_prod : AssocR relationH prod :=
fun A B C '(a,b,c) '(a',(b',c')) ⇒ a = a' ∧ b = b' ∧ c = c'.
Global Instance AssocL_prod : AssocL relationH prod :=
fun A B C '(a,(b,c)) '(a',b',c') ⇒ a = a' ∧ b = b' ∧ c = c'.
Global Instance UnitL_prod : UnitL relationH prod unit :=
fun _ '(_,a) a' ⇒ a = a'.
Global Instance UnitR_prod : UnitR relationH prod unit :=
fun _ '(a,_) a' ⇒ a = a'.
Global Instance UnitL'_prod : UnitL' relationH prod unit :=
fun _ a '(_,a') ⇒ a = a'.
Global Instance UnitR'_prod : UnitR' relationH prod unit :=
fun _ a '(a',_) ⇒ a = a'.
(* The transpose operation forms a dagger category *)
Global Instance Dagger_rel : Dagger relationH :=
fun a b R ⇒ transpose R.
End Operations.
The following instances prove that the operations claimed above to be what
they are are indeed what the are
Section Facts.
Section CategoryRel.
Global Instance CatIdL_rel: CatIdL relationH.
Proof.
constructor; unfold subrelationH, cat, id_, Cat_rel, Id_rel, rel_compose; intros.
- edestruct H as (B' & EQ & R). rewrite <- EQ in R.
assumption.
- ∃ x. split. reflexivity. assumption.
Qed.
Global Instance CatIdR_rel: CatIdR relationH.
Proof.
constructor; unfold subrelationH, cat, id_, Cat_rel, Id_rel, rel_compose; intros.
- edestruct H as (B' & R & EQ). rewrite EQ in R.
assumption.
- ∃ y. split. assumption. reflexivity.
Qed.
Global Instance CatAssoc_rel: CatAssoc relationH.
Proof.
constructor; unfold subrelationH, cat, id_, Cat_rel, Id_rel, rel_compose;
intros A D H.
- edestruct H as (C & (B & Rf & Rg) & Rh); clear H.
∃ B. split; [assumption | ].
∃ C. split; assumption.
- edestruct H as (B & Rf & (C & Rg & Rh)); clear H.
∃ C. split; [ | assumption].
∃ B; split; assumption.
Qed.
Global Instance ProperCat_rel: ∀ a b c,
@Proper (relationH a b → relationH b c → relationH a c)
(eq2 ==> eq2 ==> eq2) cat.
Proof.
intros a b c.
constructor; unfold subrelationH, cat, id_, Cat_rel, Id_rel, rel_compose;
intros A C He.
- edestruct He as (B & Hx & Hx0).
unfold eq2, Eq2_rel, eq_rel, subrelationH in ×.
destruct H, H0.
∃ B. split. specialize (H A B Hx). assumption.
specialize (H0 _ _ Hx0). assumption.
- edestruct He as (B & Hy & Hy0).
unfold eq2, Eq2_rel, eq_rel, subrelationH in ×.
destruct H, H0.
∃ B. split. specialize (H1 _ _ Hy). assumption.
specialize (H2 _ _ Hy0). assumption.
Qed.
Global Instance Category_rel : Category relationH.
Proof.
constructor; typeclasses eauto.
Qed.
End CategoryRel.
Global Instance InitialObject_rel : InitialObject relationH void.
Proof.
split; intros [].
Qed.
Section CoproductRel.
Global Instance CaseInl_rel : CaseInl relationH sum.
Proof.
split.
intros ? ? [[] [H1 H2]]; inversion H1; subst; apply H2.
intros x ? ?.
∃ (inl x); split; auto; reflexivity.
Qed.
Global Instance CaseInr_rel : CaseInr relationH sum.
Proof.
split.
intros ? ? [[] [H1 H2]]; inversion H1; subst; apply H2.
intros x ? ?.
∃ (inr x); split; auto; reflexivity.
Qed.
Global Instance CaseUniversal_rel : CaseUniversal relationH sum.
Proof.
intros a b c R S T [TR RT] [TS ST].
split.
intros [] ? ?; cbn; [apply TR | apply TS]; eexists; split; eauto; reflexivity.
intros [] ? HR; [apply RT in HR | apply ST in HR];
destruct HR as [? [EQ ?]]; repeat red in EQ; subst; auto.
Qed.
Global Instance Proper_Case_rel : ∀ a b c : Type, Proper (eq2 ==> eq2 ==> eq2) (@case_ _ _ _ _ a b c).
Proof.
intros ? ? ? R S [RS SR] T U [TU UT]; split; intros [] ? ?; cbn in *;
[apply RS | apply TU | apply SR | apply UT]; auto.
Qed.
Global Instance Coproduct_rel : Coproduct relationH sum.
Proof.
constructor; typeclasses eauto.
Qed.
End CoproductRel.
Section ProductRel.
Global Instance PairFst_rel : PairFst relationH sum.
Proof.
split.
- intros ? ? ([] & ? & EQ); inversion EQ; subst; auto.
- intros ? ? ?.
∃ (inl y); cbv; auto.
Qed.
Global Instance PairSnd_rel : PairSnd relationH sum.
Proof.
split.
- intros ? ? ([] & ? & EQ); inversion EQ; subst; auto.
- intros ? ? ?.
∃ (inr y); cbv; auto.
Qed.
Global Instance PairUniversal_rel : PairUniversal relationH sum.
Proof.
intros ? ? ? R S RS [RSR RRS] [RSS SRS]; split.
- cbv. intros ? [] ?; [apply RSR | apply RSS];
(eexists; split; [| reflexivity]; auto).
- cbv. intros ? [] EQ; [apply RRS in EQ | apply SRS in EQ]; destruct EQ as [[] [? EQ]];
inversion EQ; subst; auto.
Qed.
Global Instance Proper_pair_rel : ∀ a b c : Type, Proper (eq2 ==> eq2 ==> eq2) (@pair_ _ _ _ _ a b c).
Proof.
intros ? ? ? R S [RS SR] T U [TU UT]; split.
cbv; intros ? [] ?; [apply RS | apply TU]; auto.
cbv; intros ? [] ?; [apply SR | apply UT]; auto.
Qed.
Global Instance Product_rel : Product relationH sum.
Proof.
constructor; typeclasses eauto.
Qed.
End ProductRel.
Section DaggerRel.
Global Instance DaggerInvolution_rel : DaggerInvolution relationH.
Proof.
split; intros ? ? H; apply H.
Qed.
Local Existing Instance Eq2_Op.
Local Existing Instance Id_Op.
Local Existing Instance Cat_Op.
Global Instance DaggerFunctor_rel : Functor (op relationH) relationH id (@dagger _ _ _).
Proof.
constructor.
- split; intros ? ? H; inversion H; subst; reflexivity.
- split; intros ? ? (? & ? & ?); eexists; eauto.
- intros a b x y [INCL1 INCL2].
split; intros ? ? H; [apply INCL1 | apply INCL2]; apply H.
Qed.
Global Instance DaggerLaws_rel : DaggerLaws relationH.
Proof.
constructor; typeclasses eauto.
Qed.
End DaggerRel.
Section BifunctorProd.
Global Instance BimapId_prod_rel : BimapId relationH prod.
Proof.
split.
- cbv; intros ? ? ?; subst; auto.
destruct x, y.
cbv; intros. destruct H; cbn in *; subst; auto.
- red. intros. destruct x, y. inversion H. subst. repeat red.
repeat red in H. intuition.
Qed.
Global Instance BimapCat_prod_rel : BimapCat relationH prod.
Proof.
split.
- cbv; intros [] [] ([] & H1 & H2).
inv H1; inv H2; eauto 6.
- cbv; intros [] [] H. destruct H as [(? & ? & ?) (? & ? & ?)].
cbn in *; eexists (_, _); eauto.
Qed.
Global Instance Bifunctor_prod_rel : Bifunctor relationH prod.
Proof.
constructor; try typeclasses eauto.
Qed.
Global Instance Iso_Assoc_prod_rel : ∀ a b c : Type, Iso relationH (@assoc_r _ relationH prod _ a b c) assoc_l.
Proof.
split.
- cbv; split.
+ intros ? ? ?; repeat destructn prod.
destructn ex; repeat destructn prod; repeat destructn and; subst; auto.
+ intros ((? & ?) & ?) ((x & y) & z) EQ; inv EQ.
∃ (x,(y,z)); intuition.
- cbv; split.
+ intros ? ? ?; destructn ex; repeat destructn prod; intuition subst; auto.
+ intros ? (x & y & z) ->; repeat destructn prod.
∃ (x,y,z); intuition.
Qed.
Global Instance Iso_UnitL_prod_rel: ∀ a : Type, Iso relationH (@unit_l _ relationH prod _ _ a) unit_l'.
Proof.
split; cbv; split; intros; repeat (subst || destructn ex || destructn prod || invn @eq || destructn unit); intuition subst; auto.
eexists; intuition.
∃ (tt,y); auto.
Qed.
Global Instance Iso_UnitR_prod_rel: ∀ a : Type, Iso relationH (@unit_r _ relationH prod _ _ a) unit_r'.
Proof.
split; cbv; split; intros; repeat (subst || destructn ex || destructn prod || invn @eq || destructn unit); intuition subst; auto.
eexists; intuition.
∃ (y,tt); auto.
Qed.
Global Instance UnitLNatural_prod_rel : UnitLNatural relationH prod unit.
Proof.
split;
cbv; intros; repeat (subst || destructn ex || destructn prod || invn @eq || destructn unit || destructn and
|| invn prod_rel).
- eexists; intuition subst; eauto.
- eexists (_, _); constructor; [ constructor; cbn; eauto | auto ].
Qed.
Global Instance UnitL'Natural_prod_rel : UnitL'Natural relationH prod unit.
Proof.
split;
cbv; intros; repeat (subst || destructn ex || destructn prod || destructn unit || destructn and
|| invn prod_rel).
eexists; intuition subst; eauto.
∃ (tt,x); intuition subst; auto.
Qed.
Global Instance AssocRUnit_prod_rel : AssocRUnit relationH prod unit.
Proof.
split; cbv; intros [[? ?] ?] [].
- intros [[? []] [? []]]. intuition. cbn in *; subst. constructor; cbn; auto.
- intros []; eexists (_, (u, _)). intuition.
Qed.
Ltac decomp :=
repeat lazymatch goal with
| [ H : ∃ _, _ |- _ ] ⇒ destruct H
| [ H : _ ∧ _ |- _ ] ⇒ destruct H
| [ H : _ × _ |- _ ] ⇒ destruct H
| [ H : prod_rel _ _ _ _ |- _ ] ⇒
let H1 := fresh H in let H2 := fresh H in
destruct H as [H1 H2]; cbn in H1, H2
| [ H : ?x = _ |- _ ] ⇒ subst x
| [ |- ∀ _, _ ] ⇒ intros
| [ |- prod_rel _ _ _ _ ] ⇒ constructor; cbn
| [ |- _ ∧ _ ] ⇒ constructor
end.
Global Instance AssocRAssocR_prod_rel : AssocRAssocR relationH prod.
Proof.
split; cbv; decomp.
- eexists (_, _, (_, _)). firstorder congruence.
- eexists (_, (_, _, _)); firstorder. eexists (_, (_, _), _). firstorder (cbn; congruence).
Qed.
Global Instance Monoidal_prod_rel : Monoidal relationH prod unit.
Proof.
constructor; typeclasses eauto.
Qed.
End BifunctorProd.
Section BifunctorSum.
Global Instance BimapId_sum_rel : BimapId relationH sum.
Proof.
split.
red. intros ? ? ?. repeat red in H.
destruct x, y; subst; inversion H; subst; repeat red; auto.
inversion H; inversion H2; subst; reflexivity.
inversion H; inversion H2; subst; reflexivity.
red. intros ? ? ?. repeat red in H.
subst. repeat red. destruct y; econstructor; reflexivity.
Qed.
Global Instance BimapCat_sum_rel : BimapCat relationH sum.
Proof.
split.
cbv. intros; destruct x, y; destruct H as (? & ? & ?); inversion H;
inversion H0; subst; inversion H5; subst; econstructor; eauto.
repeat intro. inversion H; inversion H0; inversion H3; repeat red; subst; eauto.
∃ (inl x0). split; econstructor; eauto.
∃ (inr x0). split; econstructor; eauto.
Qed.
Global Instance Bifunctor_sum_rel : Bifunctor relationH sum.
Proof.
constructor; try typeclasses eauto.
Qed.
Global Instance Iso_Assoc_sum_rel : ∀ a b c : Type, Iso relationH (@assoc_r _ relationH sum _ a b c) assoc_l.
Proof.
split.
- cbv; split;
intros;
repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit || destructn and
|| invn prod_rel); intuition.
∃ (inl a0); intuition.
∃ (inr (inl b0)); intuition.
∃ (inr (inr c0)); intuition.
- cbv; split; intros;
repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit || destructn and
|| invn prod_rel); intuition.
∃ (inl (inl a0)); intuition.
∃ (inl (inr b0)); intuition.
∃ (inr c0); intuition.
Qed.
Global Instance Iso_UnitL_sum_rel: ∀ a : Type, Iso relationH (@unit_l _ relationH sum _ _ a) unit_l'.
Proof.
split; cbv; split; intros; repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit); intuition subst; auto.
eexists; intuition.
∃ (inr y); auto.
Qed.
Global Instance Iso_UnitR_sum_rel: ∀ a : Type, Iso relationH (@unit_r _ relationH sum _ _ a) unit_r'.
Proof.
split; cbv; split; intros; repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit); intuition subst; auto.
eexists; intuition.
∃ (inl y); auto.
Qed.
Global Instance UnitLNatural_sum_rel : UnitLNatural relationH sum void.
Proof.
split;
cbv; intros; repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit || destructn and
|| invn sum_rel || invn void).
eexists; intuition subst; eauto.
eexists; intuition subst; eauto.
Qed.
Global Instance UnitL'Natural_sum_rel : UnitL'Natural relationH sum void.
Proof.
split;
cbv; intros; repeat (subst || destructn ex || destructn sum || invn @eq || destructn unit || destructn and
|| invn sum_rel || invn void).
eexists; intuition subst; eauto.
∃ (inr x); intuition subst; auto.
Qed.
Global Instance AssocRUnit_sum_rel : AssocRUnit relationH sum void.
Proof.
split; cbv; intros.
destruct H.
destruct x; try destruct s; try destruct x0; try inversion H; try inversion H1; subst; eauto;
try econstructor; try contradiction; eauto.
destruct s; try contradiction; subst; eauto.
inversion H; subst; eauto; try destruct a1; try contradiction; subst.
inv H. ∃ (inl a2); eauto.
inv H; ∃ (inr (inr b2)); eauto.
Qed.
Global Instance AssocRAssocR_sum_rel : AssocRAssocR relationH sum.
Proof.
split;
cbv; intros;
repeat (invn False || subst || destructn ex || destructn and || invn sum_rel
|| destructn sum || invn @eq || destructn unit).
- ∃ (inl (inl a2)); intuition; auto.
- eexists (inl (inr _)); intuition; auto.
- eexists (inr (inl _)); intuition; auto.
- eexists (inr (inr _)); intuition; auto.
- eexists (inl _); intuition; auto.
∃ (inl (inl a1)); intuition; auto.
- ∃ (inr (inl (inl b1))); intuition; econstructor; auto.
split. econstructor. Unshelve. 3 : exact ((inr (inl b1))). intuition; auto.
intuition.
- ∃ (inr (inl (inr c0))); intuition; econstructor; auto.
split. Unshelve. econstructor. Unshelve.
3 : refine ((inr (inr c0))). intuition; econstructor; auto.
intuition.
- ∃ (inr (inr d0)); intuition; econstructor; auto.
split. Unshelve. econstructor. reflexivity. cbn. auto.
Qed.
Global Instance Monoidal_sum_rel : Monoidal relationH sum void.
Proof.
constructor; typeclasses eauto.
Qed.
End BifunctorSum.
End Facts.