Last active
June 24, 2023 11:55
-
-
Save Skantz/52047f07f044846b0af2774b981d10c7 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/TypeTheory/Initiality/Interpretation.v b/TypeTheory/Initiality/Interpretation.v | |
index 4693be2..112e29c 100644 | |
--- a/TypeTheory/Initiality/Interpretation.v | |
+++ b/TypeTheory/Initiality/Interpretation.v | |
@@ -1,14 +1,6 @@ | |
(** This file defines the interpretation function, from the syntax of our toy type theory into any split type-cat with suitable structure. *) | |
-(** * TODO NOTE: This file depends on Coq.Init.Logic. | |
- Removing the following line causes the error: | |
- | |
- File "./TypeTheory/TypeTheory/Initiality/Interpretation.v", line 366, characters 4-5: | |
- Error: [Focus] Wrong bullet -: Current bullet + is not finished. | |
- *) | |
-Require Import Coq.Init.Logic. | |
- | |
Require Import UniMath.MoreFoundations.All. | |
Require Import UniMath.CategoryTheory.Core.Prelude. | |
@@ -362,7 +354,7 @@ Section Partial_Interpretation. | |
apply funextfun; intros i. apply maponpaths_2. | |
eapply pathscomp0. 2: { apply partial_interpretation_rename_ty. } | |
apply maponpaths_2, funextfun. | |
- refine (dB_Sn_rect _ _ _); auto. | |
+ refine (dB_Sn_rect _ _ _); reflexivity. | |
- (* term expressions *) | |
destruct e as [ m i | m A B b | m A B t a ]. | |
+ (* [var_expr i] *) | |
@@ -373,7 +365,7 @@ Section Partial_Interpretation. | |
apply funextfun; intros A_interp. | |
assert (e_EA : (extend_environment (E ∘ f) A_interp | |
= extend_environment E A_interp ∘ fmap_dB_S f)). | |
- { apply funextfun. refine (dB_Sn_rect _ _ _); auto. } | |
+ { apply funextfun. refine (dB_Sn_rect _ _ _); reflexivity. } | |
apply maponpaths_12. | |
{ eapply pathscomp0. 2: { apply partial_interpretation_rename_ty. } | |
apply maponpaths_2, e_EA. } | |
@@ -386,7 +378,7 @@ Section Partial_Interpretation. | |
apply funextfun; intros A_interp. | |
assert (e_EA : (extend_environment (E ∘ f) A_interp | |
= extend_environment E A_interp ∘ fmap_dB_S f)). | |
- { apply funextfun. refine (dB_Sn_rect _ _ _); auto. } | |
+ { apply funextfun. refine (dB_Sn_rect _ _ _); reflexivity. } | |
apply maponpaths_12. | |
{ eapply pathscomp0. 2: { apply partial_interpretation_rename_ty. } | |
apply maponpaths_2, e_EA. } | |
@@ -514,7 +506,7 @@ a little more work to state. *) | |
apply make_leq_partial'; cbn; intros [f_def b_def]. | |
use tpair. | |
- refine (dB_Sn_rect _ _ _); assumption. | |
- - apply funextfun. refine (dB_Sn_rect _ _ _); auto. | |
+ - apply funextfun. refine (dB_Sn_rect _ _ _); reflexivity. | |
Defined. | |
Definition partial_interpretation_tm_as_raw_context_map | |
diff --git a/TypeTheory/TypeCat/General.v b/TypeTheory/TypeCat/General.v | |
index 1fffe1f..41daed8 100644 | |
--- a/TypeTheory/TypeCat/General.v | |
+++ b/TypeTheory/TypeCat/General.v | |
@@ -5,13 +5,6 @@ Note: much of this essentially duplicates material given already in the [CwF_Spl | |
Probably much of this really should belong in a different package. *) | |
-(** * TODO NOTE: This file depends on Coq.Init.Logic. | |
- Removing the following line causes the error: | |
- | |
- File "./TypeTheory/TypeTheory/TypeCat/General.v", line 365, characters 6-115: | |
- Error: not found in table: core.eq.type | |
- *) | |
-Require Import Coq.Init.Logic. | |
Require Import UniMath.MoreFoundations.All. | |
Require Import TypeTheory.Auxiliary.CategoryTheoryImports. | |
@@ -362,7 +355,8 @@ Section Terms. | |
rewrite !maponpathscomp0, !idtoiso_concat_pr, <-!assoc. | |
etrans; [ do 2 eapply maponpaths; rewrite assoc; | |
apply (!q_comp_typecat A (dpr_typecat A) a)|]. | |
- now rewrite af, id_left, q_id_typecat, | |
+ destruct e, (!af). | |
+ now rewrite id_left, q_id_typecat, | |
<- idtoiso_concat_pr, <-maponpathscomp0, pathsinv0l. | |
Qed. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment