From 31eda5ac8170b2ac791451a5697f1722372395c4 Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 30 Jun 2022 18:53:55 +0200 Subject: [PATCH] move /misc to /agda, add KUIP and UIPK --- {misc => agda}/Agda.Builtin.Bool.html | 0 {misc => agda}/Agda.Builtin.Equality.html | 0 {misc => agda}/Agda.Builtin.Maybe.html | 0 {misc => agda}/Agda.Builtin.Nat.html | 0 {misc => agda}/Agda.Builtin.Sigma.html | 0 {misc => agda}/Agda.Builtin.Strict.html | 0 {misc => agda}/Agda.Builtin.Unit.html | 0 {misc => agda}/Agda.Primitive.html | 0 {misc => agda}/Agda.css | 0 {misc => agda}/Algebra.Bundles.html | 0 {misc => agda}/Algebra.Consequences.Base.html | 0 .../Algebra.Consequences.Setoid.html | 0 {misc => agda}/Algebra.Core.html | 0 {misc => agda}/Algebra.Definitions.html | 0 {misc => agda}/Algebra.Structures.html | 0 {misc => agda}/Algebra.html | 0 .../Axiom.Extensionality.Propositional.html | 0 .../Axiom.UniquenessOfIdentityProofs.html | 0 {misc => agda}/Data.Bool.Base.html | 0 {misc => agda}/Data.Empty.Irrelevant.html | 0 {misc => agda}/Data.Empty.html | 0 {misc => agda}/Data.Maybe.Base.html | 0 {misc => agda}/Data.Product.html | 0 {misc => agda}/Data.Sum.Base.html | 0 {misc => agda}/Data.These.Base.html | 0 {misc => agda}/Data.Unit.Base.html | 0 {misc => agda}/Function.Base.html | 0 {misc => agda}/Function.Bundles.html | 0 {misc => agda}/Function.Core.html | 0 .../Function.Definitions.Core1.html | 0 .../Function.Definitions.Core2.html | 0 {misc => agda}/Function.Definitions.html | 0 {misc => agda}/Function.Equality.html | 0 {misc => agda}/Function.Structures.html | 0 {misc => agda}/Function.html | 0 agda/KUIP.html | 10 +++++++++ {misc => agda}/Level.html | 0 {misc => agda}/Relation.Binary.Bundles.html | 0 .../Relation.Binary.Consequences.html | 0 {misc => agda}/Relation.Binary.Core.html | 0 .../Relation.Binary.Definitions.html | 0 ....Binary.Indexed.Heterogeneous.Bundles.html | 0 ...dexed.Heterogeneous.Construct.Trivial.html | 0 ...ion.Binary.Indexed.Heterogeneous.Core.html | 0 ...ary.Indexed.Heterogeneous.Definitions.html | 0 ...nary.Indexed.Heterogeneous.Structures.html | 0 ...Relation.Binary.Indexed.Heterogeneous.html | 0 ....Binary.PropositionalEquality.Algebra.html | 0 ...ion.Binary.PropositionalEquality.Core.html | 0 ...nary.PropositionalEquality.Properties.html | 0 ...Relation.Binary.PropositionalEquality.html | 0 ...Relation.Binary.Reasoning.Base.Single.html | 0 .../Relation.Binary.Reasoning.Setoid.html | 0 .../Relation.Binary.Structures.html | 0 {misc => agda}/Relation.Binary.html | 0 .../Relation.Nullary.Decidable.Core.html | 0 {misc => agda}/Relation.Nullary.Reflects.html | 0 {misc => agda}/Relation.Nullary.html | 0 {misc => agda}/Relation.Unary.html | 0 {misc => agda}/Strict.html | 0 agda/UIPK.html | 22 +++++++++++++++++++ {misc => agda}/llpo.html | 0 62 files changed, 32 insertions(+) rename {misc => agda}/Agda.Builtin.Bool.html (100%) rename {misc => agda}/Agda.Builtin.Equality.html (100%) rename {misc => agda}/Agda.Builtin.Maybe.html (100%) rename {misc => agda}/Agda.Builtin.Nat.html (100%) rename {misc => agda}/Agda.Builtin.Sigma.html (100%) rename {misc => agda}/Agda.Builtin.Strict.html (100%) rename {misc => agda}/Agda.Builtin.Unit.html (100%) rename {misc => agda}/Agda.Primitive.html (100%) rename {misc => agda}/Agda.css (100%) rename {misc => agda}/Algebra.Bundles.html (100%) rename {misc => agda}/Algebra.Consequences.Base.html (100%) rename {misc => agda}/Algebra.Consequences.Setoid.html (100%) rename {misc => agda}/Algebra.Core.html (100%) rename {misc => agda}/Algebra.Definitions.html (100%) rename {misc => agda}/Algebra.Structures.html (100%) rename {misc => agda}/Algebra.html (100%) rename {misc => agda}/Axiom.Extensionality.Propositional.html (100%) rename {misc => agda}/Axiom.UniquenessOfIdentityProofs.html (100%) rename {misc => agda}/Data.Bool.Base.html (100%) rename {misc => agda}/Data.Empty.Irrelevant.html (100%) rename {misc => agda}/Data.Empty.html (100%) rename {misc => agda}/Data.Maybe.Base.html (100%) rename {misc => agda}/Data.Product.html (100%) rename {misc => agda}/Data.Sum.Base.html (100%) rename {misc => agda}/Data.These.Base.html (100%) rename {misc => agda}/Data.Unit.Base.html (100%) rename {misc => agda}/Function.Base.html (100%) rename {misc => agda}/Function.Bundles.html (100%) rename {misc => agda}/Function.Core.html (100%) rename {misc => agda}/Function.Definitions.Core1.html (100%) rename {misc => agda}/Function.Definitions.Core2.html (100%) rename {misc => agda}/Function.Definitions.html (100%) rename {misc => agda}/Function.Equality.html (100%) rename {misc => agda}/Function.Structures.html (100%) rename {misc => agda}/Function.html (100%) create mode 100644 agda/KUIP.html rename {misc => agda}/Level.html (100%) rename {misc => agda}/Relation.Binary.Bundles.html (100%) rename {misc => agda}/Relation.Binary.Consequences.html (100%) rename {misc => agda}/Relation.Binary.Core.html (100%) rename {misc => agda}/Relation.Binary.Definitions.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.Bundles.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.Core.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.Definitions.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.Structures.html (100%) rename {misc => agda}/Relation.Binary.Indexed.Heterogeneous.html (100%) rename {misc => agda}/Relation.Binary.PropositionalEquality.Algebra.html (100%) rename {misc => agda}/Relation.Binary.PropositionalEquality.Core.html (100%) rename {misc => agda}/Relation.Binary.PropositionalEquality.Properties.html (100%) rename {misc => agda}/Relation.Binary.PropositionalEquality.html (100%) rename {misc => agda}/Relation.Binary.Reasoning.Base.Single.html (100%) rename {misc => agda}/Relation.Binary.Reasoning.Setoid.html (100%) rename {misc => agda}/Relation.Binary.Structures.html (100%) rename {misc => agda}/Relation.Binary.html (100%) rename {misc => agda}/Relation.Nullary.Decidable.Core.html (100%) rename {misc => agda}/Relation.Nullary.Reflects.html (100%) rename {misc => agda}/Relation.Nullary.html (100%) rename {misc => agda}/Relation.Unary.html (100%) rename {misc => agda}/Strict.html (100%) create mode 100644 agda/UIPK.html rename {misc => agda}/llpo.html (100%) diff --git a/misc/Agda.Builtin.Bool.html b/agda/Agda.Builtin.Bool.html similarity index 100% rename from misc/Agda.Builtin.Bool.html rename to agda/Agda.Builtin.Bool.html diff --git a/misc/Agda.Builtin.Equality.html b/agda/Agda.Builtin.Equality.html similarity index 100% rename from misc/Agda.Builtin.Equality.html rename to agda/Agda.Builtin.Equality.html diff --git a/misc/Agda.Builtin.Maybe.html b/agda/Agda.Builtin.Maybe.html similarity index 100% rename from misc/Agda.Builtin.Maybe.html rename to agda/Agda.Builtin.Maybe.html diff --git a/misc/Agda.Builtin.Nat.html b/agda/Agda.Builtin.Nat.html similarity index 100% rename from misc/Agda.Builtin.Nat.html rename to agda/Agda.Builtin.Nat.html diff --git a/misc/Agda.Builtin.Sigma.html b/agda/Agda.Builtin.Sigma.html similarity index 100% rename from misc/Agda.Builtin.Sigma.html rename to agda/Agda.Builtin.Sigma.html diff --git a/misc/Agda.Builtin.Strict.html b/agda/Agda.Builtin.Strict.html similarity index 100% rename from misc/Agda.Builtin.Strict.html rename to agda/Agda.Builtin.Strict.html diff --git a/misc/Agda.Builtin.Unit.html b/agda/Agda.Builtin.Unit.html similarity index 100% rename from misc/Agda.Builtin.Unit.html rename to agda/Agda.Builtin.Unit.html diff --git a/misc/Agda.Primitive.html b/agda/Agda.Primitive.html similarity index 100% rename from misc/Agda.Primitive.html rename to agda/Agda.Primitive.html diff --git a/misc/Agda.css b/agda/Agda.css similarity index 100% rename from misc/Agda.css rename to agda/Agda.css diff --git a/misc/Algebra.Bundles.html b/agda/Algebra.Bundles.html similarity index 100% rename from misc/Algebra.Bundles.html rename to agda/Algebra.Bundles.html diff --git a/misc/Algebra.Consequences.Base.html b/agda/Algebra.Consequences.Base.html similarity index 100% rename from misc/Algebra.Consequences.Base.html rename to agda/Algebra.Consequences.Base.html diff --git a/misc/Algebra.Consequences.Setoid.html b/agda/Algebra.Consequences.Setoid.html similarity index 100% rename from misc/Algebra.Consequences.Setoid.html rename to agda/Algebra.Consequences.Setoid.html diff --git a/misc/Algebra.Core.html b/agda/Algebra.Core.html similarity index 100% rename from misc/Algebra.Core.html rename to agda/Algebra.Core.html diff --git a/misc/Algebra.Definitions.html b/agda/Algebra.Definitions.html similarity index 100% rename from misc/Algebra.Definitions.html rename to agda/Algebra.Definitions.html diff --git a/misc/Algebra.Structures.html b/agda/Algebra.Structures.html similarity index 100% rename from misc/Algebra.Structures.html rename to agda/Algebra.Structures.html diff --git a/misc/Algebra.html b/agda/Algebra.html similarity index 100% rename from misc/Algebra.html rename to agda/Algebra.html diff --git a/misc/Axiom.Extensionality.Propositional.html b/agda/Axiom.Extensionality.Propositional.html similarity index 100% rename from misc/Axiom.Extensionality.Propositional.html rename to agda/Axiom.Extensionality.Propositional.html diff --git a/misc/Axiom.UniquenessOfIdentityProofs.html b/agda/Axiom.UniquenessOfIdentityProofs.html similarity index 100% rename from misc/Axiom.UniquenessOfIdentityProofs.html rename to agda/Axiom.UniquenessOfIdentityProofs.html diff --git a/misc/Data.Bool.Base.html b/agda/Data.Bool.Base.html similarity index 100% rename from misc/Data.Bool.Base.html rename to agda/Data.Bool.Base.html diff --git a/misc/Data.Empty.Irrelevant.html b/agda/Data.Empty.Irrelevant.html similarity index 100% rename from misc/Data.Empty.Irrelevant.html rename to agda/Data.Empty.Irrelevant.html diff --git a/misc/Data.Empty.html b/agda/Data.Empty.html similarity index 100% rename from misc/Data.Empty.html rename to agda/Data.Empty.html diff --git a/misc/Data.Maybe.Base.html b/agda/Data.Maybe.Base.html similarity index 100% rename from misc/Data.Maybe.Base.html rename to agda/Data.Maybe.Base.html diff --git a/misc/Data.Product.html b/agda/Data.Product.html similarity index 100% rename from misc/Data.Product.html rename to agda/Data.Product.html diff --git a/misc/Data.Sum.Base.html b/agda/Data.Sum.Base.html similarity index 100% rename from misc/Data.Sum.Base.html rename to agda/Data.Sum.Base.html diff --git a/misc/Data.These.Base.html b/agda/Data.These.Base.html similarity index 100% rename from misc/Data.These.Base.html rename to agda/Data.These.Base.html diff --git a/misc/Data.Unit.Base.html b/agda/Data.Unit.Base.html similarity index 100% rename from misc/Data.Unit.Base.html rename to agda/Data.Unit.Base.html diff --git a/misc/Function.Base.html b/agda/Function.Base.html similarity index 100% rename from misc/Function.Base.html rename to agda/Function.Base.html diff --git a/misc/Function.Bundles.html b/agda/Function.Bundles.html similarity index 100% rename from misc/Function.Bundles.html rename to agda/Function.Bundles.html diff --git a/misc/Function.Core.html b/agda/Function.Core.html similarity index 100% rename from misc/Function.Core.html rename to agda/Function.Core.html diff --git a/misc/Function.Definitions.Core1.html b/agda/Function.Definitions.Core1.html similarity index 100% rename from misc/Function.Definitions.Core1.html rename to agda/Function.Definitions.Core1.html diff --git a/misc/Function.Definitions.Core2.html b/agda/Function.Definitions.Core2.html similarity index 100% rename from misc/Function.Definitions.Core2.html rename to agda/Function.Definitions.Core2.html diff --git a/misc/Function.Definitions.html b/agda/Function.Definitions.html similarity index 100% rename from misc/Function.Definitions.html rename to agda/Function.Definitions.html diff --git a/misc/Function.Equality.html b/agda/Function.Equality.html similarity index 100% rename from misc/Function.Equality.html rename to agda/Function.Equality.html diff --git a/misc/Function.Structures.html b/agda/Function.Structures.html similarity index 100% rename from misc/Function.Structures.html rename to agda/Function.Structures.html diff --git a/misc/Function.html b/agda/Function.html similarity index 100% rename from misc/Function.html rename to agda/Function.html diff --git a/agda/KUIP.html b/agda/KUIP.html new file mode 100644 index 0000000..f6ed9e3 --- /dev/null +++ b/agda/KUIP.html @@ -0,0 +1,10 @@ + +KUIP
{-# OPTIONS --safe #-}
+module KUIP where
+
+open import Agda.Primitive renaming (Set to 𝒰)
+open import Agda.Builtin.Equality
+
+UIP : ∀ {ₙ} {A : 𝒰 ₙ} {x y : A} (p q : x ≡ y) → p ≡ q
+UIP refl refl = refl
+
\ No newline at end of file diff --git a/misc/Level.html b/agda/Level.html similarity index 100% rename from misc/Level.html rename to agda/Level.html diff --git a/misc/Relation.Binary.Bundles.html b/agda/Relation.Binary.Bundles.html similarity index 100% rename from misc/Relation.Binary.Bundles.html rename to agda/Relation.Binary.Bundles.html diff --git a/misc/Relation.Binary.Consequences.html b/agda/Relation.Binary.Consequences.html similarity index 100% rename from misc/Relation.Binary.Consequences.html rename to agda/Relation.Binary.Consequences.html diff --git a/misc/Relation.Binary.Core.html b/agda/Relation.Binary.Core.html similarity index 100% rename from misc/Relation.Binary.Core.html rename to agda/Relation.Binary.Core.html diff --git a/misc/Relation.Binary.Definitions.html b/agda/Relation.Binary.Definitions.html similarity index 100% rename from misc/Relation.Binary.Definitions.html rename to agda/Relation.Binary.Definitions.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html b/agda/Relation.Binary.Indexed.Heterogeneous.Bundles.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html rename to agda/Relation.Binary.Indexed.Heterogeneous.Bundles.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html b/agda/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html rename to agda/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Core.html b/agda/Relation.Binary.Indexed.Heterogeneous.Core.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.Core.html rename to agda/Relation.Binary.Indexed.Heterogeneous.Core.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html b/agda/Relation.Binary.Indexed.Heterogeneous.Definitions.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html rename to agda/Relation.Binary.Indexed.Heterogeneous.Definitions.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Structures.html b/agda/Relation.Binary.Indexed.Heterogeneous.Structures.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.Structures.html rename to agda/Relation.Binary.Indexed.Heterogeneous.Structures.html diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.html b/agda/Relation.Binary.Indexed.Heterogeneous.html similarity index 100% rename from misc/Relation.Binary.Indexed.Heterogeneous.html rename to agda/Relation.Binary.Indexed.Heterogeneous.html diff --git a/misc/Relation.Binary.PropositionalEquality.Algebra.html b/agda/Relation.Binary.PropositionalEquality.Algebra.html similarity index 100% rename from misc/Relation.Binary.PropositionalEquality.Algebra.html rename to agda/Relation.Binary.PropositionalEquality.Algebra.html diff --git a/misc/Relation.Binary.PropositionalEquality.Core.html b/agda/Relation.Binary.PropositionalEquality.Core.html similarity index 100% rename from misc/Relation.Binary.PropositionalEquality.Core.html rename to agda/Relation.Binary.PropositionalEquality.Core.html diff --git a/misc/Relation.Binary.PropositionalEquality.Properties.html b/agda/Relation.Binary.PropositionalEquality.Properties.html similarity index 100% rename from misc/Relation.Binary.PropositionalEquality.Properties.html rename to agda/Relation.Binary.PropositionalEquality.Properties.html diff --git a/misc/Relation.Binary.PropositionalEquality.html b/agda/Relation.Binary.PropositionalEquality.html similarity index 100% rename from misc/Relation.Binary.PropositionalEquality.html rename to agda/Relation.Binary.PropositionalEquality.html diff --git a/misc/Relation.Binary.Reasoning.Base.Single.html b/agda/Relation.Binary.Reasoning.Base.Single.html similarity index 100% rename from misc/Relation.Binary.Reasoning.Base.Single.html rename to agda/Relation.Binary.Reasoning.Base.Single.html diff --git a/misc/Relation.Binary.Reasoning.Setoid.html b/agda/Relation.Binary.Reasoning.Setoid.html similarity index 100% rename from misc/Relation.Binary.Reasoning.Setoid.html rename to agda/Relation.Binary.Reasoning.Setoid.html diff --git a/misc/Relation.Binary.Structures.html b/agda/Relation.Binary.Structures.html similarity index 100% rename from misc/Relation.Binary.Structures.html rename to agda/Relation.Binary.Structures.html diff --git a/misc/Relation.Binary.html b/agda/Relation.Binary.html similarity index 100% rename from misc/Relation.Binary.html rename to agda/Relation.Binary.html diff --git a/misc/Relation.Nullary.Decidable.Core.html b/agda/Relation.Nullary.Decidable.Core.html similarity index 100% rename from misc/Relation.Nullary.Decidable.Core.html rename to agda/Relation.Nullary.Decidable.Core.html diff --git a/misc/Relation.Nullary.Reflects.html b/agda/Relation.Nullary.Reflects.html similarity index 100% rename from misc/Relation.Nullary.Reflects.html rename to agda/Relation.Nullary.Reflects.html diff --git a/misc/Relation.Nullary.html b/agda/Relation.Nullary.html similarity index 100% rename from misc/Relation.Nullary.html rename to agda/Relation.Nullary.html diff --git a/misc/Relation.Unary.html b/agda/Relation.Unary.html similarity index 100% rename from misc/Relation.Unary.html rename to agda/Relation.Unary.html diff --git a/misc/Strict.html b/agda/Strict.html similarity index 100% rename from misc/Strict.html rename to agda/Strict.html diff --git a/agda/UIPK.html b/agda/UIPK.html new file mode 100644 index 0000000..da014a7 --- /dev/null +++ b/agda/UIPK.html @@ -0,0 +1,22 @@ + +UIPK
{-# OPTIONS --safe --without-K #-}
+open import Agda.Primitive renaming (Set to 𝒰)
+open import Agda.Builtin.Equality
+
+module UIPK (UIP : ∀ {ₙ} {A : 𝒰 ₙ} {x y : A} (p q : x ≡ y) → p ≡ q)
+            where
+
+J : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x y : A} (P : (a b : A) → a ≡ b → 𝒰 ₘ) → P x x refl → (p : x ≡ y) → P x y p
+J _ Prefl refl = Prefl
+
+square : ∀ {ₙ} {A : 𝒰 ₙ} {x y z w : A} → x ≡ z → y ≡ w → x ≡ y → z ≡ w
+square refl refl p = p
+
+transp : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x y : A} (P : A → 𝒰 ₘ) → x ≡ y → P x → P y
+transp P refl Px = Px
+
+K : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x : A} (P : x ≡ x → 𝒰 ₘ) → P refl → (p : x ≡ x) → P p
+K {x = x} P Prefl p = (J (λ a b q → (r : a ≡ x) → (s : b ≡ x) → P (square r s q))
+                         (λ a b → transp P (UIP refl (square a b refl)) Prefl)
+                         p) refl refl
+
\ No newline at end of file diff --git a/misc/llpo.html b/agda/llpo.html similarity index 100% rename from misc/llpo.html rename to agda/llpo.html