MySum.idr

module MySum

record ADepType : Type where
  MkADepType : 
    (dtBase : Type) -> 
    (dtFiber : dtBase -> Type) ->
    ADepType

record ADepSum : ADepType -> Type where
  MkADepSum : 
    {dt : ADepType} ->
    (dsBaseValue : dtBase dt) ->
    (dsFiberValue : dtFiber dt dsBaseValue) ->
    ADepSum dt

class Base t b where
  base : t -> b

instance Base ADepType Type where
  base = dtBase

instance Base (ADepSum dt) (dtBase dt) where
  base = ?see
--  base = dsBaseValue