- intros; apply Build_Equivalence;
- [ unfold Reflexive; intros; reflexivity
- | unfold Symmetric; intros; symmetry; auto
- | unfold Transitive; intros; transitivity y; auto ].
- unfold Proper; unfold respectful; intros; simpl.
- apply ndr_comp_respects. reflexivity.
- apply al_subst_respects; auto.
- intros; simpl. apply al_subst_left_identity.
- intros; simpl.
- assert (@nd_llecnac _ Rule [] === @nd_rlecnac _ _ []).
- apply ndr_structural_indistinguishable; auto.
- setoid_rewrite H.
- apply al_subst_right_identity.
- intros; apply al_subst_associativity''.
- Defined.
- End Types1.
-
- (* Formalized Definition 4.10 *)
- Instance Judgments : Category (Tree ??Sequent) (fun h c => h /⋯⋯/ c) :=
- { id := fun h => nd_id _
- ; comp := fun a b c f g => f ;; g
- ; eqv := fun a b f g => f===g
- }.
- intros; apply Build_Equivalence;
- [ unfold Reflexive; intros; reflexivity
- | unfold Symmetric; intros; symmetry; auto
- | unfold Transitive; intros; transitivity y; auto ].
- unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
- intros; apply ndr_comp_left_identity.
- intros; apply ndr_comp_right_identity.
- intros; apply ndr_comp_associativity.
- Defined.
-
- (* a "primitive" proof has exactly one hypothesis and one conclusion *)
- Inductive IsPrimitive : forall (h_:Tree ??(@Sequent T)), Type :=
- isPrimitive : forall h, IsPrimitive [h].
- Hint Constructors IsPrimitive.
- Instance IsPrimitiveSubCategory : SubCategory Judgments IsPrimitive (fun _ _ _ _ _ => True).
- apply Build_SubCategory; intros; auto.
- Defined.
-
- (* The primitive judgments form a subcategory; nearly all of the
- * functors we build that go into Judgments will factor through the
- * inclusion functor for this subcategory. Explicitly constructing
- * it makes the formalization easier, but distracts from what's
- * actually going on (from an expository perspective) *)
- Definition PrimitiveJudgments := SubCategoriesAreCategories Judgments IsPrimitiveSubCategory.
- Definition PrimitiveInclusion := InclusionFunctor Judgments IsPrimitiveSubCategory.
-
- Section Types0.
- Inductive IsNil : Tree ??(@Sequent T) -> Prop := isnil : IsNil [].
- Inductive IsClosed : Tree ??(@Sequent T) -> Prop := isclosed:forall t, IsClosed [[]|=[t]].
- Inductive IsIdentity : forall h c, (h /⋯⋯/ c) -> Prop :=
- | isidentity0 : forall t, IsIdentity t t (nd_id t)
- | isidentity1 : forall t pf1 pf2, IsIdentity t t pf1 -> IsIdentity t t pf2 -> IsIdentity t t (pf1 ;; pf2).
- Inductive IsInTypes0 (h c:Tree ??Sequent)(pf:h /⋯⋯/ c) : Prop :=
- | iit0_id0 : IsNil h -> IsNil c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
- | iit0_id1 : @IsClosed h -> @IsClosed c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
- | iit0_term : IsNil h -> @IsClosed c -> IsInTypes0 _ _ pf.
- Instance Types0P : SubCategory Judgments
- (fun x:Judgments => IsInTypes0 _ _ (id(Category:=Judgments) x))
- (fun h c _ _ f => IsInTypes0 h c f).
- intros.
- apply Build_SubCategory; intros; simpl.
- auto.
- inversion H0.
- inversion H1; subst.
- inversion H2; subst.
- inversion H; subst. inversion H4; subst.
- apply iit0_id0; auto. apply isidentity1; auto.
- inversion H5.
- inversion H5.
- inversion H1; subst.
- inversion H2; subst.
- inversion H3; subst. clear H8. clear H7.
- inversion H; subst. inversion H5.
- inversion H4; subst.
- inversion H6; subst.
- apply iit0_id1; auto. apply isidentity1; auto.
- clear H10. clear H8.
- apply iit0_id1; auto. apply isidentity1; auto.
- inversion H4; subst. inversion H; subst.
- inversion H8.
- inversion H6.
- apply iit0_term; auto.
- clear H7; subst.
- inversion H; subst.
- inversion H4; subst.
- apply iit0_term; auto.
- inversion H4; subst.
- inversion H7; subst. clear H14.
- apply iit0_id1; auto. apply isidentity1; auto.
- clear H13.
- apply iit0_id1; auto. apply isidentity1; auto.
- inversion H4; subst.
- inversion H; subst.
- inversion H10.
- inversion H7.
- apply iit0_term; auto.
- inversion H1; subst.
- inversion H; subst.
- inversion H3; subst. apply iit0_term; auto.
- inversion H4.
- inversion H4.
- Qed.
-
- (* Formalized Definition 4.8 *)
- Definition Types0 := SubCategoriesAreCategories Judgments Types0P.
- End Types0.
-
- (* Formalized Definition 4.11 *)
- Instance Judgments_binoidal : BinoidalCat Judgments (fun a b:Tree ??Sequent => a,,b) :=
- { bin_first := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => a,,x) (fun a b (f:a/⋯⋯/b) => f**(nd_id x)) _ _ _
- ; bin_second := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => x,,a) (fun a b (f:a/⋯⋯/b) => (nd_id x)**f) _ _ _
- }.
- intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
- intros. simpl. reflexivity.
- intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
- intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
- intros. simpl. reflexivity.
- intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
- Defined.
-
- Definition jud_assoc_iso (a b c:Judgments) : @Isomorphic _ _ Judgments ((a,,b),,c) (a,,(b,,c)).
- apply (@Build_Isomorphic _ _ Judgments _ _ nd_assoc nd_cossa); simpl; auto.
- Defined.
- Definition jud_cancelr_iso (a:Judgments) : @Isomorphic _ _ Judgments (a,,[]) a.
- apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancelr nd_rlecnac); simpl; auto.
- Defined.
- Definition jud_cancell_iso (a:Judgments) : @Isomorphic _ _ Judgments ([],,a) a.
- apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancell nd_llecnac); simpl; auto.
- Defined.
-
- (* just for this section *)
- Notation "a ⊗ b" := (@bin_obj _ _ Judgments _ Judgments_binoidal a b).
- Notation "c ⋊ -" := (@bin_second _ _ Judgments _ Judgments_binoidal c).
- Notation "- ⋉ c" := (@bin_first _ _ Judgments _ Judgments_binoidal c).
- Notation "c ⋊ f" := ((c ⋊ -) \ f).
- Notation "g ⋉ c" := ((- ⋉ c) \ g).
-
- Hint Extern 1 => apply (@nd_structural_id0 _ Rule).
- Hint Extern 1 => apply (@nd_structural_id1 _ Rule).
- Hint Extern 1 => apply (@nd_structural_weak _ Rule).
- Hint Extern 1 => apply (@nd_structural_copy _ Rule).
- Hint Extern 1 => apply (@nd_structural_prod _ Rule).
- Hint Extern 1 => apply (@nd_structural_comp _ Rule).
- Hint Extern 1 => apply (@nd_structural_cancell _ Rule).
- Hint Extern 1 => apply (@nd_structural_cancelr _ Rule).
- Hint Extern 1 => apply (@nd_structural_llecnac _ Rule).
- Hint Extern 1 => apply (@nd_structural_rlecnac _ Rule).
- Hint Extern 1 => apply (@nd_structural_assoc _ Rule).
- Hint Extern 1 => apply (@nd_structural_cossa _ Rule).
- Hint Extern 2 => apply (@ndr_structural_indistinguishable _ Rule).
-
- Program Instance Judgments_premonoidal : PreMonoidalCat Judgments_binoidal [ ] :=
- { pmon_assoc := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso a x b)) _
- ; pmon_cancell := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancell_iso x)) _
- ; pmon_cancelr := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancelr_iso x)) _
- ; pmon_assoc_rr := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso x a b)⁻¹) _
- ; pmon_assoc_ll := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => jud_assoc_iso a b x) _
- }.
- Next Obligation.
- setoid_rewrite (ndr_prod_associativity (nd_id a) f (nd_id b)).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
- Defined.
- Next Obligation.
- setoid_rewrite (ndr_prod_right_identity f).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
- Defined.
- Next Obligation.
- setoid_rewrite (ndr_prod_left_identity f).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
- Defined.
- Next Obligation.
- apply Build_Pentagon; intros.
- simpl; apply ndr_structural_indistinguishable; auto.
- Defined.
- Next Obligation.
- apply Build_Triangle; intros;
- simpl; apply ndr_structural_indistinguishable; auto.
- Defined.
- Next Obligation.
- setoid_rewrite (ndr_prod_associativity f (nd_id a) (nd_id b)).
- repeat setoid_rewrite <- ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
- Defined.
- Next Obligation.
- setoid_rewrite (ndr_prod_associativity (nd_id a) (nd_id b) f).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
- Defined.
- Check (@Judgments_premonoidal). (* to force Coq to verify that we've finished all the obligations *)
-
- Definition Judgments_monoidal_endofunctor_fobj : Judgments ×× Judgments -> Judgments :=
- (fun xy =>
- match xy with
- | pair_obj x y => T_Branch x y
- end).
- Definition Judgments_monoidal_endofunctor_fmor :
- forall a b, (a~~{Judgments ×× Judgments}~~>b) ->
- ((Judgments_monoidal_endofunctor_fobj a)~~{Judgments}~~>(Judgments_monoidal_endofunctor_fobj b)).
- intros.
- destruct a.
- destruct b.
- destruct X.
- exact (h**h0).
- Defined.
- Definition Judgments_monoidal_endofunctor : Functor (Judgments ×× Judgments) Judgments Judgments_monoidal_endofunctor_fobj.
- refine {| fmor := Judgments_monoidal_endofunctor_fmor |}; intros; simpl.
- abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; apply ndr_prod_respects; auto).
- abstract (destruct a; simpl; reflexivity).
- abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; apply ndr_prod_preserves_comp).
- Defined.
-
- Instance Judgments_monoidal : MonoidalCat _ _ Judgments_monoidal_endofunctor [ ].
- admit.
- Defined.
-
- (* all morphisms in the category of Judgments are central; there's probably a very short route from here to CartesianCat *)
- Lemma all_central : forall a b:Judgments, forall (f:a~>b), CentralMorphism f.
- intros; apply Build_CentralMorphism; intros.
- simpl.
- setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
- setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) g f (nd_id _)).
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- reflexivity.
- simpl.
- setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
- setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- reflexivity.
- Defined.
-
- (*
- Instance NoHigherOrderFunctionTypes : SubCategory Judgments
- Instance NoFunctionTypes : SubCategory Judgments
- Lemma first_order_functions_eliminable : IsomorphicCategories NoHigherOrderFunctionTypes NoFunctionTypes
- *)