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

Merge branch 'dev'

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-16 12:04:29 +01:00
parent 4df4231906 7dc7a5aee3
commit b8994b8f4a
8 changed files with 128 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
libs/agda-stdlib

@ -1 +1 @@
Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6
Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68

2
libs/cubical

@ -1 +1 @@
Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48
Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151

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

@ -44,7 +44,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-- ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
-- ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
module _ {A B : Object ℂ} where
isSet : IsSet (Path A B)
isSet : Cubical.isSet (Path A B)
isSet = {!!}
RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
RawFree = record

52
src/Cat/Categories/Fun.agda
View file

@ -1,13 +1,23 @@
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Categories.Fun where
open import Agda.Primitive
open import Cubical
open import Function
open import Data.Product
import Cubical.GradLemma
module UIP = Cubical.GradLemma
open import Cubical.Sigma
open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
module Nat = Data.Nat
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Wishlist
open import Cat.Equality
open Equality.Data.Product
module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
open Category hiding ( _∘_ ; Arrow )
@ -27,6 +37,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
-- naturalIsProp : ∀ θ → isProp (Natural θ)
-- naturalIsProp θ x y = {!funExt!}
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
@ -86,12 +99,39 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
NatComp = _:⊕:_
private
module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B}
{g : NaturalTransformation B C} {h : NaturalTransformation C D} where
module _ {F G : Functor ℂ 𝔻} where
module 𝔻 = IsCategory (isCategory 𝔻)
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j
IsSet' : {ℓ : Level} (A : Set ℓ) → Set ℓ
IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
λ θ → ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)
module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
private
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {D}
:assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
:assoc: = {!!}
:assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
:assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
where
open IsCategory (isCategory 𝔻)
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
ident-r = {!!}
@ -116,7 +156,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
:isCategory: = record
{ assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
; ident = λ {A B} → :ident: {A} {B}
; arrowIsSet = {!!}
; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
; univalent = {!!}
}

50
src/Cat/Category.agda
View file

@ -11,8 +11,8 @@ open import Data.Product renaming
)
open import Data.Empty
import Function
open import Cubical hiding (isSet)
open import Cubical.GradLemma using ( propIsEquiv )
open import Cubical
open import Cubical.NType.Properties using ( propIsEquiv )
∃! : ∀ {a b} {A : Set a}
→ (A → Set b) → Set (a ⊔ b)
@ -23,8 +23,9 @@ open import Cubical.GradLemma using ( propIsEquiv )
syntax ∃!-syntax (λ x → B) = ∃![ x ] B
IsSet : {ℓ : Level} (A : Set ℓ) → Set ℓ
IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q
-- This follows from [HoTT-book: §7.1.10]
-- Andrea says the proof is in `cubical` but I can't find it.
postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-- adding no-eta-equality can speed up type-checking.
@ -53,12 +54,13 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-- (univalent).
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
open RawCategory ℂ
module Raw = RawCategory ℂ
field
assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
→ h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
ident : {A B : Object} {f : Arrow A B}
→ f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
arrowIsSet : ∀ {A B : Object} → IsSet (Arrow A B)
arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
@ -91,22 +93,40 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
-- This lemma will be useful to prove the equality of two categories.
IsCategory-is-prop : isProp (IsCategory ℂ)
IsCategory-is-prop x y i = record
{ assoc = x.arrowIsSet x.assoc y.assoc i
-- Why choose `x`'s `arrowIsSet`?
{ assoc = x.arrowIsSet _ _ x.assoc y.assoc i
; ident =
( x.arrowIsSet (fst x.ident) (fst y.ident) i
, x.arrowIsSet (snd x.ident) (snd y.ident) i
( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
, x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
)
; arrowIsSet = λ p q →
let
golden : x.arrowIsSet p q ≡ y.arrowIsSet p q
golden = {!!}
in
golden i
; univalent = λ y₁ → {!!}
; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
; univalent = {!!}
}
where
module x = IsCategory x
module y = IsCategory y
xuni : x.Univalent
xuni = x.univalent
yuni : y.Univalent
yuni = y.univalent
open RawCategory ℂ
T : I → Set (ℓa ⊔ ℓb)
T i = {A B : Object} →
isEquiv (A ≡ B) (A x.≅ B)
(λ A≡B →
transp
(λ j →
Σ-syntax (Arrow A (A≡B j))
(λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
( 𝟙
, 𝟙
, x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
, x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
)
)
eqUni : T [ xuni ≡ yuni ]
eqUni = {!!}
record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
field

27
src/Cat/Category/Functor.agda
View file

@ -1,3 +1,4 @@
{-# OPTIONS --cubical #-}
module Cat.Category.Functor where
open import Agda.Primitive
@ -60,14 +61,14 @@ module _
IsFunctorIsProp : isProp (IsFunctor _ _ F)
IsFunctorIsProp isF0 isF1 i = record
{ ident = 𝔻.arrowIsSet isF0.ident isF1.ident i
; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i
{ ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
}
where
module isF0 = IsFunctor isF0
module isF1 = IsFunctor isF1
-- Alternate version of above where `F` is a path in
-- Alternate version of above where `F` is indexed by an interval
module _
{ℓa ℓb : Level}
{ℂ 𝔻 : Category ℓa ℓb}
@ -78,14 +79,11 @@ module _
IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
-- IsFunctorIsProp' isF0 isF1 i = record
-- { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!}
-- ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!}
-- }
-- where
-- module isF0 = IsFunctor isF0
-- module isF1 = IsFunctor isF1
IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
(\ F → IsFunctorIsProp {F = F}) (\ i → F i)
where
open import Cubical.NType.Properties using (lemPropF)
module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
Functor≡ : {F G : Functor ℂ 𝔻}
@ -95,14 +93,13 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
→ F ≡ G
Functor≡ {F} {G} eq* eq→ i = record
{ raw = eqR i
; isFunctor = f i
; isFunctor = eqIsF i
}
where
eqR : raw F ≡ raw G
eqR i = record { func* = eq* i ; func→ = eq→ i }
postulate T : isSet (IsFunctor _ _ (raw F))
f : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
f = IsFunctorIsProp' (isFunctor F) (isFunctor G)
eqIsF : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
private

26
src/Cat/Equality.agda
View file

@ -1,3 +1,4 @@
{-# OPTIONS --cubical #-}
-- Defines equality-principles for data-types from the standard library.
module Cat.Equality where
@ -19,3 +20,28 @@ module Equality where
Σ≡ : a ≡ b
proj₁ (Σ≡ i) = proj₁≡ i
proj₂ (Σ≡ i) = proj₂≡ i
-- Remark 2.7.1: This theorem:
--
-- (x , u) ≡ (x , v) → u ≡ v
--
-- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
-- such that
--
-- p* u ≡ v
-- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
-- thm sA sB (x , y) (x' , y') p q = res
-- where
-- x≡x'0 : x ≡ x'
-- x≡x'0 = λ i → proj₁ (p i)
-- x≡x'1 : x ≡ x'
-- x≡x'1 = λ i → proj₁ (q i)
-- someP : x ≡ x'
-- someP = {!!}
-- tricky : {!y!} ≡ y'
-- tricky = {!!}
-- -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
-- res' : ({!!} , {!!}) ≡ ({!!} , {!!})
-- res' = {!!}
-- res : p ≡ q
-- res i = {!res'!}

6
src/Cat/Wishlist.agda Normal file
View file

@ -0,0 +1,6 @@
module Cat.Wishlist where
open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A