22
33module Cheshire.Core where
44
5+ import Overture
6+ open import Overture
7+ hiding (module Func ; module × ; _⊎_)
8+ renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) public
59import Algebra
610
7- open Algebra using (Op₁; Op₂)
8-
9- module 𝕃 where
10- open import Level renaming (Level to t) public
11-
1211open 𝕃 using (_⊔_) public
13-
14- module 𝟘 where
15- import Data.Empty as 𝟘0ℓ
16- open import Data.Empty.Polymorphic renaming (⊥ to t) public
17-
18- module 𝟙 where
19- import Data.Unit as 𝟙0ℓ
20- open import Data.Unit.Polymorphic renaming (⊤ to t; tt to tt-lift) public
21- pattern tt = 𝕃.lift 𝟙0ℓ.tt
22-
23- module Rel₀ where
24- open import Relation.Nullary public
25-
26- module Rel₁ where
27- open import Relation.Unary hiding (∅; U) public
28- open import Relation.Unary.Polymorphic public
29-
30- module Rel₂ where
31- open import Relation.Binary public hiding (Setoid)
32- open import Relation.Binary.PropositionalEquality public
33-
34- open Rel₂ using (Rel) public
35-
36- module Setoid where
37- open import Relation.Binary.Bundles using () renaming (Setoid to t) public
38- import Relation.Binary.Reasoning.Setoid as SetoidR
39- module Reasoning {s₁ s₂} (S : t s₁ s₂) = SetoidR S
40-
41- lift : ∀ {c ℓ} (o r : 𝕃.t) → t c ℓ → t (o 𝕃.⊔ c) (r 𝕃.⊔ ℓ)
42- lift o r S = record
43- { Carrier = 𝕃.Lift o Carrier
44- ; _≈_ = λ where
45- (𝕃.lift x) (𝕃.lift y) → 𝕃.Lift r (x ≈ y)
46- ; isEquivalence = record
47- { refl = 𝕃.lift (Rel₂.IsEquivalence.refl (t.isEquivalence S))
48- ; sym = λ where
49- (𝕃.lift eq) → 𝕃.lift (Rel₂.IsEquivalence.sym (t.isEquivalence S) eq)
50- ; trans = λ where
51- (𝕃.lift eq) (𝕃.lift eq′) → 𝕃.lift (Rel₂.IsEquivalence.trans (t.isEquivalence S) eq eq′)
52- }
53- } where open t S
12+ open Algebra using (Op₁; Op₂)
5413
5514module Func where
56- open import Function.Bundles renaming (Func to t) public
57- open import Function.Relation.Binary.Setoid.Equality public
15+ open Overture using ( module Func )
16+ open Func public
5817
5918 module _ {c ℓ} (S : Setoid.t c ℓ) where
6019 open Setoid.t S renaming (Carrier to X; _≈_ to eq)
6120
6221 unary : {f : Op₁ X} → Algebra.Congruent₁ eq f → S ⟶ₛ S
63- unary {f} _ .t.to = f
64- unary cong .t.cong = cong
22+ unary {f} _ .Func. t.to = f
23+ unary cong .Func. t.cong = cong
6524
6625 module _ {c ℓ} (S : Setoid.t c ℓ) where
6726 open Setoid.t S renaming (Carrier to X; _≈_ to eq; isEquivalence to isEq)
6827
6928 binary : {f : Op₂ X} → Algebra.Congruent₂ eq f → S ⟶ₛ (S ⇨ S)
70- binary {f} eq .t.to = λ x → record
29+ binary {f} eq .Func. t.to = λ x → record
7130 { to = λ y → f x y
7231 ; cong = eq (Rel₂.IsEquivalence.refl isEq)
7332 }
74- binary eq .t.cong = λ x≈y _ → eq x≈y (Rel₂.IsEquivalence.refl isEq)
33+ binary eq .Func. t.cong = λ x≈y _ → eq x≈y (Rel₂.IsEquivalence.refl isEq)
7534
7635 module _ {c ℓ} (m : Algebra.Magma c ℓ) where
7736 open Algebra.Magma m renaming (setoid to S)
@@ -81,12 +40,11 @@ module Func where
8140
8241open Func using (_⟨$⟩_; _⟶ₛ_; _⇨_) public
8342
84- module Function where
85- open import Function renaming (_∘_ to _⊙_) public
86-
87- open Function using (case_of_; case_returning_of_; const; flip; _on_; _$_) public
43+ open Function
44+ using (case_of_; case_returning_of_; const; flip; _on_; _$_)
45+ renaming (_∘_ to _⊙_) public
8846
89- record Quiver o ℓ : Set (𝕃.suc (o ⊔ ℓ)) where
47+ record Quiver o ℓ : Set (𝕃.suc (o 𝕃. ⊔ ℓ)) where
9048 no-eta-equality
9149 constructor mk⇒
9250 infix 4 _⇒_
@@ -109,7 +67,7 @@ _[_,_] : (𝒬 : Quiver o ℓ) → Rel (𝒬 .Ob) ℓ
10967{-# DISPLAY Hom 𝒬 A B = 𝒬 [ A , B ] #-}
11068{-# DISPLAY Quiver._⇒_ 𝒬 A B = 𝒬 [ A , B ] #-}
11169
112- record Equivalence (𝒬 : Quiver o ℓ) (e : 𝕃.t) : Set (o ⊔ ℓ ⊔ 𝕃.suc e) where
70+ record Equivalence (𝒬 : Quiver o ℓ) (e : 𝕃.t) : Set (o 𝕃. ⊔ ℓ 𝕃. ⊔ 𝕃.suc e) where
11371 infix 4 _≈_
11472 open Quiver 𝒬 using (_⇒_)
11573 field
0 commit comments