Organize modules
This commit is contained in:
parent
37cb8e0541
commit
32244c912a
|
|
@ -1,8 +1,7 @@
|
|||
name: cat
|
||||
include:
|
||||
src
|
||||
--libs/cubical-demo
|
||||
-- description:
|
||||
-- A formalization of category theory in Agda using cubical type theory.
|
||||
depend:
|
||||
agda-prelude
|
||||
standard-library
|
||||
--cubical-demo
|
||||
cubical
|
||||
include: src
|
||||
|
|
|
|||
150
src/Cat.agda
150
src/Cat.agda
|
|
@ -1,150 +0,0 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
module Cat where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Prelude.Function
|
||||
open import PathPrelude
|
||||
open ≡-Reasoning
|
||||
|
||||
-- Questions:
|
||||
--
|
||||
-- Is there a canonical `postulate trustme : {l : Level} {A : Set l} -> A`
|
||||
-- in Agda (like undefined in Haskell).
|
||||
--
|
||||
-- Does Agda have a way to specify local submodules?
|
||||
--
|
||||
-- Can I open parts of a record, like say:
|
||||
--
|
||||
-- open Functor {{...}} ( fmap )
|
||||
|
||||
record Functor {a b} (F : Set a → Set b) : Set (lsuc a ⊔ b) where
|
||||
field
|
||||
-- morphisms
|
||||
fmap : ∀ {A B} → (A → B) → F A → F B
|
||||
-- laws
|
||||
identity : { A : Set a }
|
||||
-> id ≡ fmap (id { A = A })
|
||||
fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B )
|
||||
-> fmap f ∘ fmap g ≡ fmap (f ∘ g)
|
||||
|
||||
open Functor {{ ... }} hiding ( identity )
|
||||
|
||||
_<$>_ : {a b : Level} {F : Set a → Set b} {{r : Functor F}} {A B : Set a} → (A → B) → F A → F B
|
||||
_<$>_ = fmap
|
||||
|
||||
record Identity (A : Set) : Set where
|
||||
constructor identity
|
||||
field
|
||||
runIdentity : A
|
||||
|
||||
open Identity {{...}}
|
||||
|
||||
instance
|
||||
IdentityFunctor : Functor Identity
|
||||
IdentityFunctor = record
|
||||
{ fmap = λ { f (identity a) -> identity (f a) }
|
||||
; identity = refl
|
||||
; fusion = λ { f g -> refl }
|
||||
}
|
||||
|
||||
data Maybe ( A : Set ) : Set where
|
||||
nothing : Maybe A
|
||||
just : A -> Maybe A
|
||||
|
||||
instance
|
||||
MaybeFunctor : Functor Maybe
|
||||
Functor.fmap MaybeFunctor f nothing = nothing
|
||||
Functor.fmap MaybeFunctor f (just x) = just (f x)
|
||||
Functor.identity MaybeFunctor = fun-ext (λ { nothing → refl ; (just x) → refl })
|
||||
Functor.fusion MaybeFunctor f g = fun-ext (λ
|
||||
-- QUESTION: Why does inlining `lem₀` give rise to an error?
|
||||
{ nothing → lem₀
|
||||
; (just x) → {! refl!}
|
||||
{- ; (just x) → begin
|
||||
(fmap f ∘ fmap g) (just x) ≡⟨⟩
|
||||
(fmap f (fmap g (just x))) ≡⟨⟩
|
||||
(fmap f (just (g x))) ≡⟨⟩
|
||||
(just (f (g x))) ≡⟨⟩
|
||||
just ((f ∘ g) x) ∎-}
|
||||
})
|
||||
where
|
||||
lem₀ : nothing ≡ nothing
|
||||
lem₀ = refl
|
||||
-- `lem₁` and `fusionjust` are the same.
|
||||
lem₁ : {A B C : Set} {f : B → C} {g : A → B} {x : A}
|
||||
→ just (f (g x)) ≡ just (f (g x))
|
||||
lem₁ = refl
|
||||
fusionjust : { A B C : Set } { x : A } { f : B -> C } { g : A -> B }
|
||||
-> (fmap f ∘ fmap g) (just x) ≡ just ((f ∘ g) x)
|
||||
fusionjust {x = x} {f = f} {g = g} = begin
|
||||
(fmap f ∘ fmap g) (just x) ≡⟨⟩
|
||||
(fmap f (fmap g (just x))) ≡⟨⟩
|
||||
(fmap f (just (g x))) ≡⟨⟩
|
||||
(just (f (g x))) ≡⟨⟩
|
||||
just ((f ∘ g) x) ∎
|
||||
|
||||
|
||||
record Applicative {a} (F : Set a -> Set a) : Set (lsuc a) where
|
||||
field
|
||||
-- morphisms
|
||||
pure : { A : Set a } -> A -> F A
|
||||
ap : { A B : Set a } -> F (A -> B) -> F A -> F B
|
||||
-- laws
|
||||
-- `ap-identity` is paraphrased from the documentation for Applicative on hackage.
|
||||
ap-identity : { A : Set a } -> ap (pure (id { A = A })) ≡ id
|
||||
composition : { A B C : Set a } ( u : F (B -> C) ) ( v : F (A -> B) ) ( w : F A )
|
||||
-> ap (ap (ap (pure _∘′_) u) v) w ≡ ap u (ap v w)
|
||||
homomorphism : { A B : Set a } { a : A } { f : A -> B }
|
||||
-> ap (pure f) (pure a) ≡ pure (f a)
|
||||
interchange : { A B : Set a } ( u : F (A -> B) ) ( a : A )
|
||||
-> ap u (pure a) ≡ ap (pure (_$ a)) u
|
||||
|
||||
open Applicative {{...}}
|
||||
_<*>_ = ap
|
||||
|
||||
instance
|
||||
IdentityApplicative : Applicative Identity
|
||||
Applicative.pure IdentityApplicative = identity
|
||||
Applicative.ap IdentityApplicative (identity f) (identity a) = identity (f a)
|
||||
Applicative.ap-identity IdentityApplicative = refl
|
||||
Applicative.composition IdentityApplicative _ _ _ = refl
|
||||
Applicative.homomorphism IdentityApplicative = refl
|
||||
Applicative.interchange IdentityApplicative _ _ = refl
|
||||
|
||||
-- QUESTION: Is this provable? How?
|
||||
-- I suppose this would be `≡`'s functor-instance.
|
||||
equiv-app : {A B : Set} -> {f g : A -> B} -> {a : A} -> f ≡ g -> f a ≡ g a
|
||||
equiv-app f≡g = {!!}
|
||||
|
||||
instance
|
||||
MaybeApplicative : Applicative Maybe
|
||||
Applicative.pure MaybeApplicative = just
|
||||
Applicative.ap MaybeApplicative nothing _ = nothing
|
||||
Applicative.ap MaybeApplicative (just f) x = fmap f x
|
||||
-- QUESTION: Why does termination-check fail when I use `refl` in both cases below?
|
||||
Applicative.ap-identity MaybeApplicative = fun-ext (λ
|
||||
{ nothing → {!refl!}
|
||||
; (just x) → {!refl!}
|
||||
})
|
||||
Applicative.composition MaybeApplicative nothing v w = refl
|
||||
Applicative.composition MaybeApplicative (just x) nothing w = refl
|
||||
-- Easy-mode:
|
||||
-- Applicative.composition MaybeApplicative {u = just f} {just g} {nothing} = refl
|
||||
-- Applicative.composition MaybeApplicative {u = just f} {just g} {just x} = refl
|
||||
-- Re-use mode:
|
||||
-- QUESTION: What's wrong here?
|
||||
Applicative.composition MaybeApplicative (just f) (just g) w = sym (equiv-app lem)
|
||||
where
|
||||
lem : ∀ {A B C} {f : B → C} {g : A → B} {w : Maybe A} →
|
||||
(fmap f) ∘ (fmap g) ≡
|
||||
(Functor.fmap MaybeFunctor (f ∘ g))
|
||||
lem = Functor.fusion MaybeFunctor _ _
|
||||
{-
|
||||
Applicative.composition MaybeApplicative { u = u } { v = v } { w = w } = begin
|
||||
ap (ap (ap (pure _∘′_) u) v) w ≡⟨⟩
|
||||
ap (ap (fmap _∘′_ u) v) w ≡⟨ {!!} ⟩
|
||||
{!!} ∎
|
||||
-}
|
||||
Applicative.homomorphism MaybeApplicative = refl
|
||||
Applicative.interchange MaybeApplicative nothing a = refl
|
||||
Applicative.interchange MaybeApplicative (just x) a = refl
|
||||
|
|
@ -0,0 +1,196 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Category where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Data.Unit.Base
|
||||
open import Data.Product
|
||||
open import Cubical.PathPrelude
|
||||
|
||||
postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
|
||||
|
||||
record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
|
||||
field
|
||||
Object : Set ℓ
|
||||
Arrow : Object → Object → Set ℓ'
|
||||
𝟙 : {o : Object} → Arrow o o
|
||||
_⊕_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c
|
||||
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
|
||||
infixl 45 _⊕_
|
||||
dom : { a b : Object } → Arrow a b → Object
|
||||
dom {a = a} _ = a
|
||||
cod : { a b : Object } → Arrow a b → Object
|
||||
cod {b = b} _ = b
|
||||
|
||||
open Category public
|
||||
|
||||
record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
|
||||
: Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
|
||||
private
|
||||
open module C = Category C
|
||||
open module D = Category D
|
||||
field
|
||||
F : C.Object → D.Object
|
||||
f : {c c' : C.Object} → C.Arrow c c' → D.Arrow (F c) (F c')
|
||||
ident : { c : C.Object } → f (C.𝟙 {c}) ≡ D.𝟙 {F c}
|
||||
-- TODO: Avoid use of ugly explicit arguments somehow.
|
||||
-- This guy managed to do it:
|
||||
-- https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
|
||||
distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
|
||||
→ f (a' C.⊕ a) ≡ f a' D.⊕ f a
|
||||
|
||||
FunctorComp : ∀ {ℓ ℓ'} {a b c : Category {ℓ} {ℓ'}} → Functor b c → Functor a b → Functor a c
|
||||
FunctorComp {a = a} {b = b} {c = c} F G =
|
||||
record
|
||||
{ F = F.F ∘ G.F
|
||||
; f = F.f ∘ G.f
|
||||
; ident = λ { {c = obj} →
|
||||
let --t : (F.f ∘ G.f) (𝟙 a) ≡ (𝟙 c)
|
||||
g-ident = G.ident
|
||||
k : F.f (G.f {c' = obj} (𝟙 a)) ≡ F.f (G.f (𝟙 a))
|
||||
k = refl {x = F.f (G.f (𝟙 a))}
|
||||
t : F.f (G.f (𝟙 a)) ≡ (𝟙 c)
|
||||
-- t = subst F.ident (subst G.ident k)
|
||||
t = undefined
|
||||
in t }
|
||||
; distrib = undefined -- subst F.distrib (subst G.distrib refl)
|
||||
}
|
||||
where
|
||||
open module F = Functor F
|
||||
open module G = Functor G
|
||||
|
||||
-- The identity functor
|
||||
Identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
|
||||
Identity = record { F = λ x → x ; f = λ x → x ; ident = refl ; distrib = refl }
|
||||
|
||||
module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where
|
||||
private
|
||||
open module ℂ = Category ℂ
|
||||
_+_ = ℂ._⊕_
|
||||
|
||||
Isomorphism : (f : ℂ.Arrow A B) → Set ℓ'
|
||||
Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g + f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙
|
||||
|
||||
Epimorphism : {X : ℂ.Object } → (f : ℂ.Arrow A B) → Set ℓ'
|
||||
Epimorphism {X} f = ( g₀ g₁ : ℂ.Arrow B X ) → g₀ + f ≡ g₁ + f → g₀ ≡ g₁
|
||||
|
||||
Monomorphism : {X : ℂ.Object} → (f : ℂ.Arrow A B) → Set ℓ'
|
||||
Monomorphism {X} f = ( g₀ g₁ : ℂ.Arrow X A ) → f + g₀ ≡ f + g₁ → g₀ ≡ g₁
|
||||
|
||||
iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f
|
||||
-- Idea: Pre-compose with f- on both sides of the equality of eq to get
|
||||
-- g₀ + f + f- ≡ g₁ + f + f-
|
||||
-- which by left-inv reduces to the goal.
|
||||
iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
|
||||
trans (sym (fst ℂ.ident))
|
||||
( trans (cong (_+_ g₀) (sym right-inv))
|
||||
( trans ℂ.assoc
|
||||
( trans (cong (λ x → x + f-) eq)
|
||||
( trans (sym ℂ.assoc)
|
||||
( trans (cong (_+_ g₁) right-inv) (fst ℂ.ident))
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f
|
||||
-- For the next goal we do something similar: Post-compose with f- and use
|
||||
-- right-inv to get the goal.
|
||||
iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
|
||||
trans (sym (snd ℂ.ident))
|
||||
( trans (cong (λ x → x + g₀) (sym left-inv))
|
||||
( trans (sym ℂ.assoc)
|
||||
( trans (cong (_+_ f-) eq)
|
||||
( trans ℂ.assoc
|
||||
( trans (cong (λ x → x + g₁) left-inv) (snd ℂ.ident)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
|
||||
iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
|
||||
|
||||
data ⊥ : Set where
|
||||
|
||||
¬_ : {ℓ : Level} → Set ℓ → Set ℓ
|
||||
¬ A = A → ⊥
|
||||
|
||||
{-
|
||||
epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
|
||||
epi-mono-is-not-iso f =
|
||||
let k = f {!!} {!!} {!!} {!!}
|
||||
in {!!}
|
||||
-}
|
||||
|
||||
_≅_ : { ℓ ℓ' : Level } → { ℂ : Category {ℓ} {ℓ'} } → ( A B : Object ℂ ) → Set ℓ'
|
||||
_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
|
||||
where
|
||||
open module ℂ = Category ℂ
|
||||
|
||||
Product : {ℓ : Level} → ( C D : Category {ℓ} {ℓ} ) → Category {ℓ} {ℓ}
|
||||
Product C D =
|
||||
record
|
||||
{ Object = C.Object × D.Object
|
||||
; Arrow = λ { (c , d) (c' , d') →
|
||||
let carr = C.Arrow c c'
|
||||
darr = D.Arrow d d'
|
||||
in carr × darr}
|
||||
; 𝟙 = C.𝟙 , D.𝟙
|
||||
; _⊕_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → bc∈C C.⊕ ab∈C , bc∈D D.⊕ ab∈D}
|
||||
; assoc = eqpair C.assoc D.assoc
|
||||
; ident =
|
||||
let (Cl , Cr) = C.ident
|
||||
(Dl , Dr) = D.ident
|
||||
in eqpair Cl Dl , eqpair Cr Dr
|
||||
}
|
||||
where
|
||||
open module C = Category C
|
||||
open module D = Category D
|
||||
-- Two pairs are equal if their components are equal.
|
||||
eqpair : {ℓ : Level} → { A : Set ℓ } → { B : Set ℓ } → { a a' : A } → { b b' : B } → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
|
||||
eqpair {a = a} {b = b} eqa eqb = subst eqa (subst eqb (refl {x = (a , b)}))
|
||||
|
||||
Opposite : ∀ {ℓ ℓ'} → Category {ℓ} {ℓ'} → Category {ℓ} {ℓ'}
|
||||
Opposite ℂ =
|
||||
record
|
||||
{ Object = ℂ.Object
|
||||
; Arrow = λ A B → ℂ.Arrow B A
|
||||
; 𝟙 = ℂ.𝟙
|
||||
; _⊕_ = λ g f → f ℂ.⊕ g
|
||||
; assoc = sym ℂ.assoc
|
||||
; ident = swap ℂ.ident
|
||||
}
|
||||
where
|
||||
open module ℂ = Category ℂ
|
||||
|
||||
CatCat : {ℓ ℓ' : Level} → Category {ℓ-suc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
|
||||
CatCat {ℓ} {ℓ'} =
|
||||
record
|
||||
{ Object = Category {ℓ} {ℓ'}
|
||||
; Arrow = Functor
|
||||
; 𝟙 = Identity
|
||||
; _⊕_ = FunctorComp
|
||||
; assoc = undefined
|
||||
; ident = λ { {f = f} →
|
||||
let eq : f ≡ f
|
||||
eq = refl
|
||||
in undefined , undefined}
|
||||
}
|
||||
|
||||
Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ'
|
||||
Hom {ℂ = ℂ} A B = Arrow ℂ A B
|
||||
|
||||
module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
|
||||
private
|
||||
Obj = Object ℂ
|
||||
Arr = Arrow ℂ
|
||||
_+_ = _⊕_ ℂ
|
||||
|
||||
HomFromArrow : (A : Obj) → {B B' : Obj} → (g : Arr B B')
|
||||
→ Hom {ℂ = ℂ} A B → Hom {ℂ = ℂ} A B'
|
||||
HomFromArrow _A g = λ f → g + f
|
||||
|
|
@ -0,0 +1,43 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
open import Cubical.PathPrelude hiding ( Id )
|
||||
|
||||
module _ {A : Set} {a : A} {P : A → Set} where
|
||||
Q : A → Set
|
||||
Q a = A
|
||||
|
||||
t : Σ[ a ∈ A ] P a → Q a
|
||||
t (a , Pa) = a
|
||||
u : Q a → Σ[ a ∈ A ] P a
|
||||
u a = a , {!!}
|
||||
|
||||
tu-bij : (a : Q a) → (t ∘ u) a ≡ a
|
||||
tu-bij a = refl
|
||||
|
||||
v : P a → Q a
|
||||
v x = {!!}
|
||||
w : Q a → P a
|
||||
w x = {!!}
|
||||
|
||||
vw-bij : (a : P a) → (w ∘ v) a ≡ a
|
||||
vw-bij a = refl
|
||||
-- tubij a with (t ∘ u) a
|
||||
-- ... | q = {!!}
|
||||
|
||||
data Id {A : Set} (a : A) : Set where
|
||||
id : A → Id a
|
||||
|
||||
data Id' {A : Set} (a : A) : Set where
|
||||
id' : A → Id' a
|
||||
|
||||
T U : Set
|
||||
T = Id a
|
||||
U = Id' a
|
||||
|
||||
f : T → U
|
||||
f (id x) = id' x
|
||||
g : U → T
|
||||
g (id' x) = id x
|
||||
|
||||
fg-bij : (x : U) → (f ∘ g) x ≡ x
|
||||
fg-bij (id' x) = {!!}
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
module Category.Free where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.PathPrelude hiding (Path)
|
||||
|
||||
open import Category as C
|
||||
|
||||
module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
|
||||
private
|
||||
open module ℂ = Category ℂ
|
||||
Obj = ℂ.Object
|
||||
|
||||
Path : ( a b : Obj ) → Set
|
||||
Path a b = undefined
|
||||
|
||||
postulate emptyPath : (o : Obj) → Path o o
|
||||
|
||||
postulate concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
|
||||
|
||||
private
|
||||
module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where
|
||||
postulate
|
||||
p-assoc : concatenate {A} {C} {D} p (concatenate {A} {B} {C} q r)
|
||||
≡ concatenate {A} {B} {D} (concatenate {B} {C} {D} p q) r
|
||||
module _ {A B : Obj} {p : Path A B} where
|
||||
postulate
|
||||
ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
|
||||
ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
|
||||
|
||||
Free : Category
|
||||
Free = record
|
||||
{ Object = Obj
|
||||
; Arrow = Path
|
||||
; 𝟙 = λ {o} → emptyPath o
|
||||
; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
|
||||
; assoc = p-assoc
|
||||
; ident = ident-r , ident-l
|
||||
}
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Category.Pathy where
|
||||
|
||||
open import Cubical.PathPrelude
|
||||
|
||||
{-
|
||||
module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
|
||||
(P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
|
||||
pathJ' : (y : A) → (p : x ≡ y) → P y p
|
||||
pathJ' _ p = transp (λ i → uncurry P (contrSingl p i)) d
|
||||
|
||||
pathJprop' : pathJ' _ refl ≡ d
|
||||
pathJprop' i
|
||||
= primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d
|
||||
|
||||
|
||||
module _ {ℓ ℓ'} {A : Set ℓ}
|
||||
(P : (x y : A) → x ≡ y → Set ℓ') (d : (x : A) → P x x refl) where
|
||||
pathJ'' : (x y : A) → (p : x ≡ y) → P x y p
|
||||
pathJ'' _ _ p = transp (λ i →
|
||||
let
|
||||
P' = uncurry P
|
||||
q = (contrSingl p i)
|
||||
in
|
||||
{!uncurry (uncurry P)!} ) d
|
||||
-}
|
||||
|
||||
module _ {ℓ ℓ'} {A : Set ℓ}
|
||||
(C : (x y : A) → x ≡ y → Set ℓ')
|
||||
(c : (x : A) → C x x refl) where
|
||||
|
||||
=-ind : (x y : A) → (p : x ≡ y) → C x y p
|
||||
=-ind x y p = pathJ (C x) (c x) y p
|
||||
|
||||
module _ {ℓ ℓ' : Level} {A : Set ℓ} {P : A → Set ℓ} {x y : A} where
|
||||
private
|
||||
D : (x y : A) → (x ≡ y) → Set ℓ
|
||||
D x y p = P x → P y
|
||||
|
||||
id : {ℓ : Level} → {A : Set ℓ} → A → A
|
||||
id x = x
|
||||
|
||||
d : (x : A) → D x x refl
|
||||
d x = id {A = P x}
|
||||
|
||||
-- the p refers to the third argument
|
||||
liftP : x ≡ y → P x → P y
|
||||
liftP p = =-ind D d x y p
|
||||
|
||||
-- lift' : (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , liftP p u)
|
||||
-- lift' u p = {!!}
|
||||
|
|
@ -0,0 +1,159 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
module Category.Rel where
|
||||
|
||||
open import Data.Product
|
||||
open import Cubical.PathPrelude
|
||||
open import Cubical.GradLemma
|
||||
open import Agda.Primitive
|
||||
open import Category
|
||||
|
||||
-- Sets are built-in to Agda. The set of all small sets is called Set.
|
||||
|
||||
Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
|
||||
Fun T U = T → U
|
||||
|
||||
𝕊et-as-Cat : {ℓ : Level} → Category {lsuc ℓ} {ℓ}
|
||||
𝕊et-as-Cat {ℓ} = record
|
||||
{ Object = Set ℓ
|
||||
; Arrow = λ T U → Fun {ℓ} T U
|
||||
; 𝟙 = λ x → x
|
||||
; _⊕_ = λ g f x → g ( f x )
|
||||
; assoc = refl
|
||||
; ident = funExt (λ x → refl) , funExt (λ x → refl)
|
||||
}
|
||||
|
||||
-- Subsets are predicates over some type.
|
||||
Subset : {ℓ : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc lzero)
|
||||
Subset A = A → Set
|
||||
-- Subset : {ℓ ℓ' : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc ℓ')
|
||||
-- Subset {ℓ' = ℓ'} A = A → Set ℓ'
|
||||
-- {a ∈ A | P a}
|
||||
|
||||
-- subset-syntax : {ℓ ℓ' : Level} → (A : Set ℓ) → (P : A → Set ℓ') → ( a : A ) → Set ℓ'
|
||||
-- subset-syntax A P a = P a
|
||||
-- infix 2 subset-syntax
|
||||
|
||||
-- syntax subset P a = << a ∈ A >>>
|
||||
-- syntax subset P = ⦃ a ∈ A | P a ⦄
|
||||
-- syntax subset-syntax A (λ a → B) = ⟨ a foo A ∣ B ⟩
|
||||
|
||||
-- Membership is function applicatiom.
|
||||
_∈_ : {ℓ : Level} {A : Set ℓ} → A → Subset A → Set
|
||||
s ∈ S = S s
|
||||
|
||||
infixl 45 _∈_
|
||||
|
||||
-- The diagnoal of a set is a synonym for equality.
|
||||
Diag : ∀ S → Subset (S × S)
|
||||
Diag S (s₀ , s₁) = s₀ ≡ s₁
|
||||
-- Diag S = subset (S × S) (λ {(p , q) → p ≡ q})
|
||||
-- Diag S = ⟨ ? foo ? ∣ ? ⟩
|
||||
-- Diag S (s₀ , s₁) = ⦃ (s₀ , s₁) ∈ S | s₀ ≡ s₁ ⦄
|
||||
|
||||
module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
|
||||
private
|
||||
a : A
|
||||
a = fst ab
|
||||
b : B
|
||||
b = snd ab
|
||||
|
||||
module _ where
|
||||
private
|
||||
forwards : ((a , b) ∈ S)
|
||||
→ (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
forwards ab∈S = a , (refl , ab∈S)
|
||||
|
||||
backwards : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
→ (a , b) ∈ S
|
||||
backwards (a' , (a=a' , a'b∈S)) = subst (sym a=a') a'b∈S
|
||||
|
||||
isbijective : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x
|
||||
-- isbijective x = pathJ (λ y x₁ → (backwards ∘ forwards) x ≡ x) {!!} {!!} {!!}
|
||||
isbijective x = pathJprop (λ y _ → y) x
|
||||
|
||||
postulate
|
||||
back-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
→ (forwards ∘ backwards) x ≡ x
|
||||
-- back-fwd (a , (p , ab∈S))
|
||||
-- = =-ind (λ x y p → {!(forwards ∘ backwards) x ≡ x!}) {!!} {!!} {!!} p
|
||||
-- = pathJprop (λ y _ → snd (snd y)) ab∈S
|
||||
-- has type P x refl where P is the first argument
|
||||
{-
|
||||
|
||||
module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
|
||||
(P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
|
||||
pathJ : (y : A) → (p : x ≡ y) → P y p
|
||||
pathJ _ p = transp (λ i → uncurry P (contrSingl p i)) d
|
||||
|
||||
pathJprop : pathJ _ refl ≡ d
|
||||
pathJprop i = primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d
|
||||
-}
|
||||
isequiv : isEquiv
|
||||
(Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
((a , b) ∈ S)
|
||||
backwards
|
||||
-- isequiv ab∈S = (forwards ab∈S , sym (isbijective ab∈S)) , λ y → fiberhelp y
|
||||
isequiv y = gradLemma backwards forwards isbijective back-fwd y
|
||||
|
||||
equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
≃ (a , b) ∈ S
|
||||
equi = backwards , isequiv
|
||||
|
||||
ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
|
||||
≡ (a , b) ∈ S
|
||||
ident-l = equivToPath equi
|
||||
|
||||
module _ where
|
||||
private
|
||||
forwards : ((a , b) ∈ S)
|
||||
→ (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
forwards proof = b , (proof , refl)
|
||||
|
||||
backwards : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
→ (a , b) ∈ S
|
||||
backwards (b' , (ab'∈S , b'=b)) = subst b'=b ab'∈S
|
||||
|
||||
isbijective : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x
|
||||
isbijective x = pathJprop (λ y _ → y) x
|
||||
|
||||
fwd-bwd : (x : Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
→ (forwards ∘ backwards) x ≡ x
|
||||
fwd-bwd (b , (ab∈S , refl)) = pathJprop (λ y _ → fst (snd y)) ab∈S
|
||||
|
||||
isequiv : isEquiv
|
||||
(Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
((a , b) ∈ S)
|
||||
backwards
|
||||
isequiv ab∈S = gradLemma backwards forwards isbijective fwd-bwd ab∈S
|
||||
|
||||
equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
≃ ab ∈ S
|
||||
equi = backwards , isequiv
|
||||
|
||||
ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
|
||||
≡ ab ∈ S
|
||||
ident-r = equivToPath equi
|
||||
|
||||
Rel-as-Cat : Category
|
||||
Rel-as-Cat = record
|
||||
{ Object = Set
|
||||
; Arrow = λ S R → Subset (S × R)
|
||||
; 𝟙 = λ {S} → Diag S
|
||||
; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
|
||||
; assoc = {!!}
|
||||
; ident = funExt ident-l , funExt ident-r
|
||||
}
|
||||
|
||||
module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where
|
||||
private
|
||||
C-Obj = Object ℂ
|
||||
_+_ = Arrow ℂ
|
||||
|
||||
RepFunctor : Functor ℂ 𝕊et-as-Cat
|
||||
RepFunctor =
|
||||
record
|
||||
{ F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B
|
||||
; f = λ { {c' = c'} f g → HomFromArrow {ℂ = {!𝕊et-as-Cat!}} c' g}
|
||||
; ident = {!!}
|
||||
; distrib = {!!}
|
||||
}
|
||||
|
|
@ -1,293 +0,0 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
module PathPrelude where
|
||||
|
||||
open import Primitives public
|
||||
open import Level
|
||||
open import Data.Product using (Σ; _,_) renaming (proj₁ to fst; proj₂ to snd)
|
||||
|
||||
refl : ∀ {a} {A : Set a} {x : A} → Path x x
|
||||
refl {x = x} = λ i → x
|
||||
|
||||
sym : ∀ {a} {A : Set a} → {x y : A} → Path x y → Path y x
|
||||
sym p = \ i → p (~ i)
|
||||
|
||||
pathJ : ∀ {a}{p}{A : Set a}{x : A}(P : ∀ y → Path x y → Set p) → P x ((\ i -> x)) → ∀ y (p : Path x y) → P y p
|
||||
pathJ P d _ p = primComp (λ i → P (p i) (\ j → p (i ∧ j))) i0 (\ _ → empty) d
|
||||
|
||||
|
||||
pathJprop : ∀ {a}{p}{A : Set a}{x : A}(P : ∀ y → Path x y → Set p) → (d : P x ((\ i -> x))) → pathJ P d _ refl ≡ d
|
||||
pathJprop {x = x} P d i = primComp (λ _ → P x refl) i (\ { j (i = i1) → d }) d
|
||||
|
||||
|
||||
trans : ∀ {a} {A : Set a} → {x y z : A} → Path x y → Path y z → Path x z
|
||||
trans {A = A} {x} {y} p q = \ i → primComp (λ j → A) (i ∨ ~ i)
|
||||
(\ j → \ { (i = i1) → q j
|
||||
; (i = i0) → x
|
||||
}
|
||||
)
|
||||
(p i)
|
||||
|
||||
fun-ext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x}
|
||||
→ (∀ x → Path (f x) (g x)) → Path f g
|
||||
fun-ext p = λ i x → p x i
|
||||
|
||||
|
||||
-- comp using only Path
|
||||
compP : ∀ {a : Level} {A0 A1 : Set a} (A : Path A0 A1) → {φ : I} → (a0 : A i0) → (Partial (Σ A1 \ y → PathP (\ i → A i) a0 y) φ) → A i1
|
||||
compP A {φ} a0 p = primComp (λ i → A i) φ (\ i o → p o .snd i) a0
|
||||
|
||||
-- fill using only Path
|
||||
|
||||
fillP : ∀ {a : Level} {A0 A1 : Set a} (A : Path A0 A1) → {φ : I} → (a0 : A i0) → (Partial (Σ A1 \ y → PathP (\ i → A i) a0 y) φ) → ∀ i → A i
|
||||
fillP A {φ} a0 p j = primComp (λ i → A (i ∧ j)) (φ ∨ ~ j) (\ { i (φ = i1) → p itIsOne .snd (i ∧ j); i (j = i0) → a0 }) a0
|
||||
|
||||
|
||||
reflId : ∀ {a} {A : Set a}{x : A} → Id x x
|
||||
reflId {x = x} = conid i1 (λ _ → x)
|
||||
|
||||
Jdef : ∀ {a}{p}{A : Set a}{x : A}(P : ∀ y → Id x y → Set p) → (d : P x reflId) → J P d reflId ≡ d
|
||||
Jdef P d = refl
|
||||
|
||||
fromPath : ∀ {A : Set}{x y : A} → Path x y -> Id x y
|
||||
fromPath p = conid i0 (\ i → p i)
|
||||
|
||||
transId : ∀ {a} {A : Set a} → {x y z : A} → Id x y → Id y z → Id x z
|
||||
transId {A = A} {x} {y} p = J (λ y _ → Id x y) p
|
||||
|
||||
congId : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → ∀ {x y} → Id x y → Id (f x) (f y)
|
||||
congId f {x} {y} = J (λ y _ → Id (f x) (f y)) reflId
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
fill : ∀ {a : I -> Level} (A : (i : I) → Set (a i)) (φ : I) → ((i : I) → Partial (A i) φ) → A i0 → (i : I) → A i
|
||||
fill A φ u a0 i = unsafeComp (\ j → A (i ∧ j)) (φ ∨ ~ i) (\ j → unsafePOr φ (~ i) (u (i ∧ j)) \ { _ → a0 }) a0
|
||||
|
||||
singl : ∀ {l} {A : Set l} (a : A) -> Set l
|
||||
singl {A = A} a = Σ A (\ x → a ≡ x)
|
||||
|
||||
contrSingl : ∀ {l} {A : Set l} {a b : A} (p : a ≡ b) → Path {A = singl a} (a , refl) (b , p)
|
||||
contrSingl p = \ i → ((p i) , \ j → p (i ∧ j))
|
||||
|
||||
|
||||
module Contr where
|
||||
|
||||
isContr : ∀ {a} → (A : Set a) → Set a
|
||||
isContr A = Σ A (\ x → ∀ y → x ≡ y)
|
||||
|
||||
contr : ∀ {a} {A : Set a} → isContr A → (φ : I) → (u : Partial A φ) → A
|
||||
contr {A = A} (c , p) φ u = primComp (\ _ → A) φ (λ i → \ o → p (u o) i) c
|
||||
|
||||
lemma : ∀ {a} {A : Set a}
|
||||
→ (contr1 : ∀ φ → Partial A φ → A)
|
||||
→ (contr2 : ∀ u → u ≡ (contr1 i1 \{_ → u}))
|
||||
→ isContr A
|
||||
lemma {A = A} contr1 contr2 = x , (λ y → let module M = R y in trans (contr2 x) (trans (\ i → M.v i) (sym (contr2 y)))) where
|
||||
x = contr1 i0 empty
|
||||
module R (y : A) (i : I) where
|
||||
φ = ~ i ∨ i
|
||||
u : Partial A φ
|
||||
u = primPOr (~ i) i (\{_ → x}) (\{_ → y})
|
||||
v = contr1 φ u
|
||||
|
||||
isContrProp : ∀ {a} {A : Set a} (h : isContr A) -> ∀ (x y : A) → x ≡ y
|
||||
isContrProp {A = A} h a b = \ i → primComp (\ _ → A) _ (\ j → [ (~ i) ↦ (\{_ → snd h a j}) , i ↦ (\{_ → snd h b j}) ]) (fst h)
|
||||
|
||||
module Pres {la lb : I → _} {T : (i : I) → Set (lb i)}{A : (i : I) → Set (la i)} (f : ∀ i → T i → A i) (φ : I) (t : ∀ i → Partial (T i) φ)
|
||||
(t0 : T i0 {- [ φ ↦ t i0 ] -}) where
|
||||
|
||||
c1 c2 : A i1
|
||||
c1 = unsafeComp A φ (λ i → (\{_ → f i (t i itIsOne) })) (f i0 t0)
|
||||
c2 = f i1 (unsafeComp T φ t t0)
|
||||
|
||||
a0 = f i0 t0
|
||||
|
||||
a : ∀ i → Partial (A i) φ
|
||||
a i = (\{_ → f i ((t i) itIsOne) })
|
||||
|
||||
u : ∀ i → A i
|
||||
u = fill A φ a a0
|
||||
|
||||
v : ∀ i → T i
|
||||
v = fill T φ t t0
|
||||
|
||||
pres : Path c1 c2
|
||||
pres = \ j → unsafeComp A (φ ∨ (j ∨ ~ j)) (λ i → primPOr φ ((j ∨ ~ j)) (a i) (primPOr j (~ j) (\{_ → f i (v i) }) (\{_ → u i }))) a0
|
||||
|
||||
module Equiv {l l'} (A : Set l)(B : Set l') where
|
||||
isEquiv : (A -> B) → Set (l' ⊔ l)
|
||||
isEquiv f = ∀ y → Contr.isContr (Σ A \ x → y ≡ f x)
|
||||
|
||||
Equiv = Σ _ isEquiv
|
||||
|
||||
equiv : (f : Equiv) → ∀ φ (t : Partial A φ) (a : B {- [ φ ↦ f t ] -}) → PartialP φ (\ o → Path a (fst f (t o)))
|
||||
-> Σ A \ x → a ≡ fst f x -- [ φ ↦ (t , \ j → a) ]
|
||||
equiv (f , [f]) φ t a p = Contr.contr ([f] a) φ \ o → t o , (\ i → p o i)
|
||||
|
||||
equiv1 : (f : Equiv) → ∀ φ (t : Partial A φ) (a : B {- [ φ ↦ f t ] -}) → PartialP φ (\ o → Path a (fst f (t o))) -> A
|
||||
equiv1 f φ t a p = fst (equiv f φ t a p)
|
||||
|
||||
equiv2 : (f : Equiv) → ∀ φ (t : Partial A φ) (a : B {- [ φ ↦ f t ] -}) → (p : PartialP φ (\ o → Path a (fst f (t o))))
|
||||
→ a ≡ fst f (equiv1 f φ t a p)
|
||||
equiv2 f φ t a p = snd (equiv f φ t a p)
|
||||
|
||||
open Equiv public
|
||||
|
||||
{-# BUILTIN ISEQUIV isEquiv #-}
|
||||
|
||||
idEquiv : ∀ {a} {A : Set a} → Equiv A A
|
||||
idEquiv = (λ x → x) , (λ y → (y , refl) , (λ y₁ → contrSingl (snd y₁)))
|
||||
|
||||
|
||||
pathToEquiv : ∀ {l : I → _} (E : (i : I) → Set (l i)) → Equiv (E i0) (E i1)
|
||||
pathToEquiv E = f
|
||||
, (λ y → (g y
|
||||
, (\ j → primComp E (~ j ∨ j) (\ i → [ ~ j ↦ (\{_ → v i y }) , j ↦ (\{_ → u i (g y) }) ]) (g y))) ,
|
||||
prop-f-image y _ )
|
||||
where
|
||||
A = E i0
|
||||
B = E i1
|
||||
transp : ∀ {l : I → _} (E : (i : I) → Set (l i)) → E i0 → E i1
|
||||
transp E x = primComp E i0 (\ _ → empty) x
|
||||
f : A → B
|
||||
f = transp E
|
||||
g : B → A
|
||||
g = transp (\ i → E (~ i))
|
||||
u : (i : I) → A → E i
|
||||
u i x = fill E i0 (\ _ → empty) x i
|
||||
v : (i : I) → B → E i
|
||||
v i y = fill (\ i → E (~ i)) i0 (\ _ → empty) y (~ i)
|
||||
prop-f-image : (y : B) → (a b : Σ _ \ x → y ≡ f x) → a ≡ b
|
||||
prop-f-image y (x0 , b0) (x1 , b1) = \ k → (w k) , (\ j → d j k)
|
||||
where
|
||||
w0 = \ (j : I) → primComp (\ i → E (~ i)) (~ j ∨ j) ((\ i → [ ~ j ↦ (\{_ → v (~ i) y }) , j ↦ (\{_ → u (~ i) x0 }) ])) (b0 j)
|
||||
w1 = \ (j : I) → primComp (\ i → E (~ i)) (~ j ∨ j) ((\ i → [ ~ j ↦ (\{_ → v (~ i) y }) , j ↦ (\{_ → u (~ i) x1 }) ])) (b1 j)
|
||||
t0 = \ (j : I) → fill (\ i → E (~ i)) (~ j ∨ j) ((\ i → [ ~ j ↦ (\{_ → v (~ i) y }) , j ↦ (\{_ → u (~ i) x0 }) ])) (b0 j)
|
||||
t1 = \ (j : I) → fill (\ i → E (~ i)) (~ j ∨ j) ((\ i → [ ~ j ↦ (\{_ → v (~ i) y }) , j ↦ (\{_ → u (~ i) x1 }) ])) (b1 j)
|
||||
w = \ (k : I) → primComp (λ _ → A) (~ k ∨ k) (\ j → [ ~ k ↦ (\{_ → w0 j }) , k ↦ (\{_ → w1 j }) ]) (g y)
|
||||
t = \ (j k : I) → fill (λ _ → A) (~ k ∨ k) (\ j → [ ~ k ↦ (\{_ → w0 j }) , k ↦ (\{_ → w1 j }) ]) (g y) j
|
||||
d = \ (j k : I) → primComp E ((~ k ∨ k) ∨ (~ j ∨ j)) ((\ i → [ ~ k ∨ k ↦ [ ~ k ↦ (\{_ → t0 j (~ i) }) , k ↦ (\{_ → t1 j (~ i) }) ]
|
||||
, ~ j ∨ j ↦ [ ~ j ↦ (\{_ → v (i) y }) , j ↦ (\{_ → u (i) (w k) }) ] ])) (t j k)
|
||||
|
||||
pathToEquiv2 : ∀ {l : I → _} (E : (i : I) → Set (l i)) → _
|
||||
pathToEquiv2 {l} E = snd (pathToEquiv E)
|
||||
|
||||
{-# BUILTIN PATHTOEQUIV pathToEquiv2 #-}
|
||||
|
||||
module GluePrims where
|
||||
primitive
|
||||
primGlue : ∀ {a b} (A : Set a) → ∀ φ → (T : Partial (Set b) φ) → (f : PartialP φ (λ o → T o → A))
|
||||
→ (pf : PartialP φ (λ o → isEquiv (T o) A (f o))) → Set b
|
||||
prim^glue : ∀ {a b} {A : Set a} {φ : I} {T : Partial (Set b) φ}
|
||||
{f : PartialP φ (λ o → T o → A)}
|
||||
{pf : PartialP φ (λ o → isEquiv (T o) A (f o))} →
|
||||
PartialP φ T → A → primGlue A φ T f pf
|
||||
prim^unglue : ∀ {a b} {A : Set a} {φ : I} {T : Partial (Set b) φ}
|
||||
{f : PartialP φ (λ o → T o → A)}
|
||||
{pf : PartialP φ (λ o → isEquiv (T o) A (f o))} →
|
||||
primGlue A φ T f pf → A
|
||||
|
||||
|
||||
module GluePrims' (dummy : Set₁) = GluePrims
|
||||
open GluePrims' Set using () renaming (prim^glue to unsafeGlue) public
|
||||
|
||||
open GluePrims public renaming (prim^glue to glue; prim^unglue to unglue)
|
||||
|
||||
Glue : ∀ {a b} (A : Set a) → ∀ φ → (T : Partial (Set b) φ) (f : (PartialP φ \ o → Equiv (T o) A)) → Set _
|
||||
Glue A φ T f = primGlue A φ T (\ o → fst (f o)) (\ o → snd (f o))
|
||||
|
||||
eqToPath' : ∀ {l} {A B : Set l} → Equiv A B → Path A B
|
||||
eqToPath' {l} {A} {B} f = \ i → Glue B (~ i ∨ i) ([ ~ i ↦ (\ _ → A) , i ↦ (\ _ → B) ]) ([ ~ i ↦ (\{_ → f }) , i ↦ (\{_ → idEquiv }) ])
|
||||
|
||||
primitive
|
||||
primFaceForall : (I → I) → I
|
||||
|
||||
module FR (φ : I -> I) where
|
||||
δ = primFaceForall φ
|
||||
postulate
|
||||
∀e : IsOne δ → ∀ i → IsOne (φ i)
|
||||
∀∨ : ∀ i → IsOne (φ i) → IsOne ((δ ∨ (φ i0 ∧ ~ i)) ∨ (φ i1 ∧ i))
|
||||
|
||||
module GlueIso {a b} {A : Set a} {φ : I} {T : Partial (Set b) φ} {f : (PartialP φ \ o → Equiv (T o) A)} where
|
||||
going : PartialP φ (\ o → Glue A φ T f → T o)
|
||||
going = (\{_ → (\ x → x) })
|
||||
back : PartialP φ (\ o → T o → Glue A φ T f)
|
||||
back = (\{_ → (\ x → x) })
|
||||
|
||||
lemma : ∀ (b : PartialP φ (\ _ → Glue A φ T f)) → PartialP φ \ o → Path (unglue {φ = φ} (b o)) (fst (f o) (going o (b o)))
|
||||
lemma b = (\{_ → refl })
|
||||
|
||||
module CompGlue {la lb : I → _} (A : (i : I) → Set (la i)) (φ : I -> I) (T : ∀ i → Partial (Set (lb i)) (φ i))
|
||||
(f : ∀ i → PartialP (φ i) \ o → Equiv (T i o) (A i)) where
|
||||
B : (i : I) -> Set (lb i)
|
||||
B = \ i → Glue (A i) (φ i) (T i) (f i)
|
||||
module Local (ψ : I) (b : ∀ i → Partial (B i) ψ) (b0 : B i0 {- [ ψ ↦ b i0 ] -}) where
|
||||
a : ∀ i → Partial (A i) ψ
|
||||
a i = \ o → unglue {φ = φ i} (b i o)
|
||||
module Forall (δ : I) (∀e : IsOne δ → ∀ i → IsOne (φ i)) where
|
||||
a0 : A i0
|
||||
a0 = unglue {φ = φ i0} b0
|
||||
a₁' = unsafeComp A ψ a a0
|
||||
t₁' : PartialP δ (\ o → T i1 (∀e o i1))
|
||||
t₁' = \ o → unsafeComp (λ i → T i (∀e o i)) ψ (\ i o' → GlueIso.going {φ = φ i} (∀e o i) (b i o')) (GlueIso.going {φ = φ i0} (∀e o i0) b0)
|
||||
w : PartialP δ _
|
||||
w = \ o → Pres.pres (\ i → fst (f i (∀e o i))) ψ (λ i x → GlueIso.going {φ = φ i} (∀e o i) (b i x)) (GlueIso.going {φ = φ i0} (∀e o i0) b0)
|
||||
a₁'' = unsafeComp (\ _ → A i1) (δ ∨ ψ) (\ j → unsafePOr δ ψ (\ o → w o j) (a i1)) a₁'
|
||||
g : PartialP (φ i1) _
|
||||
g o = (equiv (T i1 _) (A i1) (f i1 o) (δ ∨ ψ) (unsafePOr δ ψ t₁' (\ o' → GlueIso.going {φ = φ i1} o (b i1 o'))) a₁''
|
||||
( (unsafePOr δ ψ (\{ (δ = i1) → refl }) ((\{ (ψ = i1) → GlueIso.lemma {φ = φ i1} (\ _ → b i1 itIsOne) o }) ) ) ))
|
||||
-- TODO figure out why we need (δ = i1) and (ψ = i1) here
|
||||
t₁ : PartialP (φ i1) _
|
||||
t₁ o = fst (g o)
|
||||
α : PartialP (φ i1) _
|
||||
α o = snd (g o)
|
||||
a₁ = unsafeComp (\ j → A i1) (φ i1 ∨ ψ) (\ j → unsafePOr (φ i1) ψ (\ o → α o j) (a i1)) a₁''
|
||||
b₁ : Glue _ (φ i1) (T i1) (f i1)
|
||||
b₁ = unsafeGlue {φ = φ i1} t₁ a₁
|
||||
b1 = Forall.b₁ (FR.δ φ) (FR.∀e φ)
|
||||
|
||||
compGlue : {la lb : I → _} (A : (i : I) → Set (la i)) (φ : I -> I) (T : ∀ i → Partial (Set (lb i)) (φ i))
|
||||
(f : ∀ i → PartialP (φ i) \ o → (T i o) → (A i)) →
|
||||
(pf : ∀ i → PartialP (φ i) (λ o → isEquiv (T i o) (A i) (f i o))) →
|
||||
let
|
||||
B : (i : I) -> Set (lb i)
|
||||
B = \ i → primGlue (A i) (φ i) (T i) (f i) (pf i)
|
||||
in (ψ : I) (b : ∀ i → Partial (B i) ψ) (b0 : B i0) → B i1
|
||||
compGlue A φ T f pf ψ b b0 = CompGlue.Local.b1 A φ T (λ i p → (f i p) , (pf i p)) ψ b b0
|
||||
|
||||
|
||||
{-# BUILTIN COMPGLUE compGlue #-}
|
||||
|
||||
module ≡-Reasoning {a} {A : Set a} where
|
||||
|
||||
infix 3 _∎
|
||||
infixr 2 _≡⟨⟩_ _≡⟨_⟩_ -- _≅⟨_⟩_
|
||||
infix 1 begin_
|
||||
|
||||
begin_ : ∀{x y : A} → x ≡ y → x ≡ y
|
||||
begin_ x≡y = x≡y
|
||||
|
||||
_≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
|
||||
_ ≡⟨⟩ x≡y = x≡y
|
||||
|
||||
_≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
|
||||
_ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
|
||||
|
||||
-- _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
|
||||
-- _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
|
||||
|
||||
_∎ : ∀ (x : A) → x ≡ x
|
||||
_∎ _ = refl
|
||||
|
|
@ -1,62 +0,0 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
module Primitives where
|
||||
|
||||
|
||||
|
||||
module Postulates where
|
||||
open import Agda.Primitive public
|
||||
open CubicalPrimitives public renaming (isOneEmpty to empty)
|
||||
|
||||
postulate
|
||||
Path : ∀ {a} {A : Set a} → A → A → Set a
|
||||
PathP : ∀ {a} → (A : I → Set a) → A i0 → A i1 → Set a
|
||||
|
||||
{-# BUILTIN PATH Path #-}
|
||||
{-# BUILTIN PATHP PathP #-}
|
||||
|
||||
primitive
|
||||
primPathApply : ∀ {a} {A : Set a} {x y : A} → Path x y → I → A
|
||||
primPathPApply : ∀ {a} → {A : I → Set a} → ∀ {x y} → PathP A x y → (i : I) → A i
|
||||
|
||||
postulate
|
||||
Id : ∀ {a} {A : Set a} → A → A → Set a
|
||||
|
||||
{-# BUILTIN ID Id #-}
|
||||
{-# BUILTIN CONID conid #-}
|
||||
|
||||
primitive
|
||||
primDepIMin : _
|
||||
primIdFace : {a : Level} {A : Set a} {x y : A} → Id x y → I
|
||||
primIdPath : {a : Level} {A : Set a} {x y : A} → Id x y → Path x y
|
||||
|
||||
primitive
|
||||
primIdJ : ∀ {a}{p}{A : Set a}{x : A}(P : ∀ y → Id x y → Set p) → P x (conid i1 (\ i -> x)) → ∀ {y} (p : Id x y) → P y p
|
||||
|
||||
{-# BUILTIN SUB Sub #-}
|
||||
|
||||
postulate
|
||||
inc : ∀ {a} {A : Set a} {φ} (x : A) → Sub {A = A} φ (\ _ → x)
|
||||
|
||||
{-# BUILTIN SUBIN inc #-}
|
||||
|
||||
primitive
|
||||
primSubOut : {a : Level} {A : Set a} {φ : I} {u : Partial A φ} → Sub φ u → A
|
||||
|
||||
|
||||
open Postulates public renaming (primPathApply to _∙_; primIMin to _∧_; primIMax to _∨_; primINeg to ~_
|
||||
; primPFrom1 to p[_]
|
||||
; primIdJ to J
|
||||
; primSubOut to ouc
|
||||
; Path to Path'
|
||||
)
|
||||
|
||||
module Unsafe' (dummy : Set₁) = Postulates
|
||||
|
||||
unsafeComp = Unsafe'.primComp Set
|
||||
unsafePOr = Unsafe'.primPOr Set
|
||||
|
||||
Path : ∀ {a} {A : Set a} → A → A → Set a
|
||||
Path {A = A} = PathP (\ _ → A)
|
||||
|
||||
infix 4 _≡_
|
||||
_≡_ = Path
|
||||
Loading…
Reference in New Issue