← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/Container.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Container.agda
6
6
 
7
7
module Data.Container where
8
8
 
 
9
open import Data.M
9
10
open import Data.Product as Prod hiding (map)
 
11
open import Data.W
10
12
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
11
13
open import Function.Equality using (_⟨$⟩_)
12
14
open import Function.Inverse using (_↔_; module Inverse)
37
39
-- The semantics ("extension") of a container.
38
40
 
39
41
⟦_⟧ : ∀ {ℓ} → Container ℓ → Set ℓ → Set ℓ
40
 
⟦ C ⟧ X = Σ[ s ∶ Shape C ] (Position C s → X)
 
42
⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X)
 
43
 
 
44
-- The least and greatest fixpoints of a container.
 
45
 
 
46
μ : ∀ {ℓ} → Container ℓ → Set ℓ
 
47
μ C = W (Shape C) (Position C)
 
48
 
 
49
ν : ∀ {ℓ} → Container ℓ → Set ℓ
 
50
ν C = M (Shape C) (Position C)
41
51
 
42
52
-- Equality, parametrised on an underlying relation.
43
53
 
44
54
Eq : ∀ {c ℓ} {C : Container c} {X Y : Set c} →
45
55
     (X → Y → Set ℓ) → ⟦ C ⟧ X → ⟦ C ⟧ Y → Set (c ⊔ ℓ)
46
56
Eq {C = C} _≈_ (s , f) (s′ , f′) =
47
 
  Σ[ eq ∶ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))
 
57
  Σ[ eq ∈ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))
48
58
 
49
59
private
50
60