projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
fix proof that Judgments(L) is Cartesian
[coq-hetmet.git]
/
src
/
ProgrammingLanguage.v
diff --git
a/src/ProgrammingLanguage.v
b/src/ProgrammingLanguage.v
index
d1a0875
..
b00d1ad
100644
(file)
--- a/
src/ProgrammingLanguage.v
+++ b/
src/ProgrammingLanguage.v
@@
-248,11
+248,11
@@
Section Programming_Language.
apply al_subst_associativity'.
Defined.
apply al_subst_associativity'.
Defined.
- Definition TypesLEnrichedInJudgments0 : Enrichment.
+ Definition TypesEnrichedInJudgments : Enrichment.
refine {| enr_c := TypesLFC |}.
Defined.
refine {| enr_c := TypesLFC |}.
Defined.
- Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
+ Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
(*
eapply Build_EFunctor; intros.
eapply MonoidalCat_all_central.
(*
eapply Build_EFunctor; intros.
eapply MonoidalCat_all_central.
@@
-262,11
+262,11
@@
Section Programming_Language.
admit.
Defined.
admit.
Defined.
- Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
+ Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
admit.
Defined.
admit.
Defined.
- Definition TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _).
+ Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _).
refine
{| bin_first := TypesL_first
; bin_second := TypesL_second
refine
{| bin_first := TypesL_first
; bin_second := TypesL_second