Packages

per

5.3.20
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 per foundations inductive.per
Raw

priv/per/foundations/inductive.per 

module inductive where



option irrelevance true



def Β¬ (A : U) : U := A β†’ 𝟎

def βˆ˜α΅€ (A B C: U) : U := (B β†’ C) β†’ (A β†’ B) β†’ (A β†’ C)

def ∘ (A B C : U) : βˆ˜α΅€ A B C := Ξ» (g : B β†’ C) (f : A β†’ B) (x : A), g (f x)

def idα΅€ (A : U) : U := A β†’ A

def id (A : U) (a : A) : A := a

def const (A B : U) : A β†’ B β†’ A := Ξ» (a : A) (b : B), a

def const₁ (A : U) : A β†’ 𝟏 := const 𝟏 A β˜…

def LineP (A : I β†’ U) : V := Ξ  (i : I), A i



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

def idp (A : U) (x : A) : Path A x x := <_> x

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



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



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

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

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

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



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

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



def 2-β₁ (C : 𝟐 β†’ U) (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 : 𝟐 β†’ U) (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



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

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



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

    (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



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

    (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



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

    (Ο† : Ξ  (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)



def W-case (A : U) (B : A β†’ U) (C : U) (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 W-proj₁ (A : U) (B : A β†’ U) : (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 : U) (B : A β†’ U) : Ξ  (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 indα΅‚-Ξ² (A : U) (B : A β†’ U) (C : (W (x : A), B x) β†’ U)

     (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))



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

--  : Ξ  (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 β†’ U) (B : Ξ  (i : I), A i β†’ U) (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)