From 57d183c7955fb54b3eb6dd431f5aec338131266b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 22 Feb 2019 23:45:50 +0100 Subject: Cleanups and reorganization --- Coprod.thy | 50 ------------- Empty.thy | 27 ------- Eq.thy | 27 ++++--- Equal.thy | 219 ------------------------------------------------------- HoTT.thy | 28 +++---- HoTT_Methods.thy | 5 +- More_Types.thy | 83 +++++++++++++++++++++ Nat.thy | 45 ++++++------ Prod.thy | 34 ++++----- Unit.thy | 32 -------- 10 files changed, 153 insertions(+), 397 deletions(-) delete mode 100644 Coprod.thy delete mode 100644 Empty.thy delete mode 100644 Equal.thy create mode 100644 More_Types.thy delete mode 100644 Unit.thy diff --git a/Coprod.thy b/Coprod.thy deleted file mode 100644 index b0a1ad2..0000000 --- a/Coprod.thy +++ /dev/null @@ -1,50 +0,0 @@ -(* -Title: Coprod.thy -Author: Joshua Chen -Date: 2018 - -Coproduct type -*) - -theory Coprod -imports HoTT_Base - -begin - - -axiomatization - Coprod :: "[t, t] \ t" (infixr "+" 50) and - inl :: "t \ t" and - inr :: "t \ t" and - indCoprod :: "[t \ t, t \ t, t] \ t" ("(1ind\<^sub>+)") -where - Coprod_form: "\A: U i; B: U i\ \ A + B: U i" and - - Coprod_intro_inl: "\a: A; B: U i\ \ inl a: A + B" and - - Coprod_intro_inr: "\b: B; A: U i\ \ inr b: A + B" and - - Coprod_elim: "\ - u: A + B; - C: A + B \ U i; - \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ c d u: C u" and - - Coprod_comp_inl: "\ - a: A; - C: A + B \ U i; - \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ c d (inl a) \ c a" and - - Coprod_comp_inr: "\ - b: B; - C: A + B \ U i; - \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ c d (inr b) \ d b" - -lemmas Coprod_form [form] -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim -lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr - - -end diff --git a/Empty.thy b/Empty.thy deleted file mode 100644 index ee11045..0000000 --- a/Empty.thy +++ /dev/null @@ -1,27 +0,0 @@ -(* -Title: Empty.thy -Author: Joshua Chen -Date: 2018 - -Empty type -*) - -theory Empty -imports HoTT_Base - -begin - - -axiomatization - Empty :: t ("\") and - indEmpty :: "t \ t" ("(1ind\<^sub>\)") -where - Empty_form: "\: U O" and - - Empty_elim: "\a: \; C: \ \ U i\ \ ind\<^sub>\ a: C a" - -lemmas Empty_form [form] -lemmas Empty_routine [intro] = Empty_form Empty_elim - - -end diff --git a/Eq.thy b/Eq.thy index e93dd8a..7783682 100644 --- a/Eq.thy +++ b/Eq.thy @@ -54,6 +54,9 @@ method path_ind for a b p :: t = method path_ind' for C :: "[t, t, t] \ t" = (rule Eq_elim[where ?C=C]; (assumption | fact)?) +syntax "_induct_over" :: "[idt, idt, idt, t] \ [t, t, t] \ t" ("(2{_, _, _}/ _)" 0) +translations "{x, y, p} C" \ "\x y p. C" + section \Properties of equality\ @@ -180,8 +183,12 @@ qed (routine add: assms) text \ We use the proof of associativity of path composition to demonstrate the process of deriving proof terms. -The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the form of the proof term in the first place. +The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place. However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. + +The proof is sensitive to the order of the quantifiers in the product. +In particular, changing the order causes unification to fail in the path inductions. +It seems to be good practice to order the variables in the order over which we will path-induct. \ declare[[pretty_pathcomp=false]] @@ -193,22 +200,22 @@ schematic_goal pathcomp_assoc: pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] pathcomp A x z w (pathcomp A x y z p q) r" apply (quantify 3) - apply (path_ind' - "\x y p. \(z: A). \(q: y =[A] z). \(w: A). \(r: z =[A] w). + apply (path_ind' "{x, y, p} + \(z: A). \(q: y =[A] z). \(w: A). \(r: z =[A] w). Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w] Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r") apply (quantify 2) - apply (path_ind' - "\xa z q. \(w: A). \(r: z =[A] w). + apply (path_ind' "{xa, z, q} + \(w: A). \(r: z =[A] w). Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w] Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r") apply (quantify 2) - apply (path_ind' - "\xb w r. Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] + apply (path_ind' "{xb, w, r} + Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r") - - text \\ - + + text \And now the rest is routine.\ + apply (derive; (rule assms|assumption)?) apply (compute, rule assms, assumption)+ apply (elim Eq_intro, rule Eq_intro, assumption) diff --git a/Equal.thy b/Equal.thy deleted file mode 100644 index 17c1c99..0000000 --- a/Equal.thy +++ /dev/null @@ -1,219 +0,0 @@ -(******** -Isabelle/HoTT: Equality -Feb 2019 - -********) - -theory Equal -imports Prod HoTT_Methods - -begin - - -section \Type definitions\ - -axiomatization - Eq :: "[t, t, t] \ t" and - refl :: "t \ t" and - indEq :: "[[t, t, t] \ t, t \ t, t, t, t] \ t" - -syntax - "_Eq" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) -translations - "a =[A] b" \ "(CONST Eq) A a b" - -axiomatization where - Eq_form: "\A: U i; a: A; b: A\ \ a =[A] b: U i" and - - Eq_intro: "a: A \ (refl a): a =[A] a" and - - Eq_elim: "\ - p: x =[A] y; - a: A; - b: A; - \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a b p : C a b p" and - - Eq_comp: "\ - a: A; - \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a a (refl a) \ f a" - -lemmas Eq_form [form] -lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim -lemmas Eq_comp [comp] - - -section \Path induction\ - -text \We set up rudimentary automation of path induction:\ - -method path_ind for a b p :: t = - (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (fact | assumption)?) - - -section \Properties of equality\ - -subsection \Symmetry (path inverse)\ - -definition inv :: "[t, t, t, t] \ t" -where "inv A x y p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) x y p" - -syntax "_inv" :: "t \ t" ("~_" [1000]) - -text \Pretty-printing switch for path inverse:\ - -ML \val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\ - -print_translation \ -let fun inv_tr' ctxt [A, x, y, p] = - if Config.get ctxt pretty_inv - then Syntax.const @{syntax_const "_inv"} $ p - else @{const inv} $ A $ x $ y $ p -in - [(@{const_syntax inv}, inv_tr')] -end -\ - -lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv A x y p: y =[A] x" -unfolding inv_def by derive - -lemma inv_comp: "\A: U i; a: A\ \ inv A a a (refl a) \ refl a" -unfolding inv_def by derive - -declare - inv_type [intro] - inv_comp [comp] - -subsection \Transitivity (path composition)\ - -schematic_goal transitivity: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?p: \z: A. y =[A]z \ x =[A] z" -proof (path_ind x y p, quantify_all) - fix x z show "\p. p: x =[A] z \ p: x =[A] z" . -qed (routine add: assms) - -definition pathcomp :: "[t, t, t, t, t, t] \ t" -where - "pathcomp A x y z p q \ - (indEq (\x y _. \z: A. y =[A] z \ x =[A] z) (\x. \y: A. id (x =[A] y)) x y p)`z`q" - -syntax "_pathcomp" :: "[t, t] \ t" (infixl "*" 110) - -text \Pretty-printing switch for path composition:\ - -ML \val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\ - -print_translation \ -let fun pathcomp_tr' ctxt [A, x, y, z, p, q] = - if Config.get ctxt pretty_pathcomp - then Syntax.const @{syntax_const "_pathcomp"} $ p $ q - else @{const pathcomp} $ A $ x $ y $ z $ p $ q -in - [(@{const_syntax pathcomp}, pathcomp_tr')] -end -\ - -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" - shows "pathcomp A x y z p q: x =[A] z" -unfolding pathcomp_def by (routine add: transitivity assms) - -lemma pathcomp_cmp: - assumes "A: U i" and "a: A" - shows "pathcomp A a a a (refl a) (refl a) \ refl a" -unfolding pathcomp_def by (derive lems: assms) - -lemmas pathcomp_type [intro] -lemmas pathcomp_comp [comp] = pathcomp_cmp - - -section \Higher groupoid structure of types\ - -schematic_goal pathcomp_idr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" -proof (path_ind x y p) - show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_idl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" -proof (path_ind x y p) - show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_invr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" -proof (path_ind x y p) - show - "\x. x: A \ refl(refl x): - pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_invl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" -proof (path_ind x y p) - show - "\x. x: A \ refl(refl x): - pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal inv_involutive: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" -proof (path_ind x y p) - show "\x. x: A \ refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -declare[[pretty_pathcomp=false]] - -schematic_goal pathcomp_assoc: - assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =[A] y" - shows - "?a: \q: y =[A] z. \r: z =[A] w. - pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] - pathcomp A x z w (pathcomp A x y z p q) r" -proof (path_ind x y p) - oops - schematic_goal l: - assumes "A: U i" "x: A" "z: A" "w: A" "q: x =[A] z" - shows - "?a: \r: z =[A] w. pathcomp A x x w (refl x) (pathcomp A y z w q r) =[x =[A] w] - pathcomp A x z w (pathcomp A x x z (refl x) q) r" - proof (path_ind x z q) - oops - schematic_goal l': - assumes "A: U i" "x: A" "w: A" "r: x =[A] w" - shows - "?a: pathcomp A x x w (refl x) (pathcomp A x x w (refl x) r) =[x =[A] w] - pathcomp A x x w (pathcomp A x x x (refl x) (refl x)) r" - proof (path_ind x w r) - show "\x. x: A \ refl(refl x): - pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] - pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - by (derive lems: assms) - qed (routine add: assms) - -(* Possible todo: - implement a custom version of schematic_goal/theorem that exports the derived proof term. -*) - -definition l'_prftm :: "[t, t, t, t] \ t" -where "l'_prftm A x w r\ - indEq - (\a b c. pathcomp A a a b (refl a) (pathcomp A a a b (refl a) c) =[a =[A] b] - pathcomp A a a b (pathcomp A a a a (refl a) (refl a)) c) - (\x. refl (refl x)) x w r" - - -end diff --git a/HoTT.thy b/HoTT.thy index 6c6ad21..e5db673 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -1,44 +1,40 @@ -(* -Title: HoTT.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT +Feb 2019 -Homotopy type theory -*) +An experimental implementation of homotopy type theory. + +********) theory HoTT imports + (* Basic theories *) HoTT_Base HoTT_Methods (* Types *) -Coprod -Empty -Equal +Eq Nat Prod Sum -Unit +More_Types (* Derived definitions and properties *) -Equality Projections Univalence begin - text \Rule bundles:\ lemmas intros = - Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Eq_intro Cprd_intro_inl Cprd_intro_inr Unit_intro lemmas elims = - Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim + Nat_elim Prod_elim Sum_elim Eq_elim Cprd_elim Unit_elim Null_elim lemmas routines = - Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine - + Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 099a73e..c9744e9 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -51,7 +51,7 @@ method cumulativity declares form = ( section \Deriving typing judgments\ -method routine uses add = (rule add | assumption | rule)+ +method routine uses add = (assumption | rule add | rule)+ text \ The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. @@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute It also handles universes using @{method hierarchy} and @{method cumulativity}. \ -method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ +method derive uses lems = + (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \Additional method combinators\ diff --git a/More_Types.thy b/More_Types.thy new file mode 100644 index 0000000..9125aca --- /dev/null +++ b/More_Types.thy @@ -0,0 +1,83 @@ +(******** +Isabelle/HoTT: Coproduct, unit, and empty types +Feb 2019 + +********) + +theory More_Types +imports HoTT_Base + +begin + + +section \Coproduct type\ + +axiomatization + Cprd :: "[t, t] \ t" (infixr "+" 50) and + inl :: "[t, t, t] \ t" and + inr :: "[t, t, t] \ t" and + indCprd :: "[t \ t, t \ t, t \ t, t] \ t" +where + Cprd_form: "\A: U i; B: U i\ \ A + B: U i" and + + Cprd_intro_inl: "\a: A; B: U i\ \ inl A B a: A + B" and + + Cprd_intro_inr: "\b: B; A: U i\ \ inr A B b: A + B" and + + Cprd_elim: "\ + u: A + B; + C: A + B \ U i; + \x. x: A \ c x: C (inl A B x); + \y. y: B \ d y: C (inr A B y) \ \ indCprd C c d u: C u" and + + Cprd_cmp_inl: "\ + a: A; + C: A + B \ U i; + \x. x: A \ c x: C (inl A B x); + \y. y: B \ d y: C (inr A B y) \ \ indCprd C c d (inl A B a) \ c a" and + + Cprd_cmp_inr: "\ + b: B; + C: A + B \ U i; + \x. x: A \ c x: C (inl A B x); + \y. y: B \ d y: C (inr A B y) \ \ indCprd C c d (inr A B b) \ d b" + +lemmas Cprd_form [form] +lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim +lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr + + +section \Unit type\ + +axiomatization + Unit :: t and + pt :: t and + indUnit :: "[t \ t, t, t] \ t" +where + Unit_form: "Unit: U O" and + + Unit_intro: "pt: Unit" and + + Unit_elim: "\x: Unit; c: C pt; C: Unit \ U i\ \ indUnit C c x: C x" and + + Unit_cmp: "\c: C Unit; C: Unit \ U i\ \ indUnit C c pt \ c" + +lemmas Unit_form [form] +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_cmp [comp] + + +section \Empty type\ + +axiomatization + Null :: t and + indNull :: "[t \ t, t] \ t" +where + Null_form: "Null: U O" and + + Null_elim: "\z: Null; C: Null \ U i\ \ indNull C z: C z" + +lemmas Null_form [form] +lemmas Null_routine [intro] = Null_form Null_elim + +end diff --git a/Nat.thy b/Nat.thy index 657e790..61e03e8 100644 --- a/Nat.thy +++ b/Nat.thy @@ -1,49 +1,46 @@ -(* -Title: Nat.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Natural numbers +Feb 2019 -Natural numbers -*) +********) theory Nat imports HoTT_Base begin - axiomatization - Nat :: t ("\") and + Nat :: t and zero :: t ("0") and succ :: "t \ t" and - indNat :: "[[t, t] \ t, t, t] \ t" ("(1ind\<^sub>\)") + indNat :: "[t \ t, [t, t] \ t, t, t] \ t" where - Nat_form: "\: U O" and + Nat_form: "Nat: U O" and - Nat_intro_0: "0: \" and + Nat_intro_0: "0: Nat" and - Nat_intro_succ: "n: \ \ succ n: \" and + Nat_intro_succ: "n: Nat \ succ n: Nat" and Nat_elim: "\ a: C 0; - n: \; - C: \ \ U i; - \n c. \n: \; c: C n\ \ f n c: C (succ n) \ \ ind\<^sub>\ f a n: C n" and + n: Nat; + C: Nat \ U i; + \n c. \n: Nat; c: C n\ \ f n c: C (succ n) \ \ indNat C f a n: C n" and - Nat_comp_0: "\ + Nat_cmp_0: "\ a: C 0; - C: \ \ U i; - \n c. \n: \; c: C(n)\ \ f n c: C (succ n) \ \ ind\<^sub>\ f a 0 \ a" and + C: Nat \ U i; + \n c. \n: Nat; c: C n\ \ f n c: C (succ n) \ \ indNat C f a 0 \ a" and - Nat_comp_succ: "\ + Nat_cmp_succ: "\ a: C 0; - n: \; - C: \ \ U i; - \n c. \n: \; c: C n\ \ f n c: C (succ n) \ \ ind\<^sub>\ f a (succ n) \ f n (ind\<^sub>\ f a n)" + n: Nat; + C: Nat \ U i; + \n c. \n: Nat; c: C n\ \ f n c: C (succ n) + \ \ indNat C f a (succ n) \ f n (indNat C f a n)" lemmas Nat_form [form] lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim -lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ - +lemmas Nat_comps [comp] = Nat_cmp_0 Nat_cmp_succ end diff --git a/Prod.thy b/Prod.thy index ff62ee6..059932c 100644 --- a/Prod.thy +++ b/Prod.thy @@ -70,23 +70,6 @@ lemmas Prod_comp [comp] = Prod_cmp Prod_uniq lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq -section \Universal quantification\ - -text \ -It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. - -Method @{theory_text quantify_all} converts the goal -@{text "t: \x1: A1. ... \xn: An. B x1 ... xn"}, -where @{term B} is not a product, to -@{text "\x1 ... xn . \x1: A1; ...; xn: An\ \ ?b x1 ... xn: B x1 ... xn"}. - -Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. -\ - -method quantify_all = (rule Prod_intro)+ -method_setup quantify = \repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\ - - section \Function composition\ definition compose :: "[t, t, t] \ t" @@ -146,4 +129,21 @@ by (derive lems: assms cong) abbreviation id :: "t \ t" where "id A \ \x: A. x" + +section \Universal quantification\ + +text \ +It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. + +Method @{theory_text quantify_all} converts the goal +@{text "t: \x1: A1. ... \xn: An. B x1 ... xn"}, +where @{term B} is not a product, to +@{text "\x1 ... xn . \x1: A1; ...; xn: An\ \ ?b x1 ... xn: B x1 ... xn"}. + +Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. +\ + +method quantify_all = (rule Prod_intro)+ +method_setup quantify = \repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\ + end diff --git a/Unit.thy b/Unit.thy deleted file mode 100644 index 7c221f0..0000000 --- a/Unit.thy +++ /dev/null @@ -1,32 +0,0 @@ -(* -Title: Unit.thy -Author: Joshua Chen -Date: 2018 - -Unit type -*) - -theory Unit -imports HoTT_Base - -begin - - -axiomatization - Unit :: t ("\") and - pt :: t ("\") and - indUnit :: "[t, t] \ t" ("(1ind\<^sub>\)") -where - Unit_form: "\: U O" and - - Unit_intro: "\: \" and - - Unit_elim: "\a: \; c: C \; C: \ \ U i\ \ ind\<^sub>\ c a: C a" and - - Unit_comp: "\c: C \; C: \ \ U i\ \ ind\<^sub>\ c \ \ c" - -lemmas Unit_form [form] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim -lemmas Unit_comp [comp] - -end -- cgit v1.2.3