favonia

{-# OPTIONS --safe #-}

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A : Set ℓ

favonia

-- Code supplement for CPP22
-- (C) 2022 Patricia Johann, Enrico Ghiorzi
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0.

-- The code was originally for the paper "(Deep) Induction Rules for GADTs",
-- then modified by Favonia, released also under CC BY-SA 4.0

{-# OPTIONS --injective-type-constructors #-}

module _ where