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