Packages

per

5.3.21
5.3.21 5.3.20 5.3.19 5.3.15 1.0.0

The Per Programming Language

HexDocs

Current section

Files

Jump to
Readme
5 Versions
0 Dependencies
Dependants
Files
Activity
per priv agda foundations inductive.agda
Raw

priv/agda/foundations/inductive.agda 

module inductive where



option irrelevance true



Path (A : Set) (x y : A) : Set = PathP (<_> A) x y

idp (A : Set) (x : A) : Path A x x = <_> x

+ (A B: Set) : Set = Ξ£ (x : 𝟐), indβ‚‚ (Ξ» (_ : 𝟐), Set) A B x



0-ind (C: 𝟎 β†’ Set) (z: 𝟎) : C z = ind-empty (C z) z



1-rec (C: Set) (x: C) : 𝟏 β†’ C = ind₁ (\(_:𝟏), C) x

1-ind (C: 𝟏 β†’ Set) (x: C β˜…) : П (z: 𝟏), C z = ind₁ C x

--def 1-Ξ² (C: Set) (c: C): Path C (1-rec C c β˜…) c = idp C c

--def 1-Ξ· (z: 𝟏) : Path 𝟏 β˜… z = idp 𝟏 β˜…



2-ind (C: 𝟐 β†’ Set) (x: C 0β‚‚) (y: C 1β‚‚) : П (z: 𝟐), C z = indβ‚‚ C x y

2-rec (C: Set) (x y: C) : П (z: bool), C = indβ‚‚ (\(_:𝟐), C) x y



2-β₁ (C : 𝟐 β†’ Set) (f : Ξ  (x : 𝟐), C 0β‚‚) (g : Ξ  (y : 𝟐), C 1β‚‚) : PathP (<_>C 0β‚‚) (f 0β‚‚) (indβ‚‚ (Ξ» (x : 𝟐), C x) (f 0β‚‚) (g 1β‚‚) 0β‚‚) = <_> f 0β‚‚

--def 2-Ξ²β‚‚ (C : 𝟐 β†’ Set) (f : Ξ  (x : 𝟐), C 0β‚‚) (g : Ξ  (y : 𝟐), C 1β‚‚) : PathP (<_>C 1β‚‚) (g 1β‚‚) (indβ‚‚ (Ξ» (x : 𝟐), C x) (f 0β‚‚) (g 1β‚‚) 1β‚‚) = <_> g 1β‚‚



--def 2-Ξ· (c : 𝟐) : + (PathP (<_> 𝟐) c 0β‚‚) (PathP (<_> 𝟐) c 1β‚‚) = indβ‚‚ (Ξ» (c : 𝟐), + (PathP (<_> 𝟐) c 0β‚‚) (PathP (<_> 𝟐) c 1β‚‚)) (0β‚‚, <_> 0β‚‚) (1β‚‚, <_> 1β‚‚) c



Wβ€² (A : Set) (B : A β†’ Set) : Set = W (x: A), B x

supβ€² (A : Set) (B : A β†’ Set) (x : A) (f : B x β†’ Wβ€² A B) : Wβ€² A B = sup A B x f



W-ind (A : Set) (B : A β†’ Set) (C : (W (x : A), B x) β†’ Set)

    (g : Ξ  (x : A) (f : B x β†’ (W (x : A), B x)), (Ξ  (b : B x), C (f b)) β†’ C (sup A B x f))

    (w : W (x : A), B x)

  : C w = indα΅‚ A B C g w



W-rec (A : Set) (B : A β†’ Set) (C : Set)

    (g : Ξ  (x : A) (f : B x β†’ (W (x : A), B x)), (B x β†’ C) β†’ C)

    (w : W (x : A), B x)

  : C = indα΅‚ A B (Ξ» (_ : W (x : A), B x), C) g w



W-indβ€² (A : Set) (B : A β†’ Set) (C : (W (x : A), B x) β†’ Set)

    (Ο† : Ξ  (x : A) (f : B x β†’ (W (x : A), B x)), C (sup A B x f))

  : Ξ  (w : W (x : A), B x), C w

 = indα΅‚ A B C (Ξ» (x : A) (f : B x β†’ (W (x : A), B x)) (g : Ξ  (b : B x), C (f b)), Ο† x f)



W-case (A : Set) (B : A β†’ Set) (C : Set) (g : Ξ  (x : A) (f : B x β†’ (W (x : A), B x)), C)

  : (W (x : A), B x) β†’ C

 = W-indβ€² A B (Ξ» (_ : W (x : A), B x), C) g



-- def indα΅‚-Ξ² (A : Set) (B : A β†’ Set) (C : (W (x : A), B x) β†’ Set)

--     (g : Ξ  (x : A) (f : B x β†’ (W (x : A), B x)), (Ξ  (b : B x), C (f b)) β†’ C (sup A B x f))

--     (a : A) (f : B a β†’ (W (x : A), B x))

--  : PathP (<_> C (sup A B a f)) (indα΅‚ A B C g (sup A B a f)) (g a f (Ξ» (b : B a), indα΅‚ A B C g (f b)))

-- = <_> g a f (Ξ» (b : B a), indα΅‚ A B C g (f b))



W-proj₁ (A : Set) (B : A β†’ Set) : (W (x : A), B x) β†’ A

 = W-case A B A (Ξ» (x : A) (f : B x β†’ (W (x : A), B x)), x)



--def W-projβ‚‚ (A : Set) (B : A β†’ Set) : Ξ  (w : W (x : A), B x), B (W-proj₁ A B w) β†’ (W (x : A), B x)

-- = W-indβ€² A B (Ξ» (w : W (x : A), B x), B (W-proj₁ A B w) β†’ (W (x : A), B x))

--               (Ξ» (x : A) (f : B x β†’ (W (x : A), B x)), f)



--def W-Ξ· (A : Set) (B : A β†’ Set)

--  : Ξ  (w : W (x : A), B x), Path (W (x : A), B x) (sup A B (W-proj₁ A B w) (W-projβ‚‚ A B w)) w

-- = W-indβ€² A B (Ξ» (w : W (x : A), B x), Path (W (x : A), B x) (sup A B (W-proj₁ A B w) (W-projβ‚‚ A B w)) w)

--               (Ξ» (x : A) (f : B x β†’ (W (x : A), B x)), <_> sup A B x f)



--def trans-W (A : I β†’ Set) (B : Ξ  (i : I), A i β†’ Set) (a : A 0) (f : B 0 a β†’ (W (x : A 0), B 0 x)) : W (x : A 1), B 1 x

-- = sup (A 1) (B 1) (transp (<i> A i) 0 a) (transp (<i> B i (transFill (A 0) (A 1) (<j> A j) a @ i) β†’ (W (x : A i), B i x)) 0 f)