← 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/IIDg.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/IIDg.agda
1
 
module IIDg where
2
 
 
3
 
open import LF
4
 
 
5
 
data OPg (I : Set) : Set1 where
6
 
  ι : I -> OPg I
7
 
  σ : (A : Set)(γ : A -> OPg I) -> OPg I
8
 
  δ : (H : Set)(i : H -> I)(γ : OPg I) -> OPg I
9
 
 
10
 
Args : {I : Set}(γ : OPg I)(U : I -> Set) -> Set
11
 
Args (ι _)     U = One
12
 
Args (σ A γ)   U = A × \a -> Args (γ a) U
13
 
Args (δ H i γ) U = ((x : H) -> U (i x)) × \_ -> Args γ U
14
 
 
15
 
Index : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> I
16
 
Index (ι i)     U _         = i
17
 
Index (σ A γ)   U < a | b > = Index (γ a) U b
18
 
Index (δ _ _ γ) U < _ | b > = Index γ U b
19
 
 
20
 
IndArg : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> Set
21
 
IndArg (ι _)     U _         = Zero
22
 
IndArg (σ A γ)   U < a | b > = IndArg (γ a) U b
23
 
IndArg (δ H i γ) U < _ | b > = H + IndArg γ U b
24
 
 
25
 
IndIndex : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U) -> IndArg γ U a -> I
26
 
IndIndex (ι _)     U _       ()
27
 
IndIndex (σ A γ)   U < a | b > h       = IndIndex (γ a) U b h
28
 
IndIndex (δ A i γ) U < g | b > (inl h) = i h
29
 
IndIndex (δ A i γ) U < g | b > (inr h) = IndIndex γ U b h
30
 
 
31
 
Ind : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U)(h : IndArg γ U a) -> U (IndIndex γ U a h)
32
 
Ind (ι _)     U _         ()
33
 
Ind (σ A γ)   U < a | b > h       = Ind (γ a) U b h
34
 
Ind (δ H i γ) U < g | b > (inl h) = g h
35
 
Ind (δ H i γ) U < _ | b > (inr h) = Ind γ U b h
36
 
 
37
 
IndHyp : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set)(a : Args γ U) -> Set
38
 
IndHyp γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp)
39
 
 
40
 
IndHyp₁ : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set1)(a : Args γ U) -> Set1
41
 
IndHyp₁ γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp)
42