refactor(hott.init): remove subdirectories, merge some files
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
86012d841b
commit
052fbe0228
16 changed files with 176 additions and 223 deletions
|
|
@ -1,6 +0,0 @@
|
|||
init.axioms
|
||||
===========
|
||||
|
||||
* [ua](ua.hlean) : the univalence axiom
|
||||
* [funext_varieties](funext_varieties.hlean) : versions of function extensionality
|
||||
* [funext_of_ua](funext_of_ua.hlean) : univalence implies funext
|
||||
|
|
@ -1,109 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.axioms.funext_varieties
|
||||
Authors: Jakob von Raumer
|
||||
|
||||
Ported from Coq HoTT
|
||||
-/
|
||||
|
||||
prelude
|
||||
import ..path ..trunc ..equiv
|
||||
|
||||
open eq is_trunc sigma function
|
||||
|
||||
/- In init.axioms.funext, we defined function extensionality to be the assertion
|
||||
that the map apd10 is an equivalence. We now prove that this follows
|
||||
from a couple of weaker-looking forms of function extensionality. We do
|
||||
require eta conversion, which Coq 8.4+ has judgmentally.
|
||||
|
||||
This proof is originally due to Voevodsky; it has since been simplified
|
||||
by Peter Lumsdaine and Michael Shulman. -/
|
||||
|
||||
definition funext.{l k} :=
|
||||
Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g)
|
||||
|
||||
-- Naive funext is the simple assertion that pointwise equal functions are equal.
|
||||
definition naive_funext :=
|
||||
Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
|
||||
|
||||
-- Weak funext says that a product of contractible types is contractible.
|
||||
definition weak_funext :=
|
||||
Π ⦃A : Type⦄ (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
|
||||
|
||||
definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
|
||||
(λ nf A P (Pc : Πx, is_contr (P x)),
|
||||
let c := λx, center (P x) in
|
||||
is_contr.mk c (λ f,
|
||||
have eq' : (λx, center (P x)) ∼ f,
|
||||
from (λx, contr (f x)),
|
||||
have eq : (λx, center (P x)) = f,
|
||||
from nf A P (λx, center (P x)) f eq',
|
||||
eq
|
||||
)
|
||||
)
|
||||
|
||||
/- The less obvious direction is that WeakFunext implies Funext
|
||||
(and hence all three are logically equivalent). The point is that under weak
|
||||
funext, the space of "pointwise homotopies" has the same universal property as
|
||||
the space of paths. -/
|
||||
|
||||
section
|
||||
universe variables l k
|
||||
parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
|
||||
|
||||
definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
|
||||
is_contr.mk (sigma.mk f (homotopy.refl f))
|
||||
(λ dp, sigma.rec_on dp
|
||||
(λ (g : Π x, B x) (h : f ∼ g),
|
||||
let r := λ (k : Π x, Σ y, f x = y),
|
||||
@sigma.mk _ (λg, f ∼ g)
|
||||
(λx, pr1 (k x)) (λx, pr2 (k x)) in
|
||||
let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
|
||||
have t1 : Πx, is_contr (Σ y, f x = y),
|
||||
from (λx, !is_contr_sigma_eq),
|
||||
have t2 : is_contr (Πx, Σ y, f x = y),
|
||||
from !wf,
|
||||
have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
|
||||
from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _,
|
||||
have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
|
||||
from ap r t3,
|
||||
have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
|
||||
from t4,
|
||||
endt
|
||||
)
|
||||
)
|
||||
|
||||
parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
|
||||
|
||||
definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
|
||||
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
|
||||
(@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d
|
||||
|
||||
local attribute weak_funext [reducible]
|
||||
local attribute homotopy_ind [reducible]
|
||||
definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
|
||||
(@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
|
||||
end
|
||||
|
||||
-- Now the proof is fairly easy; we can just use the same induction principle on both sides.
|
||||
universe variables l k
|
||||
|
||||
local attribute weak_funext [reducible]
|
||||
theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
|
||||
λ A B f g,
|
||||
let eq_to_f := (λ g' x, f = g') in
|
||||
let sim2path := homotopy_ind f eq_to_f idp in
|
||||
assert t1 : sim2path f (homotopy.refl f) = idp,
|
||||
proof homotopy_ind_comp f eq_to_f idp qed,
|
||||
assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
|
||||
proof ap apd10 t1 qed,
|
||||
have sect : apd10 ∘ (sim2path g) ∼ id,
|
||||
proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed,
|
||||
have retr : (sim2path g) ∘ apd10 ∼ id,
|
||||
from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)),
|
||||
is_equiv.adjointify apd10 (sim2path g) sect retr
|
||||
|
||||
definition funext_from_naive_funext : naive_funext -> funext :=
|
||||
compose funext_of_weak_funext weak_funext_of_naive_funext
|
||||
|
|
@ -7,7 +7,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation
|
||||
import init.reserved_notation
|
||||
|
||||
namespace bool
|
||||
definition cond {A : Type} (b : bool) (t e : A) :=
|
||||
|
|
|
|||
|
|
@ -19,12 +19,6 @@ notation `Type₃` := Type.{3}
|
|||
inductive unit.{l} : Type.{l} :=
|
||||
star : unit
|
||||
|
||||
namespace unit
|
||||
|
||||
notation `⋆` := star
|
||||
|
||||
end unit
|
||||
|
||||
inductive empty.{l} : Type.{l}
|
||||
|
||||
inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
|
||||
|
|
@ -46,6 +40,9 @@ sum.inl a
|
|||
definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B :=
|
||||
sum.inr b
|
||||
|
||||
structure sigma {A : Type} (B : A → Type) :=
|
||||
mk :: (pr1 : A) (pr2 : B pr1)
|
||||
|
||||
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
|
||||
-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
|
||||
-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
|
||||
|
|
@ -63,7 +60,6 @@ inductive num : Type :=
|
|||
| zero : num
|
||||
| pos : pos_num → num
|
||||
|
||||
|
||||
namespace num
|
||||
open pos_num
|
||||
definition succ (a : num) : num :=
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ Authors: Leonardo de Moura, Jakob von Raumer
|
|||
prelude
|
||||
import init.datatypes init.reserved_notation init.tactic init.logic
|
||||
import init.bool init.num init.priority init.relation init.wf
|
||||
import init.types.sigma init.types.prod init.types.empty
|
||||
import init.types
|
||||
import init.trunc init.path init.equiv init.util
|
||||
import init.axioms.ua init.axioms.funext_of_ua
|
||||
import init.ua init.funext
|
||||
import init.hedberg init.nat init.hit
|
||||
|
|
|
|||
|
|
@ -2,17 +2,114 @@
|
|||
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.axioms.funext_of_ua
|
||||
Author: Jakob von Raumer
|
||||
Module: init.funext
|
||||
Authors: Jakob von Raumer
|
||||
|
||||
Ported from Coq HoTT
|
||||
-/
|
||||
|
||||
prelude
|
||||
import ..equiv ..datatypes ..types.prod
|
||||
import .funext_varieties .ua
|
||||
import .trunc .equiv .ua
|
||||
open eq is_trunc sigma function is_equiv equiv prod unit
|
||||
|
||||
open eq function prod is_trunc sigma equiv is_equiv unit
|
||||
/-
|
||||
We now prove that funext follows from a couple of weaker-looking forms
|
||||
of function extensionality.
|
||||
|
||||
This proof is originally due to Voevodsky; it has since been simplified
|
||||
by Peter Lumsdaine and Michael Shulman.
|
||||
-/
|
||||
|
||||
definition funext.{l k} :=
|
||||
Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g)
|
||||
|
||||
-- Naive funext is the simple assertion that pointwise equal functions are equal.
|
||||
definition naive_funext :=
|
||||
Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
|
||||
|
||||
-- Weak funext says that a product of contractible types is contractible.
|
||||
definition weak_funext :=
|
||||
Π ⦃A : Type⦄ (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
|
||||
|
||||
definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
|
||||
(λ nf A P (Pc : Πx, is_contr (P x)),
|
||||
let c := λx, center (P x) in
|
||||
is_contr.mk c (λ f,
|
||||
have eq' : (λx, center (P x)) ∼ f,
|
||||
from (λx, contr (f x)),
|
||||
have eq : (λx, center (P x)) = f,
|
||||
from nf A P (λx, center (P x)) f eq',
|
||||
eq
|
||||
)
|
||||
)
|
||||
|
||||
/-
|
||||
The less obvious direction is that weak_funext implies funext
|
||||
(and hence all three are logically equivalent). The point is that under weak
|
||||
funext, the space of "pointwise homotopies" has the same universal property as
|
||||
the space of paths.
|
||||
-/
|
||||
|
||||
section
|
||||
universe variables l k
|
||||
parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
|
||||
|
||||
definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
|
||||
is_contr.mk (sigma.mk f (homotopy.refl f))
|
||||
(λ dp, sigma.rec_on dp
|
||||
(λ (g : Π x, B x) (h : f ∼ g),
|
||||
let r := λ (k : Π x, Σ y, f x = y),
|
||||
@sigma.mk _ (λg, f ∼ g)
|
||||
(λx, pr1 (k x)) (λx, pr2 (k x)) in
|
||||
let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
|
||||
have t1 : Πx, is_contr (Σ y, f x = y),
|
||||
from (λx, !is_contr_sigma_eq),
|
||||
have t2 : is_contr (Πx, Σ y, f x = y),
|
||||
from !wf,
|
||||
have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
|
||||
from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _,
|
||||
have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
|
||||
from ap r t3,
|
||||
have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
|
||||
from t4,
|
||||
endt
|
||||
)
|
||||
)
|
||||
|
||||
parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
|
||||
|
||||
definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
|
||||
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
|
||||
(@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d
|
||||
|
||||
local attribute weak_funext [reducible]
|
||||
local attribute homotopy_ind [reducible]
|
||||
definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
|
||||
(@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
|
||||
end
|
||||
|
||||
/- Now the proof is fairly easy; we can just use the same induction principle on both sides. -/
|
||||
section
|
||||
universe variables l k
|
||||
|
||||
local attribute weak_funext [reducible]
|
||||
theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
|
||||
λ A B f g,
|
||||
let eq_to_f := (λ g' x, f = g') in
|
||||
let sim2path := homotopy_ind f eq_to_f idp in
|
||||
assert t1 : sim2path f (homotopy.refl f) = idp,
|
||||
proof homotopy_ind_comp f eq_to_f idp qed,
|
||||
assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
|
||||
proof ap apd10 t1 qed,
|
||||
have sect : apd10 ∘ (sim2path g) ∼ id,
|
||||
proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed,
|
||||
have retr : (sim2path g) ∘ apd10 ∼ id,
|
||||
from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)),
|
||||
is_equiv.adjointify apd10 (sim2path g) sect retr
|
||||
|
||||
definition funext_from_naive_funext : naive_funext → funext :=
|
||||
compose funext_of_weak_funext weak_funext_of_naive_funext
|
||||
end
|
||||
|
||||
section
|
||||
universe variables l
|
||||
|
|
@ -13,13 +13,13 @@ Syntax declarations:
|
|||
|
||||
Datatypes and logic:
|
||||
|
||||
* [datatypes](datatypes.hlean)
|
||||
* [logic](logic.hlean)
|
||||
* [datatypes](datatypes.hlean) (declaration of common types)
|
||||
* [bool](bool.hlean)
|
||||
* [num](num.hlean)
|
||||
* [nat](nat.hlean)
|
||||
* [function](function.hlean)
|
||||
* [types](types/types.md) (subfolder)
|
||||
* [types](types.hlean) (notation and some theorems for the remaining basic types)
|
||||
|
||||
HoTT basics:
|
||||
|
||||
|
|
@ -27,7 +27,8 @@ HoTT basics:
|
|||
* [hedberg](hedberg.hlean)
|
||||
* [trunc](trunc.hlean)
|
||||
* [equiv](equiv.hlean)
|
||||
* [axioms](axioms/axioms.md) (subfolder)
|
||||
* [ua](ua.hlean) (declaration of the univalence axiom, and some basic properties)
|
||||
* [funext](funext.hlean) (proof of equivalence of certain notions of function exensionality, and a proof that function extensionality follows from univalence)
|
||||
|
||||
Support for well-founded recursion and automation:
|
||||
|
||||
|
|
@ -38,4 +39,3 @@ Support for well-founded recursion and automation:
|
|||
The default import:
|
||||
|
||||
* [default](default.hlean)
|
||||
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation
|
||||
import init.reserved_notation
|
||||
|
||||
definition not.{l} (a : Type.{l}) := a → empty.{l}
|
||||
prefix `¬` := not
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Authors: Floris van Doorn, Leonardo de Moura
|
|||
-/
|
||||
|
||||
prelude
|
||||
import init.wf init.tactic init.hedberg init.util init.types.sum
|
||||
import init.wf init.tactic init.hedberg init.util init.types
|
||||
|
||||
open eq.ops decidable sum
|
||||
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ TODO: can we replace some definitions with a hprop as codomain by theorems?
|
|||
-/
|
||||
|
||||
prelude
|
||||
import .logic .equiv .types.empty .types.sigma
|
||||
import .logic .equiv .types
|
||||
open eq nat sigma unit
|
||||
|
||||
namespace is_trunc
|
||||
|
|
|
|||
|
|
@ -1,20 +1,73 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.types.prod
|
||||
Author: Leonardo de Moura, Jeremy Avigad
|
||||
Module: init.types
|
||||
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
prelude
|
||||
import ..wf ..num
|
||||
import .logic .num .wf
|
||||
|
||||
-- Empty type
|
||||
-- ----------
|
||||
|
||||
namespace empty
|
||||
|
||||
protected theorem elim (A : Type) (H : empty) : A :=
|
||||
empty.rec (λe, A) H
|
||||
|
||||
end empty
|
||||
|
||||
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
|
||||
take (a b : empty), decidable.inl (!empty.elim a)
|
||||
|
||||
-- Unit type
|
||||
-- ---------
|
||||
|
||||
namespace unit
|
||||
|
||||
notation `⋆` := star
|
||||
|
||||
end unit
|
||||
|
||||
-- Sigma type
|
||||
-- ----------
|
||||
|
||||
notation `Σ` binders `,` r:(scoped P, sigma P) := r
|
||||
|
||||
namespace sigma
|
||||
notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
|
||||
|
||||
namespace ops
|
||||
postfix `.1`:(max+1) := pr1
|
||||
postfix `.2`:(max+1) := pr2
|
||||
abbreviation pr₁ := @pr1
|
||||
abbreviation pr₂ := @pr2
|
||||
end ops
|
||||
end sigma
|
||||
|
||||
-- Sum type
|
||||
-- --------
|
||||
|
||||
namespace sum
|
||||
infixr ⊎ := sum
|
||||
infixr + := sum
|
||||
namespace low_precedence_plus
|
||||
reserve infixr `+`:25 -- conflicts with notation for addition
|
||||
infixr `+` := sum
|
||||
end low_precedence_plus
|
||||
end sum
|
||||
|
||||
-- Product type
|
||||
-- ------------
|
||||
|
||||
definition pair := @prod.mk
|
||||
|
||||
namespace prod
|
||||
|
||||
notation A * B := prod A B
|
||||
notation A × B := prod A B
|
||||
infixr * := prod
|
||||
infixr × := prod
|
||||
|
||||
namespace ops
|
||||
postfix `.1`:(max+1) := pr1
|
||||
|
|
@ -30,7 +83,6 @@ namespace prod
|
|||
|
||||
end low_precedence_times
|
||||
|
||||
-- TODO: add lemmas about flip to hott/types/prod.hlean
|
||||
definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
|
||||
|
||||
notation `pr₁` := pr1
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.types.empty
|
||||
Author: Jeremy Avigad, Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
prelude
|
||||
import ..datatypes ..logic
|
||||
|
||||
-- Empty type
|
||||
-- ----------
|
||||
|
||||
namespace empty
|
||||
|
||||
protected theorem elim (A : Type) (H : empty) : A :=
|
||||
empty.rec (λe, A) H
|
||||
|
||||
end empty
|
||||
|
||||
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
|
||||
take (a b : empty), decidable.inl (!empty.elim a)
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.types.sigma
|
||||
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||
-/
|
||||
|
||||
prelude
|
||||
import init.num
|
||||
|
||||
structure sigma {A : Type} (B : A → Type) :=
|
||||
mk :: (pr1 : A) (pr2 : B pr1)
|
||||
|
||||
notation `Σ` binders `,` r:(scoped P, sigma P) := r
|
||||
|
||||
namespace sigma
|
||||
notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
|
||||
|
||||
namespace ops
|
||||
postfix `.1`:(max+1) := pr1
|
||||
postfix `.2`:(max+1) := pr2
|
||||
abbreviation pr₁ := @pr1
|
||||
abbreviation pr₂ := @pr2
|
||||
end ops
|
||||
end sigma
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.types.sum
|
||||
Author: Leonardo de Moura, Jeremy Avigad
|
||||
-/
|
||||
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation
|
||||
|
||||
namespace sum
|
||||
notation A ⊎ B := sum A B
|
||||
notation A + B := sum A B
|
||||
namespace low_precedence_plus
|
||||
reserve infixr `+`:25 -- conflicts with notation for addition
|
||||
infixr `+` := sum
|
||||
end low_precedence_plus
|
||||
end sum
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
init.types
|
||||
==========
|
||||
|
||||
Some basic datatypes.
|
||||
|
||||
* [empty](empty.hlean)
|
||||
* [prod](prod.hlean)
|
||||
* [sigma](sigma.hlean)
|
||||
* [sum](sum.hlean)
|
||||
|
|
@ -2,14 +2,14 @@
|
|||
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.axioms.ua
|
||||
Module: init.ua
|
||||
Author: Jakob von Raumer
|
||||
|
||||
Ported from Coq HoTT
|
||||
-/
|
||||
|
||||
prelude
|
||||
import ..path ..equiv
|
||||
import .equiv
|
||||
open eq equiv is_equiv
|
||||
|
||||
--Ensure that the types compared are in the same universe
|
||||
Loading…
Reference in a new issue