[Agda] Possibly infinite/exponential compilation time by just calling a certain function
Nils Anders Danielsson
nad at cse.gu.se
Mon Jun 26 16:33:28 CEST 2017
On 2017-06-23 12:42, Jan Bracker wrote:
> What really baffles me is that these are postulates. I do not
> understand why the compiler should ever take any significant amount of
> time to check them.
I think Agda has trouble checking that the last equality type that you
give is well-formed.
I managed to get the code to type-check by adding a large number of
"abstract" annotations to your code (and postulating a single lemma that
failed to type-check), see the attached patch. I suggest that you try to
make all of your "proofs" abstract.
--
/NAD
-------------- next part --------------
diff --git a/src/Theory/Category/Examples.agda b/src/Theory/Category/Examples.agda
index 0d36f4f..8079942 100644
--- a/src/Theory/Category/Examples.agda
+++ b/src/Theory/Category/Examples.agda
@@ -134,6 +134,9 @@ catCategory {ℓ₀} {ℓ₁} = record
; left-id = left-id
; right-id = right-id
} where
+
+ abstract
+
assoc : {a b c d : Category} {f : Functor a b} {g : Functor b c} {h : Functor c d}
→ [ h ]∘[ [ g ]∘[ f ] ] ≡ [ [ h ]∘[ g ] ]∘[ f ]
assoc = functor-eq refl refl
@@ -141,8 +144,10 @@ catCategory {ℓ₀} {ℓ₁} = record
right-id : {a b : Category} {f : Functor a b} → [ Id[ b ] ]∘[ f ] ≡ f
right-id = functor-eq refl refl
+ postulate
+
left-id : {a b : Category} {f : Functor a b} → [ f ]∘[ Id[ a ] ] ≡ f
- left-id = refl
+ -- left-id = refl
-- Category of functors and natural transformations
functorCategory : {Cℓ₀ Cℓ₁ Dℓ₀ Dℓ₁ : Level} → Category {Cℓ₀} {Cℓ₁} → Category {Dℓ₀} {Dℓ₁} → Category
@@ -151,10 +156,25 @@ functorCategory C D = record
; Hom = NaturalTransformation {C = C} {D}
; _∘_ = λ {F} {G} {H} → ⟨_⟩∘ᵥ⟨_⟩ {C = C} {D} {F} {G} {H}
; id = λ {F} → Id⟨ F ⟩
- ; assoc = natural-transformation-eq $ fun-ext $ λ _ → Category.assoc D
- ; left-id = natural-transformation-eq $ fun-ext $ λ _ → Category.left-id D
- ; right-id = natural-transformation-eq $ fun-ext $ λ _ → Category.right-id D
+ ; assoc = assoc′
+ ; left-id = left-id′
+ ; right-id = right-id′
}
+ where
+ abstract
+
+ assoc′ : {a b c d : Functor C D} {f : NaturalTransformation a b}
+ {g : NaturalTransformation b c} {h : NaturalTransformation c d} →
+ ⟨ h ⟩∘ᵥ⟨ ⟨ g ⟩∘ᵥ⟨ f ⟩ ⟩ ≡ ⟨ ⟨ h ⟩∘ᵥ⟨ g ⟩ ⟩∘ᵥ⟨ f ⟩
+ assoc′ = natural-transformation-eq $ fun-ext $ λ _ → Category.assoc D
+
+ left-id′ : {a b : Functor C D} {f : NaturalTransformation a b} →
+ ⟨ f ⟩∘ᵥ⟨ Id⟨ a ⟩ ⟩ ≡ f
+ left-id′ = natural-transformation-eq $ fun-ext $ λ _ → Category.left-id D
+
+ right-id′ : {a b : Functor C D} {f : NaturalTransformation a b} →
+ ⟨ Id⟨ b ⟩ ⟩∘ᵥ⟨ f ⟩ ≡ f
+ right-id′ = natural-transformation-eq $ fun-ext $ λ _ → Category.right-id D
[_,_] = functorCategory
diff --git a/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda b/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
index 11f847c..8cd8162 100644
--- a/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
+++ b/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
@@ -42,9 +42,7 @@ postulate
dayRightUnitor : {ℓC₀ ℓC₁ : Level} → (ℓSet : Level) → {C : Category {ℓC₀} {ℓC₁}} → (CMon : MonoidalCategory C)
→ NaturalIsomorphism ([-, dayUnit {ℓSet = ℓSet} CMon ] (dayConvolution {ℓSet = ℓSet} CMon)) Id[ FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁}) ]
- {-
day-triangle-id : {ℓC₀ ℓC₁ : Level} → (ℓSet : Level) → {C : Category {ℓC₀} {ℓC₁}} → (CMon : MonoidalCategory C)
→ (x y : Functor C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁}))
→ F₁ (dayConvolution {ℓSet = ℓSet} CMon) (iso-η (dayRightUnitor ℓSet CMon) x , id (FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁})) {y} )
≡ ⟨ F₁ (dayConvolution {ℓSet = ℓSet} CMon) (id (FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁})) {x} , iso-η (dayLeftUnitor ℓSet CMon) y) ⟩∘ᵥ⟨ iso-η (dayAssociator ℓSet CMon) (x ,' dayUnit {ℓSet = ℓSet} CMon ,' y) ⟩
- -}
diff --git a/src/Theory/End/Convolution.agda b/src/Theory/End/Convolution.agda
index b63e479..9f553f5 100644
--- a/src/Theory/End/Convolution.agda
+++ b/src/Theory/End/Convolution.agda
@@ -41,6 +41,8 @@ convolutionFunctor {ℓC₀} {ℓC₁} {ℓSet} {C} CMon (functor F₀ F₁ F-id
dayF₁ : {a b : Obj CC×CC} → Hom CC×CC a b → Hom Set' (dayF₀ a) (dayF₀ b)
dayF₁ {a} {b} ((f₁ , f₁') , (f₂ , f₂')) (homC , Fc , Fc') = (homC ∘C (f₁ ⊗C₁ f₁')) , F₁ f₂ Fc , G₁ f₂' Fc'
+ abstract
+
day-id : {a : Obj CC×CC} → dayF₁ {a} {a} (id CC×CC) ≡ id Set'
day-id {a} = begin
dayF₁ {a} {a} (id CC×CC)
@@ -99,6 +101,8 @@ convolutionTransformation {ℓC₀} {ℓC₁} {ℓSet} {C} CMon {F} {G} {F'} {G'
η : (x' : Obj CC×CC) → Hom Set' ([ convolutionFunctor {ℓSet = ℓSet} CMon F G a ]₀ x') ([ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₀ x')
η ((c₀⁻ , c₁⁻) , (c₀⁺ , c₁⁺)) (f , Fc₀ , Gc₁) = (g ∘C f) , nat-η α c₀⁺ Fc₀ , nat-η β c₁⁺ Gc₁
+ abstract
+
nat : {x y : Obj CC×CC} {f : Hom CC×CC x y} → [ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₁ f ∘F η x ≡ η y ∘F [ convolutionFunctor {ℓSet = ℓSet} CMon F G a ]₁ f
nat {x} {y} {f} = begin
[ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₁ f ∘F η x
@@ -123,7 +127,8 @@ convolutionTransFun : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {
→ NaturalTransformation (convolutionFunctor {ℓSet = ℓSet} CMon F G x) (convolutionFunctor {ℓSet = ℓSet} CMon F' G' x)
convolutionTransFun {ℓC₀} {ℓC₁} {ℓSet} {C} CMon α β x = convolutionTransformation {ℓSet = ℓSet} CMon α β (Category.id C {x})
-convolution-trans-obj-id : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {ℓC₁}} (CMon : MonoidalCategory C)
- → (F G : Functor C (setCategory {ℓSet ⊔ ℓC₁ ⊔ ℓC₀})) → (a : Obj C) → convolutionTransObj {ℓSet = ℓSet} CMon F G (id C {a}) ≡ Id⟨ convolutionFunctor {ℓSet = ℓSet} CMon F G a ⟩
-convolution-trans-obj-id {ℓC₀} {ℓC₁} {ℓSet} {C} CMon F G a = natural-transformation-eq $ fun-ext $ λ (c : Obj ((C ×C C) op ×C (C ×C C))) → fun-ext (λ {(f , Fc , Gc) → cong (λ X → X , Fc , Gc) (right-id C)})
+abstract
+ convolution-trans-obj-id : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {ℓC₁}} (CMon : MonoidalCategory C)
+ → (F G : Functor C (setCategory {ℓSet ⊔ ℓC₁ ⊔ ℓC₀})) → (a : Obj C) → convolutionTransObj {ℓSet = ℓSet} CMon F G (id C {a}) ≡ Id⟨ convolutionFunctor {ℓSet = ℓSet} CMon F G a ⟩
+ convolution-trans-obj-id {ℓC₀} {ℓC₁} {ℓSet} {C} CMon F G a = natural-transformation-eq $ fun-ext $ λ (c : Obj ((C ×C C) op ×C (C ×C C))) → fun-ext (λ {(f , Fc , Gc) → cong (λ X → X , Fc , Gc) (right-id C)})
diff --git a/src/Theory/End/DayConvolution.agda b/src/Theory/End/DayConvolution.agda
index 5cff565..afc6c83 100644
--- a/src/Theory/End/DayConvolution.agda
+++ b/src/Theory/End/DayConvolution.agda
@@ -67,6 +67,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
d0₁ : {a b : Obj C} → Hom C a b → Hom Set' (Set-co-∫ ℓSet (dayF F G a)) (Set-co-∫ ℓSet (dayF F G b))
d0₁ {a} {b} f = coendMorph (convolutionTransObj F G f)
+ abstract
+
d0-id : {a : Obj C} → d0₁ {a} {a} (id C) ≡ id Set'
d0-id {a} = begin
coendMorph (convolutionTransObj F G (id C))
@@ -88,6 +90,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
day-η : (x : Obj C) → Hom Set' (CoEnd.co-∫ (dayEnd F G x)) (CoEnd.co-∫ (dayEnd F' G' x))
day-η x = coendMorph (convolutionTransFun α β x)
+ abstract
+
day-nat : {x y : Obj C} {f : Hom C x y} → [ day₀ (F' , G') ]₁ f ∘F day-η x ≡ day-η y ∘F [ day₀ (F , G) ]₁ f
day-nat {x} {y} {f} = begin
[ day₀ (F' , G') ]₁ f ∘F day-η x
@@ -100,6 +104,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
≡⟨⟩
day-η y ∘F [ day₀ (F , G) ]₁ f ∎
+ abstract
+
day-id : {a : Obj [C,S]×[C,S]} → day₁ {a} {a} (id [C,S]×[C,S] {a}) ≡ id [ C , Set' ] {day₀ a}
day-id {F , G} = natural-transformation-eq $ fun-ext $ λ (c : Obj C) → begin
coendMorph (convolutionTransFun Id⟨ F ⟩ Id⟨ G ⟩ c)
@@ -117,4 +123,3 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
coendMorph (convolutionTransFun γ δ c) ∘F coendMorph (convolutionTransFun α β c)
≡⟨⟩
nat-η (day₁ {F' , G'} {F'' , G''} (γ , δ) ∘[C,S] day₁ {F , G} {F' , G'} (α , β)) c ∎
-
diff --git a/src/Theory/End/Properties.agda b/src/Theory/End/Properties.agda
index 97f68a7..6e0898a 100644
--- a/src/Theory/End/Properties.agda
+++ b/src/Theory/End/Properties.agda
@@ -34,6 +34,8 @@ wedgeTransform {ℓC₀} {ℓC₁} {ℓS} {C} {functor H₀ H₁ H-id H-comp} {f
f' : (c : Obj C) → Hom Set' w (H'₀ (c , c))
f' c = nat-η θ (c , c) ∘F f c
+ abstract
+
coher' : {c c' : Obj C} (g : Hom C c c') → H'₁ (g , id C) ∘F f' c' ≡ H'₁ (id C , g) ∘F f' c
coher' {c} {c'} g = begin
H'₁ (g , id C) ∘F f' c'
@@ -59,6 +61,8 @@ cowedgeTransform {ℓC₀} {ℓC₁} {ℓS} {C} {functor H₀ H₁ H-id H-comp}
f' : (c : Obj C) → Hom Set' (H₀ (c , c)) w
f' c = f c ∘F nat-η θ (c , c)
+ abstract
+
coher' : {c c' : Obj C} (g : Hom C c c') → f' c' ∘F H₁ (id C , g) ≡ f' c ∘F H₁ (g , id C)
coher' {c} {c'} g = begin
f' c' ∘F H₁ (id C , g)
@@ -83,7 +87,9 @@ coendMorph : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}}
→ Hom (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS}) (Set-co-∫ ℓS H) (Set-co-∫ ℓS H')
coendMorph {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
-coend-morph-unique : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}}
+abstract
+
+ coend-morph-unique : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}}
→ {H H' : Functor (C op ×C C) (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS})} → (θ : NaturalTransformation H H')
→ (f : Hom (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS}) (Set-co-∫ ℓS H) (Set-co-∫ ℓS H')) → f ≡ coendMorph θ
-coend-morph-unique {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ proj₂ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
+ coend-morph-unique {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ proj₂ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
diff --git a/src/Theory/Functor/Application.agda b/src/Theory/Functor/Application.agda
index eb452c1..c5950ec 100644
--- a/src/Theory/Functor/Application.agda
+++ b/src/Theory/Functor/Application.agda
@@ -50,6 +50,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ : Level}
HomF : {a b : Obj D} → Hom D a b → Hom E (ObjF a) (ObjF b)
HomF f = F₁ (id C {x} , f)
+ abstract
+
composeF : {a b c : Obj D} {f : Hom D a b} {g : Hom D b c}
→ HomF (g ∘D f) ≡ HomF g ∘E HomF f
composeF {a} {b} {c} {f} {g} = begin
@@ -68,6 +70,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ : Level}
HomF : {a b : Obj C} → Hom C a b → Hom E (ObjF a) (ObjF b)
HomF f = F₁ (f , id D {x})
+ abstract
+
composeF : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
→ HomF (g ∘C f) ≡ HomF g ∘E HomF f
composeF {a} {b} {c} {f} {g} = begin
diff --git a/src/Theory/Functor/Association.agda b/src/Theory/Functor/Association.agda
index ab82738..b8188b4 100644
--- a/src/Theory/Functor/Association.agda
+++ b/src/Theory/Functor/Association.agda
@@ -58,6 +58,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
F₁ : {a b : Obj (C ×C (D ×C E))} → Hom (C ×C (D ×C E)) a b → Hom K (F₀ a) (F₀ b)
F₁ (c , d×e) = [ C×J→K ]₁ (c , [ D×E→J ]₁ d×e)
+ abstract
+
idF : {a : Obj (C ×C (D ×C E))}
→ F₁ {a} {a} (id (C ×C (D ×C E))) ≡ id K
idF {a} = begin
@@ -72,6 +74,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
private
_∘CDE_ = _∘_ (C ×C (D ×C E))
+ abstract
+
composeF : {a b c : Obj (C ×C (D ×C E))} {f : Hom (C ×C (D ×C E)) a b} {g : Hom (C ×C (D ×C E)) b c}
→ F₁ (((C ×C (D ×C E)) ∘ g) f) ≡ (K ∘ F₁ g) (F₁ f)
composeF {f = fC , fDE} {g = gC , gDE} = begin
@@ -96,6 +100,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
F₁ : {a b : Obj ((C ×C D) ×C E)} → Hom ((C ×C D) ×C E) a b → Hom K (F₀ a) (F₀ b)
F₁ (c×d , e) = [ J×E→K ]₁ ([ C×D→J ]₁ c×d , e)
+ abstract
+
idF : {a : Obj ((C ×C D) ×C E)}
→ F₁ {a} {a} (id ((C ×C D) ×C E)) ≡ id K
idF {a} = begin
@@ -110,6 +116,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
private
_∘CDE_ = _∘_ ((C ×C D) ×C E)
+ abstract
+
composeF : {a b c : Obj ((C ×C D) ×C E)} {f : Hom ((C ×C D) ×C E) a b} {g : Hom ((C ×C D) ×C E) b c}
→ F₁ (g ∘CDE f) ≡ (F₁ g) ∘K (F₁ f)
composeF {f = fCD , fE} {g = gCD , gE} = begin
@@ -140,4 +148,3 @@ module Associator {ℓC₀ ℓC₁ : Level} {C : Category {ℓC₀} {ℓC₁}} w
-- (_ ⊗ (_ ⊗ _)) ⇒ _
rightAssociator : Functor (C ×C C) C → Functor (C ×C C ×C C) C
rightAssociator F = [ biAssocFunctorR F F ]∘[ assocFunctorR ]
-
diff --git a/src/Theory/Functor/Composition.agda b/src/Theory/Functor/Composition.agda
index ecc2624..b514152 100644
--- a/src/Theory/Functor/Composition.agda
+++ b/src/Theory/Functor/Composition.agda
@@ -27,6 +27,8 @@ compFunctor {C = C} {D = D} {E = E} F G = record
F₁ : {a b : Obj C} → Hom C a b → Hom E (F₀ a) (F₀ b)
F₁ f = [ F ]₁ ( [ G ]₁ f )
+ abstract
+
id : ∀ {a : Obj C} → F₁ {a = a} (Category.id C) ≡ Category.id E
id = trans (cong (λ X → Functor.F₁ F X) (Functor.id G)) (Functor.id F)
diff --git a/src/Theory/Functor/Examples/HomFunctor.agda b/src/Theory/Functor/Examples/HomFunctor.agda
index 9fa8b2b..9e6bde9 100644
--- a/src/Theory/Functor/Examples/HomFunctor.agda
+++ b/src/Theory/Functor/Examples/HomFunctor.agda
@@ -30,6 +30,8 @@ homFunctor {ℓC₀} {ℓC₁} ℓSet {C} a = functor HomF₀ HomF₁ id-HomF co
HomF₁ : {x y : Obj C} → Hom C x y → Hom SetCat (HomF₀ x) (HomF₀ y)
HomF₁ f = λ g → lift (f ∘C lower g)
+ abstract
+
id-HomF : {a : Obj C} → HomF₁ (id C {a}) ≡ id SetCat
id-HomF {a} = begin
HomF₁ (id C)
@@ -50,4 +52,3 @@ homFunctor {ℓC₀} {ℓC₁} ℓSet {C} a = functor HomF₀ HomF₁ id-HomF co
( λ h → lift (g ∘C (f ∘C lower h)) )
≡⟨⟩
(HomF₁ g) ∘Set (HomF₁ f) ∎
-
diff --git a/src/Theory/Natural/Transformation.agda b/src/Theory/Natural/Transformation.agda
index db4a060..065c7de 100644
--- a/src/Theory/Natural/Transformation.agda
+++ b/src/Theory/Natural/Transformation.agda
@@ -66,6 +66,8 @@ compNaturalTransformationVert {C = C} {D} {F} {G} {H} α β = record
η : (a : Category.Obj C) → Category.Hom D ([ F ]₀ a) ([ H ]₀ a)
η a = ηα a ∘D ηβ a
+ abstract
+
natural : {a b : Category.Obj C} {f : Category.Hom C a b}
→ ([ H ]₁ f) ∘D (η a) ≡ (η b) ∘D ([ F ]₁ f)
natural {a} {b} {f} = begin
More information about the Agda
mailing list