{- Lambek Encoding: Copyright (c) Groupoid Infinity, 2014-2018 see HoTT 5.4 Inductive types are initial algebras -} module lambek where import proto import path import nat import set import iso_sigma import iso_pi {- Definition 5.4.1. A Nat-algebra Definition 5.4.2. Nat Homomorphism -} natOb: U = (X: U) * (zero: X) * (succ: X -> X) * unit natHom (x1 x2: natOb): U = (map: x1.1 -> x2.1) * (mapZero: Path x2.1 (map (x1.2.1)) (x2.2.1)) * (mapSucc: (x: x1.1) -> Path x2.1 (map (x1.2.2.1 x)) (x2.2.2.1 (map x))) * unit isHomotopyInitialNat (I: natOb): U = (C: natOb) * (x: natHom I C) * ((y: natHom I C) -> Path (natHom I C) x y) {- proof : isHomotopyInitialNat (nat,zero,\(x:nat)->succ x,tt) = ((nat,zero,\(x:nat)->succ x,tt), (idfun nat, refl nat ((idfun nat) zero), \(x:nat)->refl nat ((idfun nat) (succ x)), tt), \(p: natHom (nat,zero,\(x:nat)->succ x,tt) (nat,zero,\(x:nat)->succ x,tt)) -> refl (natHom (nat,zero,\(x:nat)->succ x,tt) (nat,zero,\(x:nat)->succ x,tt)) p) -} listOb (A: U): U = (X: U) * (nil: X) * (cons: A -> X -> X) * unit listHom (A: U) (x1 x2: listOb A): U = (map: x1.1 -> x2.1) * (mapNil: Path x2.1 (map (x1.2.1)) (x2.2.1)) * (mapCons: (a:A) (x: x1.1) -> Path x2.1 (map (x1.2.2.1 a x)) (x2.2.2.1 a (map x))) * unit isHomotopyInitialList (A: U) (I: listOb A): U = (C: listOb A) -> isContr(listHom A I C)