diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean index 790e039b92..05471610cd 100644 --- a/hott/algebra/binary.hlean +++ b/hott/algebra/binary.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014-15 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.binary Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 5d6e7a3c5f..c02c04885a 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.precategory.adjoint Authors: Floris van Doorn -/ diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index 7410834373..44e2a7c434 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.category Author: Jakob von Raumer -/ diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index 9c84e2eeb5..f73e1f35d0 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.comma Authors: Floris van Doorn, Jakob von Raumer Comma category diff --git a/hott/algebra/category/constructions/default.hlean b/hott/algebra/category/constructions/default.hlean index b1fbe62e0c..ec7444404d 100644 --- a/hott/algebra/category/constructions/default.hlean +++ b/hott/algebra/category/constructions/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.default Authors: Floris van Doorn -/ diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 7c91f85025..8aa783b236 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.functor Authors: Floris van Doorn, Jakob von Raumer Functor precategory and category diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean index 010d3094cf..02ba09558b 100644 --- a/hott/algebra/category/constructions/hset.hlean +++ b/hott/algebra/category/constructions/hset.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.hset Authors: Floris van Doorn, Jakob von Raumer Category of hsets diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index 4ea82d0a70..62ce724c13 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.opposite Authors: Floris van Doorn, Jakob von Raumer Opposite precategory and (TODO) category diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean index 4f31c68110..abd2792520 100644 --- a/hott/algebra/category/constructions/product.hlean +++ b/hott/algebra/category/constructions/product.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.constructions.product Authors: Floris van Doorn, Jakob von Raumer Functor product precategory and (TODO) category diff --git a/hott/algebra/category/default.hlean b/hott/algebra/category/default.hlean index 9db29ece48..6fdf85f8c0 100644 --- a/hott/algebra/category/default.hlean +++ b/hott/algebra/category/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.default Authors: Floris van Doorn -/ diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index ad9696a09d..ae6861c34e 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.functor Authors: Floris van Doorn, Jakob von Raumer -/ diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index aab77650a5..078111cf2d 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.groupoid Author: Jakob von Raumer Ported from Coq HoTT diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 1f6cd4329e..434960c976 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.iso Author: Floris van Doorn, Jakob von Raumer -/ diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 5c27b9aef8..4e6f685083 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.nat_trans Author: Floris van Doorn, Jakob von Raumer -/ import .functor .iso diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index b892b157d2..656e7cf6bc 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.precategory Authors: Floris van Doorn -/ import types.trunc types.pi arity diff --git a/hott/algebra/category/strict.hlean b/hott/algebra/category/strict.hlean index c12b9cf0a8..10941d3776 100644 --- a/hott/algebra/category/strict.hlean +++ b/hott/algebra/category/strict.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.strict Authors: Floris van Doorn, Jakob von Raumer -/ diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean index bdd31955a4..a5a433af30 100644 --- a/hott/algebra/category/yoneda.hlean +++ b/hott/algebra/category/yoneda.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.category.yoneda Authors: Floris van Doorn -/ diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean index 7c4049ef84..eeb5875524 100644 --- a/hott/algebra/field.hlean +++ b/hott/algebra/field.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Robert Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.field Authors: Robert Lewis Structures with multiplicative and additive components, including division rings and fields. diff --git a/hott/algebra/fundamental_group.hlean b/hott/algebra/fundamental_group.hlean index 1b488aec70..3bd297bbb3 100644 --- a/hott/algebra/fundamental_group.hlean +++ b/hott/algebra/fundamental_group.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.fundamental_group Authors: Floris van Doorn fundamental group of a pointed space diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index e714f4ebd9..e322cae60e 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.group Authors: Jeremy Avigad, Leonardo de Moura Various multiplicative and additive structures. diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 91758eaefb..d6b4f9f2a2 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.algebra.hott Author: Floris van Doorn Theorems about algebra specific to HoTT diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean index 242e5c0dd2..d9c2c2f133 100644 --- a/hott/algebra/order.hlean +++ b/hott/algebra/order.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.order Author: Jeremy Avigad Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean index db2f6a0277..696cca23a3 100644 --- a/hott/algebra/ordered_group.hlean +++ b/hott/algebra/ordered_group.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ordered_group Authors: Jeremy Avigad Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures, diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean index e9a24182de..4d5d36d6c9 100644 --- a/hott/algebra/ordered_ring.hlean +++ b/hott/algebra/ordered_ring.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ordered_ring Authors: Jeremy Avigad Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak diff --git a/hott/algebra/relation.hlean b/hott/algebra/relation.hlean index 95d4760615..dd0f133ff5 100644 --- a/hott/algebra/relation.hlean +++ b/hott/algebra/relation.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.relation Author: Jeremy Avigad General properties of relations, and classes for equivalence relations and congruences. diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index b087d45a6b..282be14867 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ring Authors: Jeremy Avigad, Leonardo de Moura Structures with multiplicative and additive components, including semirings, rings, and fields. diff --git a/hott/arity.hlean b/hott/arity.hlean index 3a133c4bcc..01f647dddf 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.path Author: Floris van Doorn Theorems about functions with multiple arguments diff --git a/hott/core.hlean b/hott/core.hlean index 3bdb9fbaa6..e62b6517ae 100644 --- a/hott/core.hlean +++ b/hott/core.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: core Authors: Floris van Doorn The core of the HoTT library diff --git a/hott/cubical/pathover.hlean b/hott/cubical/pathover.hlean index 396e07c8e6..fa6dc5da36 100644 --- a/hott/cubical/pathover.hlean +++ b/hott/cubical/pathover.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: cubical.pathover Author: Floris van Doorn Theorems about pathovers diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 0391c0d43a..6923a16f39 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: cubical.square Author: Floris van Doorn Theorems about square diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index cb410d007c..17827f0787 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.circle Authors: Floris van Doorn Declaration of the circle diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 691e582a78..819541e308 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.coeq Authors: Floris van Doorn Declaration of the coequalizer diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 24beda7ecd..c9cf1d2dd4 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.colimit Authors: Floris van Doorn Definition of general colimits and sequential colimits. diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index 5f6ec0801b..a1650aee11 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.cylinder Authors: Floris van Doorn Declaration of mapping cylinders diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 3b471acda2..dc95b64623 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.pushout Authors: Floris van Doorn Declaration of the pushout diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index a30b7148d5..75362e61f3 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.quotient Authors: Floris van Doorn Declaration of set-quotients diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean index a599c24cd4..3322a2bb13 100644 --- a/hott/hit/sphere.hlean +++ b/hott/hit/sphere.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.circle Authors: Floris van Doorn Declaration of the n-spheres diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean index 65dbe88e2b..f57b114596 100644 --- a/hott/hit/suspension.hlean +++ b/hott/hit/suspension.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.suspension Authors: Floris van Doorn Declaration of suspension diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 778582e61d..69493e5d22 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.trunc Authors: Floris van Doorn n-truncation of types. diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean index e685467df0..1931e64aaa 100644 --- a/hott/hit/type_quotient.hlean +++ b/hott/hit/type_quotient.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: hit.type_quotient Authors: Floris van Doorn Type quotients (quotient without truncation) diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean index 0d066cf6e1..0c19b95dea 100644 --- a/hott/init/bool.hlean +++ b/hott/init/bool.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.bool Authors: Leonardo de Moura -/ diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index 3c6576f3e2..ea43aa821b 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.datatypes Authors: Leonardo de Moura, Jakob von Raumer Basic datatypes diff --git a/hott/init/default.hlean b/hott/init/default.hlean index ff7d87919e..71a46b51a8 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.default Authors: Leonardo de Moura, Jakob von Raumer -/ diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index f1a6e105da..7884e74a56 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.equiv Author: Jeremy Avigad, Jakob von Raumer Ported from Coq HoTT diff --git a/hott/init/function.hlean b/hott/init/function.hlean index ba890470d8..6efc39338a 100644 --- a/hott/init/function.hlean +++ b/hott/init/function.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.function Author: Leonardo de Moura General operations on functions. diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 63b81869fa..b4efb3162d 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.funext Authors: Jakob von Raumer Ported from Coq HoTT diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index c9ffd5f44d..165f109ece 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.hit Authors: Floris van Doorn Declaration of the primitive hits in Lean diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 0a6da07c9c..0bf3234519 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.logic Authors: Leonardo de Moura -/ diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index b45770cd19..2f3f25be8f 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.nat Authors: Floris van Doorn, Leonardo de Moura -/ prelude diff --git a/hott/init/num.hlean b/hott/init/num.hlean index 9fad2b3397..5e67d8aa70 100644 --- a/hott/init/num.hlean +++ b/hott/init/num.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.num Authors: Leonardo de Moura -/ diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 4d10df5a7e..c553670ef7 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.path Authors: Jeremy Avigad, Jakob von Raumer, Floris van Doorn Ported from Coq HoTT diff --git a/hott/init/priority.hlean b/hott/init/priority.hlean index 01d5fcffdf..b6731949ad 100644 --- a/hott/init/priority.hlean +++ b/hott/init/priority.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.priority Authors: Leonardo de Moura -/ diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean index e68f545cbc..4cdeee4dfd 100644 --- a/hott/init/relation.hlean +++ b/hott/init/relation.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.relation Authors: Leonardo de Moura -/ diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index acbc6c5e3d..a08fae2631 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.reserved_notation Authors: Leonardo de Moura -/ prelude diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 7a7326c80e..7bc6461d31 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.tactic Author: Leonardo de Moura This is just a trick to embed the 'tactic language' as a Lean diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 8673d0b40a..2f5c1f0786 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.trunc Authors: Jeremy Avigad, Floris van Doorn Definition of is_trunc (n-truncatedness) diff --git a/hott/init/types.hlean b/hott/init/types.hlean index f51eb06a8a..260ab12120 100644 --- a/hott/init/types.hlean +++ b/hott/init/types.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.types Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer -/ diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index 571ec8b2ce..24a418c3ad 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.ua Author: Jakob von Raumer Ported from Coq HoTT diff --git a/hott/init/util.hlean b/hott/init/util.hlean index 650904a28d..4d5055af6b 100644 --- a/hott/init/util.hlean +++ b/hott/init/util.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.util Author: Leonardo de Moura Auxiliary definitions used by automation diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index 1e41258b6f..b5fc9cc712 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.wf Author: Leonardo de Moura -/ diff --git a/hott/types/W.hlean b/hott/types/W.hlean index 5dcdf3bdc1..63f8437c18 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.W Author: Floris van Doorn Theorems about W-types (well-founded trees) diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean index 86d5ceed23..076c899c8a 100644 --- a/hott/types/arrow.hlean +++ b/hott/types/arrow.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.arrow Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean index 8aca74c058..aca68997b9 100644 --- a/hott/types/bool.hlean +++ b/hott/types/bool.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.bool Authors: Floris van Doorn Theorems about the booleans diff --git a/hott/types/default.hlean b/hott/types/default.hlean index 48739ad73f..d15359b9ca 100644 --- a/hott/types/default.hlean +++ b/hott/types/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.default Authors: Floris van Doorn -/ diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 44b326e6e7..b4b0091b9a 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.eq Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 00d85f4baa..9dc5d1f558 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.equiv Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 930f1f4aee..1e9f27d3e8 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.fiber Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/function.hlean b/hott/types/function.hlean index b43b31cd62..1eb9e48554 100644 --- a/hott/types/function.hlean +++ b/hott/types/function.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.function Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean index 61baedd17b..1d0b3c8a45 100644 --- a/hott/types/hprop_trunc.hlean +++ b/hott/types/hprop_trunc.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.hprop_trunc Authors: Jakob von Raumer, Floris van Doorn Proof of the theorem that (is_trunc n A) is a mere proposition diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index 994d7c3a50..d4907c04c2 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.int.basic Authors: Floris van Doorn, Jeremy Avigad The integers, with addition, multiplication, and subtraction. The representation of the integers is diff --git a/hott/types/int/default.hlean b/hott/types/int/default.hlean index e6db52580c..f83a9b73f0 100644 --- a/hott/types/int/default.hlean +++ b/hott/types/int/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.int.default Authors: Floris van Doorn -/ diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 0ba73a4a5e..cd02efc2f4 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.int.hott Author: Floris van Doorn Theorems about the integers specific to HoTT diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index 81de282504..32dc4f0106 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.nat.basic (Ported from standard library file data.nat.basic on May 02, 2015) Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad diff --git a/hott/types/nat/default.hlean b/hott/types/nat/default.hlean index db02d9522e..a4f04a6cac 100644 --- a/hott/types/nat/default.hlean +++ b/hott/types/nat/default.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.nat.default Authors: Floris van Doorn -/ diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean index 0852c90b42..36e80ff03f 100644 --- a/hott/types/nat/order.hlean +++ b/hott/types/nat/order.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.nat.order Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad The order relation on the natural numbers. diff --git a/hott/types/nat/sub.hlean b/hott/types/nat/sub.hlean index 5d0246c13d..dff319ca99 100644 --- a/hott/types/nat/sub.hlean +++ b/hott/types/nat/sub.hlean @@ -3,8 +3,6 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Jeremy Avigad -Module: data.nat.sub - Subtraction on the natural numbers, as well as min, max, and distance. Ported from standard library diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 4bcc0500ee..43e601d4b9 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014-15 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.pi Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 7651d85c9c..214e92fda1 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.pointed Authors: Jakob von Raumer, Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 2bf48ac713..9b4a2699a7 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.prod Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 481cceab02..e753265662 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2014-15 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.sigma Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 99cdc78d29..5496e047a8 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: types.trunc Authors: Floris van Doorn Properties of is_trunc and trunctype