underscore.dk 879 Bytes
Newer Older
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
#NAME hott.

Nat: Type.
Fin : Nat -> Type.

type:Type.
e: type -> Type.


def Finm: Nat -> Nat -> Type
:= i:Nat => j:Nat => (Fin i -> Fin j).

def comp := i:Nat => j:Nat => k:Nat => f:Finm i j => g:Finm j k => x:Fin i => g (f x).

Sn1: Type.
Bn: Sn1 -> Nat -> Type.
def mapBn: Ln1:Sn1 -> i:Nat -> ip:Nat -> Finm i ip -> Bn Ln1 ip -> Bn Ln1 i.

[Ln1,i,j,k,f,g,p]
mapBn Ln1 i j f (mapBn _ _ k g p) --> mapBn Ln1 i k (comp i j k f g) p.

n:Nat.

Sn: Type.
Ln1: Sn -> Sn1.
Xn : Ln:Sn -> Bn (Ln1 Ln) n -> Type.

Bsn: Sn -> Nat -> Type.
def bn : Ln:Sn -> i:Nat -> Bsn Ln i -> Bn (Ln1 Ln) i.
def bsn: Ln:Sn -> i:Nat -> p:Bsn Ln i -> f:Finm n i -> Xn Ln (mapBn (Ln1 Ln) n i f (bn Ln i p)).
mkBsn: Ln:Sn -> i:Nat -> bn:Bn (Ln1 Ln) i
	-> bsn:(f:Finm n i -> Xn Ln (mapBn (Ln1 Ln) n i f bn)) -> Bsn Ln i.

[bn2] bn _ _ (mkBsn _ _ bn2 _) --> bn2.

[bsn2] bsn _ _ (mkBsn _ _ _ bsn2) --> bsn2.