Library Exercise_4_2_4_4


Require Import Utf8.
Require Import ProofIrrelevance.
Require Import Ensembles.
Require Import Common Notations Orders PropPreOrder PreOrderCategory Duals SetCategory EnsemblePreOrder.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.2.4.4

Problem

Take again the preorder J of jurisdictions from Exercise 4.2.4.3 and the idea that laws are propositions. But this time, let R(V) be the set of all possible laws (not just those dictated to hold) that are in actuality being respected, i.e. followed, by all people in V. This assigns to each jurisdiction a set. Since preorders can be considered categories, does our "the set of respected laws" function R : Ob J Ob Set extend to a functor J Set?
What about if instead we take the meet of all these laws and assign to each jurisdiction the maximal law respected throughout. Does this assignment Ob J Ob Prop extend to a functor J Prop?

  Variable Person : Type.
  Definition Jurisdiction := Ensemble Person.
  Variable Law : Type.
  Variable LawAsProp : LawProp.
  Definition SetOfLaws := Ensemble Law.
  Variable RespectedLawsOfPerson : PersonSetOfLaws.
  Inductive RespectedLawsOf (J : Jurisdiction) : SetOfLaws :=
  | RespectedLawsOfAll : law,
                         ( person,
                            person J
                            → law RespectedLawsOfPerson person)
                         → law RespectedLawsOf J.


  Global Instance JurisdictionPreOrder
  : @PreOrder Jurisdiction (fun U VU V).
  firstorder.
  Qed.

  Global Instance SetsPreOrder : @PreOrder SetOfLaws _
    := Ensemble_PreOrder _.

  Hint Extern 1 ⇒ constructor.
  Hint Extern 1 ⇒ destruct_head_hnf @RespectedLawsOf.
  Definition RespectedLawsOfFunctor_MorphismOf
             s d (m : Morphism (PreOrderCategory JurisdictionPreOrder) s d)
  : Morphism (OppositeCategory (PreOrderCategory SetsPreOrder))
             (RespectedLawsOf s)
             (RespectedLawsOf d).
    compute in *;
    repeat (split || intro);
    destruct_head_hnf @RespectedLawsOf.
    intuition.
  Qed.
  Definition RespectedLawsOfFunctor
  : Functor (PreOrderCategory JurisdictionPreOrder)
            (OppositeCategory (PreOrderCategory SetsPreOrder)).
    refine (Build_Functor (PreOrderCategory JurisdictionPreOrder)
                          (OppositeCategory (PreOrderCategory SetsPreOrder))
                          (RespectedLawsOf)
                          (RespectedLawsOfFunctor_MorphismOf)
                          _
                          _);
    abstract (intros; simpl; apply ProofIrrelevance.proof_irrelevance).
  Defined.

  Section maximal_law.
    Variable S : SetOfLaws.
    Let SetOfLawsAsProp : Ensemble Prop := fun P
                                              L,
                                               L S
                                                LawAsProp L = P.

    Definition maximal_law : Prop :=
      EnsembleMeetElement (EnsembleMeetOf := PropHasEnsembleMeets SetOfLawsAsProp).
  End maximal_law.
  Definition MaximalRespectedLawOfFunctor_MorphismOf
             s d (m : Morphism (PreOrderCategory JurisdictionPreOrder) s d)
  : Morphism (PreOrderCategory Prop_PreOrder)
             (maximal_law (RespectedLawsOf s))
             (maximal_law (RespectedLawsOf d)).
    repeat match goal with
             | _progress compute in ×
             | _split
             | _intro
             | _progress destruct_head_hnf @RespectedLawsOf
             | _progress destruct_head_hnf @ex
             | _progress intuition
             | [ H : _ |- _ ] ⇒ apply H; clear H
             | _eexists; split; try eassumption; []
             | _constructor
             | _solve [ firstorder ]
           end.
  Defined.
  Definition MaximalRespectedLawOfFunctor
  : Functor (PreOrderCategory JurisdictionPreOrder)
            (PreOrderCategory Prop_PreOrder).
    refine (Build_Functor (PreOrderCategory JurisdictionPreOrder)
                          (PreOrderCategory Prop_PreOrder)
                          (fun Jmaximal_law (RespectedLawsOf J))
                          MaximalRespectedLawOfFunctor_MorphismOf
                          _
                          _);
    abstract (intros; simpl; apply ProofIrrelevance.proof_irrelevance).
  Defined.
End Exercise_4_2_4_4.