- (* Formalized Definition 4.6 *)
- Section Types1.
- Instance Types1 : Category T (fun t1 t2 => [ ] /⋯⋯/ [ [t1] |= [t2] ]) :=
- { eqv := fun ta tb pf1 pf2 => pf1 === pf2
- ; id := fun t => [#al_reflexive_seq [t]#]
- ; comp := fun {ta tb tc:T}(pf1:[]/⋯⋯/[[ta]|=[tb]])(pf2:[]/⋯⋯/[[tb]|=[tc]]) => nd_llecnac ;; ((pf1 ** pf2) ;; (al_subst _ _ _))
- }.
- 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
- *)
-
- (* Formalized Theorem 4.19 *)
- Instance Types_omega_e : ECategory Judgments_monoidal (Tree ??T) (fun tt1 tt2 => [ tt1 |= tt2 ]) :=
- { eid := fun tt => [#al_reflexive_seq tt#]
- ; ecomp := fun a b c => al_subst a b c
- }.
- admit.
- admit.
- admit.
- admit.
- admit.
- Defined.
-
- Definition Types_omega_monoidal_functor
- : Functor (Types_omega_e ×× Types_omega_e) Types_omega_e (fun a => match a with pair_obj a1 a2 => a1,,a2 end).
- admit.
- Defined.
-
- Instance Types_omega_monoidal : MonoidalCat Types_omega_e _ Types_omega_monoidal_functor [].
- admit.
- Defined.
-
- Definition AL_Enrichment : Enrichment.
- refine {| enr_c := Types_omega_e |}.
- Defined.
-
- Definition AL_SurjectiveEnrichment : SurjectiveEnrichment.
- refine {| se_enr := AL_Enrichment |}.
- unfold treeDecomposition.
- intros; induction d; simpl.
- destruct a.
- destruct s.
- exists [pair t t0]; auto.
- exists []; auto.
- destruct IHd1.
- destruct IHd2.
- exists (x,,x0); subst; auto.
- Defined.
-
- Definition AL_MonoidalEnrichment : MonoidalEnrichment.
- refine {| me_enr := AL_SurjectiveEnrichment ; me_mon := Types_omega_monoidal |}.
- admit.
- Defined.
-
- Definition AL_MonicMonoidalEnrichment : MonicMonoidalEnrichment.
- refine {| ffme_enr := AL_MonoidalEnrichment |}.
- admit.
- admit.
- admit.
- Defined.
-
- (*
- Instance Types_omega_be : BinoidalECategory Types_omega_e :=
- { bec_obj := fun tt1 tt2 => tt1,,tt2
- ; bec_efirst := fun a b c => nd_rule (@al_horiz_expand_right _ _ Lang _ _ _)
- ; bec_esecond := fun a b c => nd_rule (@al_horiz_expand_left _ _ Lang _ _ _)
- }.
- intros; apply all_central.
- intros; apply all_central.
- intros. unfold eid. simpl.
- setoid_rewrite <- al_horiz_expand_right_reflexive.
- reflexivity.
- intros. unfold eid. simpl.
- setoid_rewrite <- al_horiz_expand_left_reflexive.
- reflexivity.
- intros. simpl.
- set (@al_subst_commutes_with_horiz_expand_right _ _ _ a b c d) as q.
- setoid_rewrite <- q. clear q.
- apply ndr_comp_respects; try reflexivity.
- distribute.
- apply ndr_prod_respects.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; reflexivity.
- eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
- apply ndr_comp_respects; reflexivity.
- intros. simpl.
- set (@al_subst_commutes_with_horiz_expand_left _ _ _ a b c d) as q.
- setoid_rewrite <- q. clear q.
- apply ndr_comp_respects; try reflexivity.
- distribute.
- apply ndr_prod_respects.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; reflexivity.
- eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
- apply ndr_comp_respects; reflexivity.
- Defined.
- *)
-
- Definition Types_omega : Category _ (fun tt1 tt2 => [ ]/⋯⋯/[ tt1 |= tt2 ]) := Underlying Types_omega_e.
- Existing Instance Types_omega.
-
- (*
- Definition Types_omega_binoidal : BinoidalCat Types_omega (fun tt1 tt2 => tt1,,tt2) := Underlying_binoidal Types_omega_be.
- Existing Instance Types_omega_binoidal.
- *)
-
- (* takes an "operation in the context" (proof from [b|=Top]/⋯⋯/[a|=Top]) and turns it into a function a-->b; note the variance *)
- Definition context_operation_as_function
- : forall {a}{b} (f:[b|=[]]~~{Judgments}~~>[a|=[]]), []~~{Judgments}~~>[a|=b].
- intros.
- apply (@al_vert_expand_suc_right _ _ _ b _ _) in f.
- simpl in f.
- apply (@al_vert_expand_ant_left _ _ _ [] _ _) in f.
- simpl in f.
- set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
- exact f'.
- Defined.
-
- (* takes an "operation in the context" (proof from [Top|=a]/⋯⋯/[Top|=b]) and turns it into a function a-->b; note the variance *)
- Definition cocontext_operation_as_function
- : forall {a}{b} (f:[[]|=a]~~{Judgments}~~>[[]|=b]), []~~{Judgments}~~>[a|=b].
- intros. unfold hom. unfold hom in f.
- apply al_vert_expand_ant_right with (x:=a) in f.
- simpl in f.
- apply al_vert_expand_suc_left with (x:=[]) in f.
- simpl in f.
- set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
- exact f'.
- Defined.
-
-
- Definition function_as_context_operation
- : forall {a}{b}{c} (f:[]~~{Judgments}~~>[a|=b]), [b|=c]~~{Judgments}~~>[a|=c]
- := fun a b c f => RepresentableFunctorºᑭ Types_omega_e c \ f.
- Definition function_as_cocontext_operation
- : forall {a}{b}{c} (f:[]/⋯⋯/[a|=b]), [c|=a]~~{Judgments}~~>[c|=b]
- := fun a b c f => RepresentableFunctor Types_omega_e c \ f.
-