← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/succeed/Issue292-17.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/succeed/Issue292-17.agda
1
 
module Issue292-17 where
2
 
 
3
 
data _≡_ {A : Set} (x : A) : A → Set where
4
 
  refl : x ≡ x
5
 
 
6
 
record Σ (A : Set) (B : A → Set) : Set where
7
 
  constructor _,_
8
 
  field
9
 
    proj₁ : A
10
 
    proj₂ : B proj₁
11
 
 
12
 
open Σ
13
 
 
14
 
postulate
15
 
  I  : Set
16
 
  U  : I → Set
17
 
  El : ∀ {i} → U i → Set
18
 
 
19
 
mutual
20
 
 
21
 
  infixl 5 _▻_
22
 
 
23
 
  data Ctxt : Set where
24
 
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt
25
 
 
26
 
  Type : Ctxt → Set
27
 
  Type Γ = Σ I (λ i → Env Γ → U i)
28
 
 
29
 
  Env : Ctxt → Set
30
 
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (proj₂ σ γ)
31
 
 
32
 
postulate
33
 
  Γ : Ctxt
34
 
  σ : Type Γ
35
 
 
36
 
data D : Type (Γ ▻ σ) → Set where
37
 
  d : (τ : Type Γ) → D (proj₁ τ , λ γ → proj₂ τ (proj₁ γ))
38
 
 
39
 
record [D] : Set where
40
 
  constructor [d]
41
 
  field
42
 
    τ : Type (Γ ▻ σ)
43
 
    x : D τ
44
 
 
45
 
Foo : {τ₁ τ₂ : Type Γ} →
46
 
      [d] (proj₁ τ₁ , λ γ → proj₂ τ₁ (proj₁ γ)) (d τ₁) ≡
47
 
      [d] (proj₁ τ₂ , λ γ → proj₂ τ₂ (proj₁ γ)) (d τ₂) →
48
 
      Set₁
49
 
Foo refl = Set