From 32244c912a957449ad21c086fa5d7f1d4fdea5fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 10 Nov 2017 16:00:00 +0100 Subject: [PATCH] Organize modules --- cat.agda-lib | 9 +- libraries | 1 + src/Cat.agda | 150 -------------------- src/Category.agda | 196 +++++++++++++++++++++++++++ src/Category/Bij.agda | 43 ++++++ src/Category/Free.agda | 38 ++++++ src/Category/Pathy.agda | 52 +++++++ src/Category/Rel.agda | 159 ++++++++++++++++++++++ src/PathPrelude.agda | 293 ---------------------------------------- src/Primitives.agda | 62 --------- 10 files changed, 493 insertions(+), 510 deletions(-) create mode 100644 libraries delete mode 100644 src/Cat.agda create mode 100644 src/Category.agda create mode 100644 src/Category/Bij.agda create mode 100644 src/Category/Free.agda create mode 100644 src/Category/Pathy.agda create mode 100644 src/Category/Rel.agda delete mode 100644 src/PathPrelude.agda delete mode 100644 src/Primitives.agda diff --git a/cat.agda-lib b/cat.agda-lib index cf8593a..1b73d48 100644 --- a/cat.agda-lib +++ b/cat.agda-lib @@ -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 diff --git a/libraries b/libraries new file mode 100644 index 0000000..1813ad5 --- /dev/null +++ b/libraries @@ -0,0 +1 @@ +libs/cubical-demo diff --git a/src/Cat.agda b/src/Cat.agda deleted file mode 100644 index bc43564..0000000 --- a/src/Cat.agda +++ /dev/null @@ -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 diff --git a/src/Category.agda b/src/Category.agda new file mode 100644 index 0000000..ef5c2c4 --- /dev/null +++ b/src/Category.agda @@ -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 diff --git a/src/Category/Bij.agda b/src/Category/Bij.agda new file mode 100644 index 0000000..217c329 --- /dev/null +++ b/src/Category/Bij.agda @@ -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) = {!!} diff --git a/src/Category/Free.agda b/src/Category/Free.agda new file mode 100644 index 0000000..c67f25a --- /dev/null +++ b/src/Category/Free.agda @@ -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 + } diff --git a/src/Category/Pathy.agda b/src/Category/Pathy.agda new file mode 100644 index 0000000..7738726 --- /dev/null +++ b/src/Category/Pathy.agda @@ -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 = {!!} diff --git a/src/Category/Rel.agda b/src/Category/Rel.agda new file mode 100644 index 0000000..2091558 --- /dev/null +++ b/src/Category/Rel.agda @@ -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 = {!!} + } diff --git a/src/PathPrelude.agda b/src/PathPrelude.agda deleted file mode 100644 index 0746fe1..0000000 --- a/src/PathPrelude.agda +++ /dev/null @@ -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 diff --git a/src/Primitives.agda b/src/Primitives.agda deleted file mode 100644 index 258b1f7..0000000 --- a/src/Primitives.agda +++ /dev/null @@ -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