← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/iird/IID.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:
examples/outdated-and-incorrect/iird/IID.agda
1
 
 
2
 
module IID where
3
 
 
4
 
open import LF
5
 
 
6
 
data OP (I : Set)(E : Set) : Set1 where
7
 
  ι : E -> OP I E
8
 
  σ : (A : Set)(γ : A -> OP I E) -> OP I E
9
 
  δ : (A : Set)(i : A -> I)(γ : OP I E) -> OP I E
10
 
 
11
 
Args : {I : Set}{E : Set} -> OP I E ->
12
 
     (U : I -> Set) -> Set
13
 
Args (ι e)     U = One
14
 
Args (σ A γ)   U = A × \a -> Args (γ a) U
15
 
Args (δ A i γ) U = ((a : A) -> U (i a)) × \_ -> Args γ U
16
 
 
17
 
index : {I : Set}{E : Set}(γ : OP I E)(U : I -> Set) -> Args γ U -> E
18
 
index (ι e)     U _ = e
19
 
index (σ A γ)   U a = index (γ (π₀ a)) U (π₁ a)
20
 
index (δ A i γ) U a = index γ U (π₁ a)
21
 
 
22
 
IndArg : {I : Set}{E : Set}
23
 
       (γ : OP I E)(U : I -> Set) ->
24
 
       Args γ U -> Set
25
 
IndArg (ι e)     U _ = Zero
26
 
IndArg (σ A γ)   U a = IndArg (γ (π₀ a)) U (π₁ a)
27
 
IndArg (δ A i γ) U a = A + IndArg γ U (π₁ a)
28
 
 
29
 
IndIndex : {I : Set}{E : Set}
30
 
          (γ : OP I E)(U : I -> Set) ->
31
 
          (a : Args γ U) -> IndArg γ U a -> I
32
 
IndIndex (ι e)     U _        ()
33
 
IndIndex (σ A γ)   U arg c       = IndIndex (γ (π₀ arg)) U (π₁ arg) c
34
 
IndIndex (δ A i γ) U arg (inl a) = i a
35
 
IndIndex (δ A i γ) U arg (inr a) = IndIndex γ U (π₁ arg) a
36
 
 
37
 
Ind : {I : Set}{E : Set}
38
 
      (γ : OP I E)(U : I -> Set) ->
39
 
      (a : Args γ U)(v : IndArg γ U a) -> U (IndIndex γ U a v)
40
 
Ind (ι e)     U _             ()
41
 
Ind (σ A γ)   U arg c       = Ind (γ (π₀ arg)) U (π₁ arg) c
42
 
Ind (δ A i γ) U arg (inl a) = (π₀ arg) a
43
 
Ind (δ A i γ) U arg (inr a) = Ind γ U (π₁ arg) a
44
 
 
45
 
IndHyp : {I : Set}{E : Set}
46
 
      (γ : OP I E)(U : I -> Set) ->
47
 
      (F : (i : I) -> U i -> Set)(a : Args γ U) -> Set
48
 
IndHyp γ U F a = (v : IndArg γ U a) -> F (IndIndex γ U a v) (Ind γ U a v)
49
 
 
50
 
IndHyp₁ : {I : Set}{E : Set}
51
 
      (γ : OP I E)(U : I -> Set) ->
52
 
      (F : (i : I) -> U i -> Set1)(a : Args γ U) -> Set1
53
 
IndHyp₁ γ U F a = (v : IndArg γ U a) -> F (IndIndex γ U a v) (Ind γ U a v)
54
 
 
55
 
induction :
56
 
  {I : Set}{E : Set}
57
 
  (γ : OP I E)(U : I -> Set)
58
 
  (F : (i : I) -> U i -> Set)
59
 
  (g : (i : I)(u : U i) -> F i u)
60
 
  (a : Args γ U) -> IndHyp γ U F a
61
 
induction γ U F g a = \hyp -> g (IndIndex γ U a hyp) (Ind γ U a hyp)
62
 
 
63
 
induction₁ :
64
 
  {I : Set}{E : Set}
65
 
  (γ : OP I E)(U : I -> Set)
66
 
  (F : (i : I) -> U i -> Set1)
67
 
  (g : (i : I)(u : U i) -> F i u)
68
 
  (a : Args γ U) -> IndHyp₁ γ U F a
69
 
induction₁ γ U F g a = \hyp -> g (IndIndex γ U a hyp) (Ind γ U a hyp)
70