From 21077433667f6c2281aa522f170b93bb0c8c23ea Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 18 Jun 2018 17:16:30 +0200
Subject: Fixed wrong definition of snd_dep. Proved projection property of
 snd_dep. Added type formation rules expressing necessity of the conditions.

---
 HoTT_Base.thy | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 7794601..a0078fa 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,7 +7,6 @@ Basic setup and definitions of a homotopy type theory object logic without unive
 
 theory HoTT_Base
   imports Pure
-
 begin
 
 section \<open>Setup\<close>
@@ -34,7 +33,7 @@ consts
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
 
 axiomatization where
-  inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U"
+  inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
-- 
cgit v1.2.3