fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Clean-up names a bit

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-13 15:35:56 +02:00
parent b7c0fe64cf
commit 98b90f2370
3 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Cat/Categories/Sets.agda
View file

@ -129,7 +129,7 @@ module _ (ℓ : Level) where
univ≃ = step2 ⊙ univalence ⊙ step0 univ≃ = step2 ⊙ univalence ⊙ step0
univalent : Univalent univalent : Univalent
univalent = from[Andrea] (λ _ _ → univ≃) univalent = univalenceFrom≃ univ≃
SetsIsCategory : IsCategory SetsRaw SetsIsCategory : IsCategory SetsRaw
IsCategory.isPreCategory SetsIsCategory = isPreCat IsCategory.isPreCategory SetsIsCategory = isPreCat

28
src/Cat/Category.agda
View file

@ -130,25 +130,23 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
-- A perhaps more readable version of univalence: -- A perhaps more readable version of univalence:
Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B) Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
-- | Equivalent formulation of univalence. private
Univalent[Contr] : Set _ -- | Equivalent formulation of univalence.
Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) Univalent[Contr] : Set _
Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
Univalent[Andrea] : Set _ -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
Univalent[Andrea] = ∀ A B → (A ≡ B) ≃ (A ≅ B) -- Date: Wed, Mar 21, 2018 at 3:12 PM
--
-- This is not so straight-forward so you can assume it
postulate from[Contr] : Univalent[Contr] → Univalent
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se> univalenceFrom≃ : Univalent≃ → Univalent
-- Date: Wed, Mar 21, 2018 at 3:12 PM univalenceFrom≃ = from[Contr] ∘ step
--
-- This is not so straight-forward so you can assume it
postulate from[Contr] : Univalent[Contr] → Univalent
from[Andrea] : Univalent[Andrea] → Univalent
from[Andrea] = from[Contr] ∘ step
where where
module _ (f : Univalent[Andrea]) (A : Object) where module _ (f : Univalent≃) (A : Object) where
lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_) lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_)
lem = equivSig (f A) lem = equivSig λ _ → f
aux : isContr (Σ Object (A ≡_)) aux : isContr (Σ Object (A ≡_))
aux = (A , refl) , (λ y → contrSingl (snd y)) aux = (A , refl) , (λ y → contrSingl (snd y))

4
src/Cat/Category/Product.agda
View file

@ -171,7 +171,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
open IsPreCategory isPreCat open IsPreCategory isPreCat
module _ (𝕏 𝕐 : Object) where module _ {𝕏 𝕐 : Object} where
open Σ 𝕏 renaming (fst to X ; snd to x) open Σ 𝕏 renaming (fst to X ; snd to x)
open Σ x renaming (fst to xa ; snd to xb) open Σ x renaming (fst to xa ; snd to xb)
open Σ 𝕐 renaming (fst to Y ; snd to y) open Σ 𝕐 renaming (fst to Y ; snd to y)
@ -286,7 +286,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
equiv1 = _ , fromIso _ _ (snd iso) equiv1 = _ , fromIso _ _ (snd iso)
univalent : Univalent univalent : Univalent
univalent = from[Andrea] equiv1 univalent = univalenceFrom≃ equiv1
isCat : IsCategory raw isCat : IsCategory raw
IsCategory.isPreCategory isCat = isPreCat IsCategory.isPreCategory isCat = isPreCat