From d1981ec0fa203f9fe1bd4fac0ba0157776199d18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 18:34:12 +0200 Subject: [PATCH] Update CHANGELOG and remove --allow-unsolved-metas pragma --- BACKLOG.md | 16 ++----------- CHANGELOG.md | 26 +++++++++++++++++++++ src/Cat/Categories/Sets.agda | 2 +- src/Cat/Category.agda | 2 +- src/Cat/Category/Monad.agda | 2 +- src/Cat/Category/Monad/Kleisli.agda | 2 +- src/Cat/Category/Monad/Monoidal.agda | 2 +- src/Cat/Category/Monad/Voevodsky.agda | 2 +- src/Cat/Category/NaturalTransformation.agda | 2 +- src/Cat/Category/Product.agda | 4 ++-- src/Cat/Category/Yoneda.agda | 2 +- src/Cat/Equivalence.agda | 2 +- 12 files changed, 39 insertions(+), 25 deletions(-) diff --git a/BACKLOG.md b/BACKLOG.md index 9a72a1d..af3f622 100644 --- a/BACKLOG.md +++ b/BACKLOG.md @@ -1,24 +1,12 @@ Backlog ======= -Prove postulates in `Cat.Wishlist`: - * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A` - -Prove that these two formulations of univalence are equivalent: - - ∀ A B → isEquiv (A ≡ B) (A ≅ B) (idToIso A B) - ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) - Prove univalence for the category of * functors and natural transformations -Prove: - * `isProp (Product ...)` - * `isProp (HasProducts ...)` +In AreInverses, dont use the "point-free" version. I.e.: -Rename composition in categories - -In stead of using AreInverses, just use a sigma-type + `∀ x → f x ≡ g x` rather than `f ≡ g` Ideas for future work --------------------- diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bd4bc4..6bb631b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,32 @@ Change log ========= +Version 1.5.0 +------------- +Prove postulates in `Cat.Wishlist`: + + * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A` + +Prove that these two formulations of univalence are equivalent: + + ∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) + ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + +Prove univalence for the category of... + + * the opposite category + * sets + * "pair" category + +Finish the proof that products are propositional: + + * `isProp (Product ...)` + * `isProp (HasProducts ...)` + +Remove --allow-unsolved-metas pragma from various files + +Also renamed a lot of different projections. E.g. arrow-composition, etc.. + Version 1.4.1 ------------- Defines a module to work with equivalence providing a way to go between diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 3fa14ce..e707b55 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,5 +1,5 @@ -- | The category of homotopy sets -{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} +{-# OPTIONS --cubical --caching #-} module Cat.Categories.Sets where open import Cat.Prelude as P diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 749ba42..274f94e 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -24,7 +24,7 @@ -- ------ -- -- Propositionality for all laws about the category. -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --cubical #-} module Cat.Category where diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index e071d92..8d5abc6 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -17,7 +17,7 @@ These two formulations are proven to be equivalent: The monoidal representation is exposed by default from this module. ---} -{-# OPTIONS --cubical --allow-unsolved-metas #-} +{-# OPTIONS --cubical #-} module Cat.Category.Monad where open import Cat.Prelude diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index 75e5a22..e0ebf86 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -1,7 +1,7 @@ {--- The Kleisli formulation of monads ---} -{-# OPTIONS --cubical --allow-unsolved-metas #-} +{-# OPTIONS --cubical #-} open import Agda.Primitive open import Cat.Prelude diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index 86111b6..f5b20ad 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -1,7 +1,7 @@ {--- Monoidal formulation of monads ---} -{-# OPTIONS --cubical --allow-unsolved-metas #-} +{-# OPTIONS --cubical #-} open import Agda.Primitive open import Cat.Prelude diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index e5ff355..abc8438 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -1,7 +1,7 @@ {- This module provides construction 2.3 in [voe] -} -{-# OPTIONS --cubical --allow-unsolved-metas --caching #-} +{-# OPTIONS --cubical --caching #-} module Cat.Category.Monad.Voevodsky where open import Cat.Prelude diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 1a7223d..3771643 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -17,7 +17,7 @@ -- Functions for manipulating the above: -- -- * A composition operator. -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --cubical #-} open import Cat.Prelude open import Data.Nat using (_≤′_ ; ≤′-refl ; ≤′-step) diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index c0c68c3..4856668 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} +{-# OPTIONS --cubical --caching #-} module Cat.Category.Product where open import Cat.Prelude as P hiding (_×_ ; fst ; snd) @@ -299,7 +299,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} open Σ ump renaming (fst to f') open Σ (snd ump) renaming (fst to f'-cond) 𝒻 : Arrow 𝒴 𝒳 - 𝒻 = f' , {!f'-cond!} + 𝒻 = f' , f'-cond contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f contractible ff@(f , f-cond) = res where diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index afea823..c02274b 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --cubical #-} module Cat.Category.Yoneda where diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 1103b9f..6e55cbf 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --cubical #-} module Cat.Equivalence where open import Cubical.Primitives