Merge pull request #238 from Skantz/initlogic

#235: Remove dependency on Coq.Init.Logic

Author: benediktahrens

TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Equiv_Cats.v

@@ -16,6 +16,7 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences.
+Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

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

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.