HereditarilySingletonRecord.agda

-- Modified: Andreas, 2011-04-11 freezing Metas
module HereditarilySingletonRecord where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- * trivial unit type

record Singleton : Set where

foo : Singleton
foo = _

-- * product of unit types

record HereditarilySingleton : Set where
  field
    singleton      : Singleton
    also-singleton : Singleton

bar : HereditarilySingleton
bar = _

-- * hiding the unit types behind a type case

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

Unit : ℕ → Set
Unit zero    = Singleton
Unit (suc n) = Unit n

mutual -- needed to avoid freezing

  one : ℕ
  one = _
  
  record HereditarilySingleton₂ : Set where
    field
      singleton : Unit one
  
  baz : HereditarilySingleton₂
  baz = _
  
  force : one ≡ suc zero
  force = refl