text:
-- Adapted from Wadler: https://plfa.github.io/Lambda/

module Context (A : Set) where
  open import Prelude

  open import Data.Nat
  open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym)
  open import Data.Maybe
  open import Data.Product using (_×_; proj₁; proj₂; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
  open import Relation.Nullary.Decidable
  open import Relation.Nullary using (Dec; yes; no)
  open import Data.Empty
  import Data.Nat.Properties

  infixl 5  _,_⦂_

  -- Internal type of contexts
  data ctx : Set where
    ∅     : ctx
    _,_⦂_  : ctx → ℕ → A → ctx

  infix  4  _∋_⦂_

  data _∋_⦂_ : ctx → ℕ → A → Set where

    Z : ∀ {Γ : ctx}
      → ∀ {x : ℕ}
      → ∀ {a : A}
        ------------------
      → Γ , x ⦂ a ∋ x ⦂ a

    S : ∀ {Γ x y a b}
      → x ≢ y
      → Γ ∋ x ⦂ a
        ------------------
      → Γ , y ⦂ b ∋ x ⦂ a

  lookup : ctx → ℕ → Maybe A
  lookup ∅ _ = nothing
  lookup (Γ , x ⦂ t) y with compare x y
  ...                       | equal _ = just t
  ...                       | _ = lookup Γ x

  data _∈dom_ : ℕ → ctx → Set where
    inDom : ∀ {x Γ a}
          → Γ ∋ x ⦂ a
          -------------
          → x ∈dom Γ

  data _∉dom_ : ℕ → ctx → Set where
    notInEmpty : ∀ {x}
               ----------
               → x ∉dom ∅

    notInNonempty : ∀ {x x' Γ T}
                    → x ≢ x'
                    → x ∉dom Γ
                    --------------------
                    → x ∉dom (Γ , x' ⦂ T)

  irrelevantExtensionsOK : ∀ {Γ : ctx}
                           → ∀ {x y t t'}
                           → Γ ∋ x ⦂ t
                           → x ≢ y
                           → Γ , y ⦂ t' ∋ x ⦂ t
  irrelevantExtensionsOK {Γ} {x} {y} {t} cont@(Z {Γ₀} {x} {t}) neq = S neq cont
  irrelevantExtensionsOK (S neq' rest) neq = S neq (irrelevantExtensionsOK rest neq')

  irrelevantReductionsOK :  ∀ {Γ : ctx}
                           → ∀ {x y t t'}
                           → Γ , x ⦂ t ∋ y ⦂ t'
                           → y ≢ x
                           → Γ ∋ y ⦂ t'
                           -- ⊥-elim (!neq (Relation.Binary.PropositionalEquality.sym x x))
  irrelevantReductionsOK {Γ} {x} {y} {t} {t'} z@(Z {Γ} {x} {t}) neq =
    let
      s : x ≡ x
      s = refl
      bot = neq s
    in
      Data.Empty.⊥-elim bot

  irrelevantReductionsOK {Γ} {x} {y} {t} {t'} (S x₁ qq) neq = qq

  irrelevantReductionsInValuesOK :  ∀ {Γ : ctx}
                                 → ∀ {x y t t'}
                                 → Γ , x ⦂ t ∋ y ⦂ t'
                                 → t ≢ t'
                                 → Γ ∋ y ⦂ t'
  irrelevantReductionsInValuesOK {Γ} {x} {.x} {t} {.t} Z tNeqt' = ⊥-elim (tNeqt' refl)
  irrelevantReductionsInValuesOK {Γ} {x} {y} {t} {t'} (S yNeqx yt'InΓ') tNeqt' = yt'InΓ'

  ∈domExcludedMiddle : ∀ {Γ x}
                       → x ∉dom Γ
                       → Relation.Nullary.¬ (x ∈dom Γ)
  ∈domExcludedMiddle {.∅} {x} notInEmpty (inDom ())
  ∈domExcludedMiddle {.(_ , _ ⦂ _)} {x} (notInNonempty xNeqx' xNotInΓ) (inDom n) =
    let
      rest = ∈domExcludedMiddle xNotInΓ
      xInΓ = irrelevantReductionsOK n xNeqx'
    in
      rest (inDom xInΓ)

  ∉domPreservation : ∀ {x x' Γ T T'}
                     → x ∉dom (Γ , x' ⦂ T)
                     ---------------------
                     → x ∉dom (Γ , x' ⦂ T')
  ∉domPreservation {x} {x'} {Γ} {T} {T'} (notInNonempty xNeqX' xNotInDom) = notInNonempty xNeqX' xNotInDom

  ∉domGreaterThan : ∀ {Γ x}
                    → (∀ x' → x' ∈dom Γ → x' < x)
                    → x ∉dom Γ
  ∉domGreaterThan {∅} {x} xBigger = notInEmpty
  ∉domGreaterThan {Γ , x' ⦂ t} {x} xBigger =
      notInNonempty x≢x' (∉domGreaterThan rest) -- (∉domGreaterThan (λ x'' → λ x''InΓ → xBigger x'' (inDom {!!})))
    where
      x'<x = xBigger x' (inDom Z)
      x≢x' : x ≢ x'
      x≢x' = ≢-sym (Data.Nat.Properties.<⇒≢ x'<x)

      rest : (x'' : ℕ)
             → x'' ∈dom Γ
             → x'' < x
      rest x'' (inDom x''InΓ) with x' ≟ x''
      ... | yes x'≡x'' rewrite x'≡x'' = xBigger x'' (inDom Z)
      ... | no x'≢x'' = xBigger x'' (inDom (S (≢-sym x'≢x'') x''InΓ))

  fresh : (Γ : ctx)
        → ∃[ x ] (x ∉dom Γ × (∀ x' → x' ∈dom Γ → x' < x))
  fresh ∅ =
    ⟨ zero , ⟨ notInEmpty , xBigger ⟩ ⟩
    where
      xBigger :  (∀ x' → x' ∈dom ∅ → x' < zero)
      xBigger x' (inDom ())
  fresh (Γ , x ⦂ t) =
    ⟨ x' , ⟨ x'IsFresh , x'Bigger ⟩ ⟩
    where
      freshInRest = fresh Γ
      biggerThanRest = suc (proj₁ freshInRest)
      x' = biggerThanRest ⊔ (suc x) -- bigger than both everything in Γ and x.
      freshInRestBigger = proj₂ (proj₂ freshInRest)
      x'Bigger : (x'' : ℕ) → (x'' ∈dom (Γ , x ⦂ t)) → x'' < x'
      x'Bigger x'' (inDom x''InΓ') with x ≟ x''
      ... | yes x≡x'' rewrite x≡x'' =
          s≤s (Data.Nat.Properties.n≤m⊔n (proj₁ (fresh Γ)) x'') -- s≤s (Data.Nat.Properties.<⇒≤ x''<oldFresh)
      ... | no x≢x'' =
        let
          x''<oldFresh = freshInRestBigger x'' (inDom (irrelevantReductionsOK x''InΓ' (≢-sym x≢x'')) )
          x''≤oldFresh = (Data.Nat.Properties.<⇒≤ x''<oldFresh)
        in
          s≤s ( Data.Nat.Properties.m≤n⇒m≤n⊔o x x''≤oldFresh) --  s≤s (Data.Nat.Properties.<⇒≤ x''<oldFresh)
      x'IsFresh : x' ∉dom (Γ , x ⦂ t)
      x'IsFresh = ∉domGreaterThan x'Bigger

-- Removing elements from a context
  _#_ : ctx → ℕ → ctx
  ∅ # x = ∅
  (Γ , x' ⦂ T) # x with compare x x'
  ... | equal _  = Γ
  ... | _ = (Γ # x) , x' ⦂ T

  contextLookupUnique : ∀ {Γ : ctx}
                        → ∀ {x t t'}
                        → Γ ∋ x ⦂ t
                        → Γ ∋ x ⦂ t'
                        → t ≡ t'
  contextLookupUnique z1@Z z2@Z = refl
  contextLookupUnique z1@Z s2@(S {Γ} {x} {y} {a} {b} neq xHasTypeT') = Data.Empty.⊥-elim (neq refl)
  contextLookupUnique (S neq xHasTypeT) Z = Data.Empty.⊥-elim (neq refl)
  contextLookupUnique (S x₁ xHasTypeT) (S x₂ xHasTypeT') = contextLookupUnique xHasTypeT xHasTypeT'

  contextLookupNeq : ∀ {Γ : ctx}
                     → ∀ {x x' t t'}
                     → Γ , x ⦂ t ∋ x' ⦂ t'
                     → t ≢ t'
                     → x ≢ x'
  contextLookupNeq Z tNeq = Data.Empty.⊥-elim (tNeq refl)
  contextLookupNeq (S xNeq x'InΓ) tNeq = λ xEq → xNeq (sym xEq)

  lookupWeakening : ∀ {Γ : ctx}
                    → ∀ {x x' t t'}
                    → Γ ∋ x ⦂ t
                    → ∃[ T ] ((Γ , x' ⦂ t') ∋ x ⦂ T)

  lookupWeakening {Γ} {x} {x'} {t} {t'} Γcontainment with x ≟ x'
  ...                                                 | yes refl = ⟨ t' , Z {Γ = Γ} {x = x'} {a = t'} ⟩
  ...                                                 | no neq =  ⟨ t , S neq Γcontainment ⟩

  ∉dom-≢ : {Γ : ctx}
           → ∀ {x x' t}
           → x ∉dom (Γ , x' ⦂ t)
           → x ≢ x'

  ∉dom-≢ {Γ} {x} {x'} {t} (notInNonempty xNeqx' xNotInΓ') xEqx' = xNeqx' xEqx'

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
open import Proc

module Hear (param : Param) where

open import Basics
private open module P = Process param

open Tran

hear : {a : U}{p : Proc a} -> Guard p -> LT a -> Proc a
hear {p = p} g    bot      = p
hear og           (lift v) = o
hear (w !g p)     (lift v) = w ! p
hear (>g f)       (lift v) = f v
hear (_ ! _ +g f) (lift v) = f v
hear (g1 ||g g2)  (lift v) = hear g1 (lift v) || hear g2 (lift v)
hear (φ /|g g)    (lift v) = φ /| hear g (downV φ v)
hear (defg x g)   (lift v) = hear g (lift v)

sound : {a : U}{p : Proc a}(g : Guard p){w : LT a} ->
        p -[ w ]-> hear g w
sound g            {bot}    = qtau
sound og           {lift v} = rx-o
sound (>g _)       {lift v} = rx->
sound (w !g p)     {lift v} = rx-!
sound (w ! p +g f) {lift v} = rx-+
sound (g1 ||g g2)  {lift v} = rx-|| (sound g1) (sound g2)
sound (φ /|g g)    {lift v} = rx-/| (sound g)
sound (defg x g)   {lift v} = rx-def (sound g)

uniq : {a : U}{p : Proc a}{w : LT a}{px py : Proc a} ->
       p -[ w ]-> px -> p -[ w ]-> py -> px == py
uniq qtau qtau = refl
uniq rx-o rx-o = refl
uniq rx-> rx-> = refl
uniq rx-! rx-! = refl
uniq rx-+ rx-+ = refl
uniq (rx-|| l1 r1) (rx-|| l2 r2) with uniq l1 l2 | uniq r1 r2
... | refl | refl = refl
uniq (rx-/| r1) (rx-/| r2) with uniq r1 r2
... | refl = refl
uniq (rx-def r1) (rx-def r2) with uniq r1 r2
... | refl = refl

complete : {a : U}{p : Proc a}(g : Guard p){w : LT a}{p' : Proc a} ->
           p -[ w ]-> p' -> p' == hear g w
complete g r = uniq r (sound g)

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NatProps where
open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s)
open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym)

<-¬≡ : ∀ {n m} → n < m → ¬ n ≡ m
<-¬≡ {zero} {zero} ()
<-¬≡ {zero} {suc m} p = λ ()
<-¬≡ {suc n} {zero} p = λ ()
<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) with (<-¬≡ p)
... | q = λ { refl → q refl }

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutations using setoid equality
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary hiding (Decidable)

module Data.List.Relation.Binary.Permutation.Setoid.Properties
  {a ℓ} (S : Setoid a ℓ)
  where

open import Algebra
open import Data.Fin.Base using (Fin)
open import Data.List.Base as List hiding (head; tail)
open import Data.List.Relation.Binary.Pointwise as Pointwise
  using (Pointwise; head; tail)
import Data.List.Relation.Binary.Equality.Setoid as Equality
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
import Data.List.Relation.Unary.Unique.Setoid as Unique
import Data.List.Membership.Setoid as Membership
open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert)
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag; _∼[_]_; empty-unique; drop-cons; commutativeMonoid)
import Data.List.Properties as Lₚ
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Induction
open import Data.Nat.Properties
open import Data.Product using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
open import Function using (_∘_; _⟨_⟩_; flip)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (inverse)
open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
open import Relation.Binary.PropositionalEquality as ≡
  using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)

private
  variable
    b p r : Level

open Setoid S using (_≈_) renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
open Permutation S
open Membership S
open Unique S using (Unique)
open module ≋ = Equality S
  using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans; All-resp-≋; Any-resp-≋; AllPairs-resp-≋)
open PermutationReasoning

------------------------------------------------------------------------
-- Relationships to other predicates
------------------------------------------------------------------------

All-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _↭_
All-resp-↭ resp (refl xs≋ys)   pxs             = All-resp-≋ resp xs≋ys pxs
All-resp-↭ resp (prep x≈y p)   (px ∷ pxs)      = resp x≈y px ∷ All-resp-↭ resp p pxs
All-resp-↭ resp (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ resp p pxs
All-resp-↭ resp (trans p₁ p₂)  pxs             = All-resp-↭ resp p₂ (All-resp-↭ resp p₁ pxs)

Any-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (Any P) Respects _↭_
Any-resp-↭ resp (refl xs≋ys) pxs                 = Any-resp-≋ resp xs≋ys pxs
Any-resp-↭ resp (prep x≈y p) (here px)           = here (resp x≈y px)
Any-resp-↭ resp (prep x≈y p) (there pxs)         = there (Any-resp-↭ resp p pxs)
Any-resp-↭ resp (swap x y p) (here px)           = there (here (resp x px))
Any-resp-↭ resp (swap x y p) (there (here px))   = here (resp y px)
Any-resp-↭ resp (swap x y p) (there (there pxs)) = there (there (Any-resp-↭ resp p pxs))
Any-resp-↭ resp (trans p₁ p₂) pxs                = Any-resp-↭ resp p₂ (Any-resp-↭ resp p₁ pxs)

AllPairs-resp-↭ : ∀ {R : Rel A r} → Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
AllPairs-resp-↭ sym resp (refl xs≋ys)     pxs             = AllPairs-resp-≋ resp xs≋ys pxs
AllPairs-resp-↭ sym resp (prep x≈y p)     (∼ ∷ pxs)       =
  All-resp-↭ (proj₁ resp) p (All.map (proj₂ resp x≈y) ∼) ∷
  AllPairs-resp-↭ sym resp p pxs
AllPairs-resp-↭ sym resp@(rʳ , rˡ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) =
  (sym (rʳ eq₂ (rˡ eq₁ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷
  All-resp-↭ rʳ p (All.map (rˡ eq₁) ∼₂) ∷
  AllPairs-resp-↭ sym resp p pxs
AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =
  AllPairs-resp-↭ sym resp p₂ (AllPairs-resp-↭ sym resp p₁ pxs)

∈-resp-↭ : ∀ {x} → (x ∈_) Respects _↭_
∈-resp-↭ = Any-resp-↭ (flip ≈-trans)

Unique-resp-↭ : Unique Respects _↭_
Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂

------------------------------------------------------------------------
-- Relationships to other relations
------------------------------------------------------------------------

≋⇒↭ : _≋_ ⇒ _↭_
≋⇒↭ = refl

↭-respʳ-≋ : _↭_ Respectsʳ _≋_
↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans eq₁ w≈z) (≈-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)

↭-respˡ-≋ : _↭_ Respectsˡ _≋_
↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans (≈-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans (≈-sym x≈y) eq₁) (≈-trans (≈-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs

------------------------------------------------------------------------
-- Properties of steps
------------------------------------------------------------------------

0<steps : ∀ {xs ys} (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
0<steps (refl _)             = s≤s z≤n
0<steps (prep eq xs↭ys)      = ≤-step (0<steps xs↭ys)
0<steps (swap eq₁ eq₂ xs↭ys) = ≤-step (0<steps xs↭ys)
0<steps (trans xs↭ys xs↭ys₁) =
  <-transˡ (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))

steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
              steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
steps-respˡ _               (refl _)            = refl
steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)

steps-respʳ : ∀ {xs ys zs} (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) →
              steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
steps-respʳ _               (refl _)            = refl
steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)

------------------------------------------------------------------------
-- Properties of list functions
------------------------------------------------------------------------

------------------------------------------------------------------------
-- map

module _ (T : Setoid b ℓ) where

  open Setoid T using () renaming (_≈_ to _≈′_)
  open Permutation T using () renaming (_↭_ to _↭′_)

  map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ →
         ∀ {xs ys} → xs ↭ ys → map f xs ↭′ map f ys
  map⁺ pres (refl xs≋ys)  = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys))
  map⁺ pres (prep x p)    = prep (pres x) (map⁺ pres p)
  map⁺ pres (swap x y p)  = swap (pres x) (pres y) (map⁺ pres p)
  map⁺ pres (trans p₁ p₂) = trans (map⁺ pres p₁) (map⁺ pres p₂)

------------------------------------------------------------------------
-- _++_

shift : ∀ {v w} → v ≈ w → (xs ys : List A) → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
shift {v} {w} v≈w []       ys = prep v≈w ↭-refl
shift {v} {w} v≈w (x ∷ xs) ys = begin
  x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v≈w xs ys ⟩
  x ∷ w ∷ xs ++ ys        <<⟨ ↭-refl ⟩
  w ∷ x ∷ xs ++ ys        ∎

++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
++⁺ˡ []       ys↭zs = ys↭zs
++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)

++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
++⁺ʳ zs (refl xs≋ys)  = refl (Pointwise.++⁺ xs≋ys ≋-refl)
++⁺ʳ zs (prep x ↭)    = prep x (++⁺ʳ zs ↭)
++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)

++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)

-- Algebraic properties

++-identityˡ : LeftIdentity _↭_ [] _++_
++-identityˡ xs = ↭-refl

++-identityʳ : RightIdentity _↭_ [] _++_
++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)

++-identity : Identity _↭_ [] _++_
++-identity = ++-identityˡ , ++-identityʳ

++-assoc : Associative _↭_ _++_
++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)

++-comm : Commutative _↭_ _++_
++-comm []       ys = ↭-sym (++-identityʳ ys)
++-comm (x ∷ xs) ys = begin
  x ∷ xs ++ ys         <⟨ ++-comm xs ys ⟩
  x ∷ ys ++ xs         ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
  (x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (shift ≈-refl ys [])) ⟩
  (ys ++ [ x ]) ++ xs  ↭⟨ ++-assoc ys [ x ] xs ⟩
  ys ++ ([ x ] ++ xs)  ≡⟨⟩
  ys ++ (x ∷ xs)       ∎

-- Structures

++-isMagma : IsMagma _↭_ _++_
++-isMagma = record
  { isEquivalence = ↭-isEquivalence
  ; ∙-cong        = ++⁺
  }

++-isSemigroup : IsSemigroup _↭_ _++_
++-isSemigroup = record
  { isMagma = ++-isMagma
  ; assoc   = ++-assoc
  }

++-isMonoid : IsMonoid _↭_ _++_ []
++-isMonoid = record
  { isSemigroup = ++-isSemigroup
  ; identity    = ++-identity
  }

++-isCommutativeMonoid : IsCommutativeMonoid _↭_ _++_ []
++-isCommutativeMonoid = record
  { isMonoid = ++-isMonoid
  ; comm     = ++-comm
  }

-- Bundles

++-magma : Magma a (a ⊔ ℓ)
++-magma = record
  { isMagma = ++-isMagma
  }

++-semigroup : Semigroup a (a ⊔ ℓ)
++-semigroup = record
  { isSemigroup = ++-isSemigroup
  }

++-monoid : Monoid a (a ⊔ ℓ)
++-monoid = record
  { isMonoid = ++-isMonoid
  }

++-commutativeMonoid : CommutativeMonoid a (a ⊔ ℓ)
++-commutativeMonoid = record
  { isCommutativeMonoid = ++-isCommutativeMonoid
  }

-- Some other useful lemmas

zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t

inject : ∀ (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
         ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)

shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
shifts xs ys {zs} = begin
   xs ++ ys  ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩
  (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
  (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
   ys ++ xs  ++ zs ∎

dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
           ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
           ws ++ ys ↭ xs ++ zs
dropMiddleElement-≋ []       []       (_   ∷ eq) = ≋⇒↭ eq
dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq) = ↭-respˡ-≋ (≋-sym eq) (shift w≈v xs _)
dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq) = ↭-respʳ-≋ eq (↭-sym (shift (≈-sym w≈x) ws _))
dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMiddleElement-≋ ws xs eq)

dropMiddleElement : ∀ {v} ws xs {ys zs} →
                    ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →
                    ws ++ ys ↭ xs ++ zs
dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl
  where
  lemma : ∀ {w x y z} → w ≈ x → x ≈ y → z ≈ y → w ≈ z
  lemma w≈x x≈y z≈y = ≈-trans (≈-trans w≈x x≈y) (≈-sym z≈y)

  open PermutationReasoning

  -- The l′ & l″ could be eliminated at the cost of making the `trans` case
  -- much more difficult to prove. At the very least would require using `Acc`.
  helper : ∀ {l′ l″ : List A} → l′ ↭ l″ →
           ∀ ws xs {ys zs : List A} →
           ws ++ [ v ] ++ ys ≋ l′ →
           xs ++ [ v ] ++ zs ≋ l″ →
           ws ++ ys ↭ xs ++ zs
  helper {as}     {bs}     (refl eq3) ws xs {ys} {zs} eq1 eq2 =
    dropMiddleElement-≋ ws xs (≋-trans (≋-trans eq1 eq3) (≋-sym eq2))
  helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin
    ys               ≋⟨  ys≋as ⟩
    as               ↭⟨  as↭bs ⟩
    bs               ≋˘⟨ zs≋bs ⟩
    zs               ∎
  helper {_ ∷ as} {_ ∷ bs} (prep a≈b as↭bs) [] (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    ys               ≋⟨  ≋₁ ⟩
    as               ↭⟨  as↭bs ⟩
    bs               ≋˘⟨ ≋₂ ⟩
    xs ++ v ∷ zs     ↭⟨  shift (lemma ≈₁ a≈b ≈₂) xs zs ⟩
    x ∷ xs ++ zs     ∎
  helper {_ ∷ as} {_ ∷ bs} (prep v≈w p) (w ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    w ∷ ws ++ ys     ↭⟨  ↭-sym (shift (lemma ≈₂ (≈-sym v≈w) ≈₁) ws ys) ⟩
    ws ++ v ∷ ys     ≋⟨  ≋₁ ⟩
    as               ↭⟨  p ⟩
    bs               ≋˘⟨ ≋₂ ⟩
    zs               ∎
  helper {_ ∷ as} {_ ∷ bs} (prep w≈x p) (w ∷ ws) (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    w ∷ ws ++ ys     ↭⟨ prep (lemma ≈₁ w≈x ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
    x ∷ xs ++ zs     ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈x y≈v p) [] [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    ys               ≋⟨  ≋₁ ⟩
    a ∷ as           ↭⟨  prep (≈-trans (≈-trans (≈-trans y≈v (≈-sym ≈₂)) ≈₁) v≈x) p ⟩
    b ∷ bs           ≋˘⟨ ≋₂ ⟩
    zs               ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    ys               ≋⟨  ≋₁ ⟩
    a ∷ as           ↭⟨  prep y≈w p ⟩
    _ ∷ bs           ≋˘⟨ ≈₂ ∷ tail ≋₂ ⟩
    x ∷ zs           ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    ys               ≋⟨ ≋₁ ⟩
    a ∷ as           ↭⟨ prep y≈x p ⟩
    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
    x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (head ≋₂)) xs zs) ⟩
    x ∷ w ∷ xs ++ zs ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈x _ p) (w ∷ []) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    w ∷ ys           ≋⟨ ≈₁ ∷ tail (≋₁) ⟩
    _ ∷ as           ↭⟨ prep w≈x p ⟩
    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
    zs               ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈y x≈v p) (w ∷ x ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (head ≋₁)) ws ys)) ⟩
    w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
    _ ∷ as           ↭⟨ prep w≈y p ⟩
    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
    zs               ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap x≈v v≈y p) (x ∷ []) (y ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    x ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
    _ ∷ as           ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (head ≋₂)) (≈-trans (head ≋₁) v≈y))) p ⟩
    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
    y ∷ zs           ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈w v≈z p) (y ∷ []) (z ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    y ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
    _ ∷ as           ↭⟨ prep y≈w p ⟩
    _ ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
    w ∷ xs ++ v ∷ zs ↭⟨ ↭-prep w (shift ≈-refl xs zs) ⟩
    w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (head ≋₁) v≈z ≈₂) ↭-refl ⟩
    z ∷ w ∷ xs ++ zs ∎
  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈v w≈z p) (y ∷ w ∷ ws) (z ∷ []) {ys} {zs}    (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
    y ∷ w ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ y≈v (head ≋₂)) ≈-refl ↭-refl ⟩
    w ∷ v ∷ ws ++ ys ↭⟨ ↭-prep w (↭-sym (shift ≈-refl ws ys)) ⟩
    w ∷ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩
    _ ∷ as           ↭⟨ prep w≈z p ⟩
    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
    z ∷ zs           ∎
  helper (swap x≈z y≈w p) (x ∷ y ∷ ws) (w ∷ z ∷ xs) {ys} {zs} (≈₁ ∷ ≈₃ ∷ ≋₁) (≈₂ ∷ ≈₄ ∷ ≋₂) = begin
    x ∷ y ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ x≈z ≈₄) (lemma ≈₃ y≈w ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
    w ∷ z ∷ xs ++ zs ∎
  helper {as} {bs} (trans p₁ p₂) ws xs eq1 eq2
    with ∈-∃++ S (∈-resp-↭ (↭-respˡ-≋ (≋-sym eq1) p₁) (∈-insert S ws ≈-refl))
  ... | (h , t , w , v≈w , eq) = trans
    (helper p₁ ws h eq1 (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)))
    (helper p₂ h xs (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)) eq2)

dropMiddle : ∀ {vs} ws xs {ys zs} →
             ws ++ vs ++ ys ↭ xs ++ vs ++ zs →
             ws ++ ys ↭ xs ++ zs
dropMiddle {[]}     ws xs p = p
dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p)

split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
split v as bs p = helper as bs p (<-wellFounded (steps p))
  where
  helper : ∀ as bs {xs} (p : xs ↭ as ++ [ v ] ++ bs) → Acc _<_ (steps p) →
           ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
  helper []           bs (refl eq)    _ = []         , bs , eq
  helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
  helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
  helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
  ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
  helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
  helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
  ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m<n+m (steps ↭₂) (0<steps ↭₁)))
  ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
    (rec _ (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))

------------------------------------------------------------------------
-- filter

module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where

  filter⁺ : ∀ {xs ys : List A} → xs ↭ ys → filter P? xs ↭ filter P? ys
  filter⁺ (refl xs≋ys)        = refl (≋.filter⁺ P? P≈ xs≋ys)
  filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys)
  filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y
  ... | yes _  | yes _  = prep x≈y (filter⁺ xs↭ys)
  ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py
  ... | no ¬Px | yes Py = contradiction (P≈ (≈-sym x≈y) Py) ¬Px
  ... | no  _  | no  _  = filter⁺ xs↭ys
  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y
  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py
    with P? z | P? w
  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
  ... | no _   | no  _  = filter⁺ xs↭ys
  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py
    with P? z | P? w
  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
  ... | no _   | yes _  = prep w≈y (filter⁺ xs↭ys)
  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys)  | yes Px | no ¬Py
    with P? z | P? w
  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
  ... | yes _  | no _   = prep x≈z (filter⁺ xs↭ys)
  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py
    with P? z | P? w
  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
  ... | yes _  | yes _  = swap x≈z w≈y (filter⁺ xs↭ys)

------------------------------------------------------------------------
-- _∷ʳ_

∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
∷↭∷ʳ x xs = ↭-sym (begin
  xs ++ [ x ]   ↭⟨ shift ≈-refl xs [] ⟩
  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
  x ∷ xs        ∎)
  where open PermutationReasoning


text:
module L.Base.Nat.Properties where

open import L.Base.Nat
open import L.Base.Id.Core
open import L.Base.Id.Properties using (ap;sym;transport)

-- Properties of +
+-idl : ∀{x} → zero + x ≡ x
+-idl = refl

+-idr : ∀{x} → x + zero ≡ x
+-idr {x} = ind (λ n → n + zero ≡ n) refl (λ _ p → ap succ p) x

+-assoc : {x y z : Nat} → (x + y) + z ≡ x + (y + z)
+-assoc {x}{y}{z} = ind (λ n → (n + y) + z ≡ n + (y + z))
          refl (λ _ p → ap succ p) x

+-succ : {x y : Nat} → x + succ y ≡ succ (x + y)
+-succ {x}{y} = ind (λ n → n + succ y ≡ succ (n + y)) refl (λ _ p → ap succ p) x

+-comm : {x y : Nat} → x + y ≡ y + x
+-comm {x}{y} = ind (λ n → n + y ≡ y + n) (sym +-idr) (λ n p → sym
                (transport (λ q → y + succ n ≡ succ q) (sym p) +-succ)) x

-- Properties of *
*-zl : ∀{x} → zero * x ≡ zero
*-zl = refl

*-zr : ∀{x} → x * zero ≡ zero
*-zr {x} = ind (λ n → n * zero ≡ zero) refl (λ _ p → p) x

*-idl : ∀{x} → 1 * x ≡ x
*-idl = +-idr

*-idr : ∀{x} → x * 1 ≡ x
*-idr {x} = ind (λ n → n * 1 ≡ n) refl (λ _ p → ap succ p) x

*-distrib-+ : {x y z : Nat} → (x + y) * z ≡ x * z + y * z
*-distrib-+ {x}{y}{z} = ind (λ n → (n + y) * z ≡ n * z + y * z) refl
                        (λ m p → transport (λ s → z + (m + y) * z ≡ s)
                        (sym (+-assoc {z} {m * z} {y * z}))
                        (ap (λ k → z + k) p)) x

*-assoc : {x y z : Nat} → (x * y) * z ≡ x * (y * z)
*-assoc {x}{y}{z} = ind (λ n → (n * y) * z ≡ n * (y * z)) refl (λ n p
                    → transport (λ q → (y + n * y) * z ≡ y * z + q) p
                    (*-distrib-+ {y}{n * y})) x

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
-- Andreas, 2017-01-12, issue #2386

open import Agda.Primitive

data _≡_ {a b} {A : Set (a ⊔ b)} : (x y : A) → Set where
  refl : (x : A) → x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Should be accepted

-- The type of primErase has to match the flavor of EQUALITY

primitive primEraseEquality : ∀ {a b}{A : Set (a ⊔ b)} {x y : A} → _≡_ x y → _≡_ x y

testTM : ∀ {a b} {A : Set (a ⊔ b)} {x : A} (eq : _≡_ {a} {b} x x) → primEraseEquality {x = x} {y = x} eq ≡ refl _
testTM _ = refl _

-- Testing rewrite

subst : ∀{ℓ}{A : Set ℓ} {P : A → Set}{a b : A} → _≡_ {a = ℓ} {b = ℓ} a b → P a → P b
subst eq p rewrite eq = p

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.DirectSumHIT where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.AbGroup

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.DirectSum.DirectSumHIT.Properties

private variable
  ℓ ℓ' : Level

module _ (Idx : Type ℓ) (P : Idx → Type ℓ') (AGP : (r : Idx) → AbGroupStr (P r)) where

  open AbGroupStr
  open AbGroupProperties Idx P AGP

  ⊕HIT-AbGr : AbGroup (ℓ-max ℓ ℓ')
  fst ⊕HIT-AbGr = ⊕HIT Idx P AGP
  0g (snd ⊕HIT-AbGr) = neutral
  _+_ (snd ⊕HIT-AbGr) = _add_
  - snd ⊕HIT-AbGr = inv
  isAbGroup (snd ⊕HIT-AbGr) = makeIsAbGroup trunc addAssoc addRid rinv addComm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Agda.Primitive
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A : Set ℓ
  P : A → Set ℓ
  x y : A
  f : (x : A) → P x

cong : x ≡ y → f x ≡ f y
cong refl = refl


text:
------------------------------------------------------------------------
-- Descending lists
------------------------------------------------------------------------

{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Foundations.Everything

module Cubical.Data.DescendingList.Base
 (A : Type₀)
 (_≥_ : A → A → Type₀)
 where

------------------------------------------------------------------------
-- Descending lists
--
-- Defined simultaneously with the relation "x ≥ the HEAD of u"

data DL : Type₀
data _≥ᴴ_ (x : A) : DL → Type₀

data DL where
 []   : DL
 cons : (x : A) (u : DL) → x ≥ᴴ u → DL

data _≥ᴴ_ x where
 ≥ᴴ[]   : x ≥ᴴ []
 ≥ᴴcons : {y : A} {u : DL} {r : y ≥ᴴ u}
         → x ≥ y → x ≥ᴴ (cons y u r)

[_] : A → DL
[ x ] = cons x [] ≥ᴴ[]

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Covec
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Codata.Covec.Categorical where

open import Codata.Conat
open import Codata.Covec

open import Category.Functor
open import Category.Applicative

functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i)
functor = record { _<$>_ = map }

applicative : ∀ {ℓ i n} → RawApplicative {ℓ} (λ A → Covec A n i)
applicative = record
  { pure = replicate _
  ; _⊛_  = ap
  }


text:
{-# OPTIONS --without-K --exact-split --safe #-}

open import Fragment.Equational.Theory.Base

module Fragment.Equational.Theory.Combinators (Θ : Theory) where

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Properties
open import Fragment.Equational.Model
  using (Model; IsModel; Models)
open import Fragment.Equational.Model.Satisfaction

open import Level using (Level)
open import Function using (_∘_)

open import Data.Nat using (ℕ)

private
  variable
    a ℓ : Level

{-
forgetₒ' : ∀ {O} → Model (Θ ⦅ O ⦆ₒ) {a} {ℓ} → Model Θ {a} {ℓ}
forgetₒ' {O = O} A =
  record { ∥_∥/≈   = ∥ A ∥/≈
         ; isModel = forget-isModel
         }
  where open import Fragment.Equational.Model (Θ ⦅ O ⦆ₒ)
          using (∥_∥/≈; ∥_∥ₐ; ∥_∥ₐ-models)
        open import Fragment.Algebra.Algebra (Σ Θ)
          using (∥_∥/≈-isAlgebra)

        forget-⊨ : ∀ {θ eq} → ∥ A ∥ₐ ⊨⟨ θ ⟩ ((Θ ⦅ O ⦆ₒ) ⟦ {!oldₑ!} ⟧ₑ)
                            → forgetₒ ∥ A ∥ₐ ⊨⟨ θ ⟩ (Θ ⟦ eq ⟧ₑ)
        forget-⊨ = {!!}

        forget-models : Models Θ (forgetₒ ∥ A ∥ₐ)
        forget-models eq θ = {!!}

        forget-isModel : IsModel Θ ∥ A ∥/≈
        forget-isModel =
          record { isAlgebra = ∥ (forgetₒ ∥ A ∥ₐ) ∥/≈-isAlgebra
                 ; models    = forget-models
                 }

forgetₑ : ∀ {O E}
          → {X : ∀ {n} → E n → Eq ((Σ Θ) ⦅ O ⦆) n}
          → Model (Θ ⦅ O ∣ E / X ⦆) {a} {ℓ}
          → Model Θ {a} {ℓ}
forgetₑ {O = O} {E} {X} A =
  record { ∥_∥/≈   = {!!}
         ; isModel = {!!}
         }
-}

data HomOp : ℕ → Set where
  h : HomOp 1

data HomEq : ℕ → Set where
  hom : ∀ {n} → ops (Σ Θ) n → HomEq n

AddHom : Theory
AddHom = Θ ⦅ HomOp ∣ HomEq / hom' ⦆
  where import Fragment.Equational.Theory.Laws ((Σ Θ) ⦅ HomOp ⦆) as L

        hom' : ∀ {arity} → HomEq arity → Eq ((Σ Θ) ⦅ HomOp ⦆) arity
        hom' (hom f) = L.hom (newₒ h) (oldₒ f)

data IdOp : ℕ → Set where
  α : IdOp 0

data IdEq : ℕ → Set where
  idₗ : IdEq 1
  idᵣ : IdEq 1

AddId : ops (Σ Θ) 2 → Theory
AddId • = Θ ⦅ IdOp ∣ IdEq / id ⦆
  where import Fragment.Equational.Theory.Laws ((Σ Θ) ⦅ IdOp ⦆) as L

        id : ∀ {arity} → IdEq arity → Eq ((Σ Θ) ⦅ IdOp ⦆) arity
        id idₗ = L.idₗ (newₒ α) (oldₒ •)
        id idᵣ = L.idᵣ (newₒ α) (oldₒ •)

data AnOp : ℕ → Set where
  ω : AnOp 0

data AnEq : ℕ → Set where
  anₗ : AnEq 1
  anᵣ : AnEq 1

AddAn : ops (Σ Θ) 2 → Theory
AddAn • = Θ ⦅ AnOp ∣ AnEq / an ⦆
  where import Fragment.Equational.Theory.Laws ((Σ Θ) ⦅ AnOp ⦆) as L

        an : ∀ {arity} → AnEq arity → Eq ((Σ Θ) ⦅ AnOp ⦆) arity
        an anₗ = L.anₗ (newₒ ω) (oldₒ •)
        an anᵣ = L.anᵣ (newₒ ω) (oldₒ •)

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --type-in-type #-}

Ty : Set
Ty =
   (Ty         : Set)
   (nat top bot  : Ty)
   (arr prod sum : Ty → Ty → Ty)
 → Ty

nat : Ty; nat = λ _ nat _ _ _ _ _ → nat
top : Ty; top = λ _ _ top _ _ _ _ → top
bot : Ty; bot = λ _ _ _ bot _ _ _ → bot

arr : Ty → Ty → Ty; arr
 = λ A B Ty nat top bot arr prod sum →
     arr (A Ty nat top bot arr prod sum) (B Ty nat top bot arr prod sum)

prod : Ty → Ty → Ty; prod
 = λ A B Ty nat top bot arr prod sum →
     prod (A Ty nat top bot arr prod sum) (B Ty nat top bot arr prod sum)

sum : Ty → Ty → Ty; sum
 = λ A B Ty nat top bot arr prod sum →
     sum (A Ty nat top bot arr prod sum) (B Ty nat top bot arr prod sum)

Con : Set; Con
 = (Con : Set)
   (nil  : Con)
   (snoc : Con → Ty → Con)
 → Con

nil : Con; nil
 = λ Con nil snoc → nil

snoc : Con → Ty → Con; snoc
 = λ Γ A Con nil snoc → snoc (Γ Con nil snoc) A

Var : Con → Ty → Set; Var
 = λ Γ A →
   (Var : Con → Ty → Set)
   (vz  : ∀{Γ A} → Var (snoc Γ A) A)
   (vs  : ∀{Γ B A} → Var Γ A → Var (snoc Γ B) A)
 → Var Γ A

vz : ∀{Γ A} → Var (snoc Γ A) A; vz
 = λ Var vz vs → vz

vs : ∀{Γ B A} → Var Γ A → Var (snoc Γ B) A; vs
 = λ x Var vz vs → vs (x Var vz vs)

Tm : Con → Ty → Set; Tm
 = λ Γ A →
   (Tm  : Con → Ty → Set)
   (var   : ∀{Γ A} → Var Γ A → Tm Γ A)
   (lam   : ∀{Γ A B} → Tm (snoc Γ A) B → Tm Γ (arr A B))
   (app   : ∀{Γ A B} → Tm Γ (arr A B) → Tm Γ A → Tm Γ B)
   (tt    : ∀{Γ} → Tm Γ top)
   (pair  : ∀{Γ A B} → Tm Γ A → Tm Γ B → Tm Γ (prod A B))
   (fst   : ∀{Γ A B} → Tm Γ (prod A B) → Tm Γ A)
   (snd   : ∀{Γ A B} → Tm Γ (prod A B) → Tm Γ B)
   (left  : ∀{Γ A B} → Tm Γ A → Tm Γ (sum A B))
   (right : ∀{Γ A B} → Tm Γ B → Tm Γ (sum A B))
   (case  : ∀{Γ A B C} → Tm Γ (sum A B) → Tm Γ (arr A C) → Tm Γ (arr B C) → Tm Γ C)
   (zero  : ∀{Γ} → Tm Γ nat)
   (suc   : ∀{Γ} → Tm Γ nat → Tm Γ nat)
   (rec   : ∀{Γ A} → Tm Γ nat → Tm Γ (arr nat (arr A A)) → Tm Γ A → Tm Γ A)
 → Tm Γ A

var : ∀{Γ A} → Var Γ A → Tm Γ A; var
 = λ x Tm var lam app tt pair fst snd left right case zero suc rec →
     var x

lam : ∀{Γ A B} → Tm (snoc Γ A) B → Tm Γ (arr A B); lam
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
     lam (t Tm var lam app tt pair fst snd left right case zero suc rec)

app : ∀{Γ A B} → Tm Γ (arr A B) → Tm Γ A → Tm Γ B; app
 = λ t u Tm var lam app tt pair fst snd left right case zero suc rec →
     app (t Tm var lam app tt pair fst snd left right case zero suc rec)
         (u Tm var lam app tt pair fst snd left right case zero suc rec)

tt : ∀{Γ} → Tm Γ top; tt
 = λ Tm var lam app tt pair fst snd left right case zero suc rec → tt

pair : ∀{Γ A B} → Tm Γ A → Tm Γ B → Tm Γ (prod A B); pair
 = λ t u Tm var lam app tt pair fst snd left right case zero suc rec →
     pair (t Tm var lam app tt pair fst snd left right case zero suc rec)
          (u Tm var lam app tt pair fst snd left right case zero suc rec)

fst : ∀{Γ A B} → Tm Γ (prod A B) → Tm Γ A; fst
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
     fst (t Tm var lam app tt pair fst snd left right case zero suc rec)

snd : ∀{Γ A B} → Tm Γ (prod A B) → Tm Γ B; snd
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
     snd (t Tm var lam app tt pair fst snd left right case zero suc rec)

left : ∀{Γ A B} → Tm Γ A → Tm Γ (sum A B); left
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
     left (t Tm var lam app tt pair fst snd left right case zero suc rec)

right : ∀{Γ A B} → Tm Γ B → Tm Γ (sum A B); right
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
     right (t Tm var lam app tt pair fst snd left right case zero suc rec)

case : ∀{Γ A B C} → Tm Γ (sum A B) → Tm Γ (arr A C) → Tm Γ (arr B C) → Tm Γ C; case
 = λ t u v Tm var lam app tt pair fst snd left right case zero suc rec →
     case (t Tm var lam app tt pair fst snd left right case zero suc rec)
           (u Tm var lam app tt pair fst snd left right case zero suc rec)
           (v Tm var lam app tt pair fst snd left right case zero suc rec)

zero  : ∀{Γ} → Tm Γ nat; zero
 = λ Tm var lam app tt pair fst snd left right case zero suc rec → zero

suc : ∀{Γ} → Tm Γ nat → Tm Γ nat; suc
 = λ t Tm var lam app tt pair fst snd left right case zero suc rec →
   suc (t Tm var lam app tt pair fst snd left right case zero suc rec)

rec : ∀{Γ A} → Tm Γ nat → Tm Γ (arr nat (arr A A)) → Tm Γ A → Tm Γ A; rec
 = λ t u v Tm var lam app tt pair fst snd left right case zero suc rec →
     rec (t Tm var lam app tt pair fst snd left right case zero suc rec)
         (u Tm var lam app tt pair fst snd left right case zero suc rec)
         (v Tm var lam app tt pair fst snd left right case zero suc rec)

v0 : ∀{Γ A} → Tm (snoc Γ A) A; v0
 = var vz

v1 : ∀{Γ A B} → Tm (snoc (snoc Γ A) B) A; v1
 = var (vs vz)

v2 : ∀{Γ A B C} → Tm (snoc (snoc (snoc Γ A) B) C) A; v2
 = var (vs (vs vz))

v3 : ∀{Γ A B C D} → Tm (snoc (snoc (snoc (snoc Γ A) B) C) D) A; v3
 = var (vs (vs (vs vz)))

tbool : Ty; tbool
 = sum top top

true : ∀{Γ} → Tm Γ tbool; true
 = left tt

tfalse : ∀{Γ} → Tm Γ tbool; tfalse
 = right tt

ifthenelse : ∀{Γ A} → Tm Γ (arr tbool (arr A (arr A A))); ifthenelse
 = lam (lam (lam (case v2 (lam v2) (lam v1))))

times4 : ∀{Γ A} → Tm Γ (arr (arr A A) (arr A A)); times4
  = lam (lam (app v1 (app v1 (app v1 (app v1 v0)))))

add : ∀{Γ} → Tm Γ (arr nat (arr nat nat)); add
 = lam (rec v0
       (lam (lam (lam (suc (app v1 v0)))))
       (lam v0))

mul : ∀{Γ} → Tm Γ (arr nat (arr nat nat)); mul
 = lam (rec v0
       (lam (lam (lam (app (app add (app v1 v0)) v0))))
       (lam zero))

fact : ∀{Γ} → Tm Γ (arr nat nat); fact
 = lam (rec v0 (lam (lam (app (app mul (suc v1)) v0)))
        (suc zero))
{-# OPTIONS --type-in-type #-}

Ty1 : Set
Ty1 =
   (Ty1         : Set)
   (nat top bot  : Ty1)
   (arr prod sum : Ty1 → Ty1 → Ty1)
 → Ty1

nat1 : Ty1; nat1 = λ _ nat1 _ _ _ _ _ → nat1
top1 : Ty1; top1 = λ _ _ top1 _ _ _ _ → top1
bot1 : Ty1; bot1 = λ _ _ _ bot1 _ _ _ → bot1

arr1 : Ty1 → Ty1 → Ty1; arr1
 = λ A B Ty1 nat1 top1 bot1 arr1 prod sum →
     arr1 (A Ty1 nat1 top1 bot1 arr1 prod sum) (B Ty1 nat1 top1 bot1 arr1 prod sum)

prod1 : Ty1 → Ty1 → Ty1; prod1
 = λ A B Ty1 nat1 top1 bot1 arr1 prod1 sum →
     prod1 (A Ty1 nat1 top1 bot1 arr1 prod1 sum) (B Ty1 nat1 top1 bot1 arr1 prod1 sum)

sum1 : Ty1 → Ty1 → Ty1; sum1
 = λ A B Ty1 nat1 top1 bot1 arr1 prod1 sum1 →
     sum1 (A Ty1 nat1 top1 bot1 arr1 prod1 sum1) (B Ty1 nat1 top1 bot1 arr1 prod1 sum1)

Con1 : Set; Con1
 = (Con1 : Set)
   (nil  : Con1)
   (snoc : Con1 → Ty1 → Con1)
 → Con1

nil1 : Con1; nil1
 = λ Con1 nil1 snoc → nil1

snoc1 : Con1 → Ty1 → Con1; snoc1
 = λ Γ A Con1 nil1 snoc1 → snoc1 (Γ Con1 nil1 snoc1) A

Var1 : Con1 → Ty1 → Set; Var1
 = λ Γ A →
   (Var1 : Con1 → Ty1 → Set)
   (vz  : ∀{Γ A} → Var1 (snoc1 Γ A) A)
   (vs  : ∀{Γ B A} → Var1 Γ A → Var1 (snoc1 Γ B) A)
 → Var1 Γ A

vz1 : ∀{Γ A} → Var1 (snoc1 Γ A) A; vz1
 = λ Var1 vz1 vs → vz1

vs1 : ∀{Γ B A} → Var1 Γ A → Var1 (snoc1 Γ B) A; vs1
 = λ x Var1 vz1 vs1 → vs1 (x Var1 vz1 vs1)

Tm1 : Con1 → Ty1 → Set; Tm1
 = λ Γ A →
   (Tm1  : Con1 → Ty1 → Set)
   (var   : ∀{Γ A} → Var1 Γ A → Tm1 Γ A)
   (lam   : ∀{Γ A B} → Tm1 (snoc1 Γ A) B → Tm1 Γ (arr1 A B))
   (app   : ∀{Γ A B} → Tm1 Γ (arr1 A B) → Tm1 Γ A → Tm1 Γ B)
   (tt    : ∀{Γ} → Tm1 Γ top1)
   (pair  : ∀{Γ A B} → Tm1 Γ A → Tm1 Γ B → Tm1 Γ (prod1 A B))
   (fst   : ∀{Γ A B} → Tm1 Γ (prod1 A B) → Tm1 Γ A)
   (snd   : ∀{Γ A B} → Tm1 Γ (prod1 A B) → Tm1 Γ B)
   (left  : ∀{Γ A B} → Tm1 Γ A → Tm1 Γ (sum1 A B))
   (right : ∀{Γ A B} → Tm1 Γ B → Tm1 Γ (sum1 A B))
   (case  : ∀{Γ A B C} → Tm1 Γ (sum1 A B) → Tm1 Γ (arr1 A C) → Tm1 Γ (arr1 B C) → Tm1 Γ C)
   (zero  : ∀{Γ} → Tm1 Γ nat1)
   (suc   : ∀{Γ} → Tm1 Γ nat1 → Tm1 Γ nat1)
   (rec   : ∀{Γ A} → Tm1 Γ nat1 → Tm1 Γ (arr1 nat1 (arr1 A A)) → Tm1 Γ A → Tm1 Γ A)
 → Tm1 Γ A

var1 : ∀{Γ A} → Var1 Γ A → Tm1 Γ A; var1
 = λ x Tm1 var1 lam app tt pair fst snd left right case zero suc rec →
     var1 x

lam1 : ∀{Γ A B} → Tm1 (snoc1 Γ A) B → Tm1 Γ (arr1 A B); lam1
 = λ t Tm1 var1 lam1 app tt pair fst snd left right case zero suc rec →
     lam1 (t Tm1 var1 lam1 app tt pair fst snd left right case zero suc rec)

app1 : ∀{Γ A B} → Tm1 Γ (arr1 A B) → Tm1 Γ A → Tm1 Γ B; app1
 = λ t u Tm1 var1 lam1 app1 tt pair fst snd left right case zero suc rec →
     app1 (t Tm1 var1 lam1 app1 tt pair fst snd left right case zero suc rec)
         (u Tm1 var1 lam1 app1 tt pair fst snd left right case zero suc rec)

tt1 : ∀{Γ} → Tm1 Γ top1; tt1
 = λ Tm1 var1 lam1 app1 tt1 pair fst snd left right case zero suc rec → tt1

pair1 : ∀{Γ A B} → Tm1 Γ A → Tm1 Γ B → Tm1 Γ (prod1 A B); pair1
 = λ t u Tm1 var1 lam1 app1 tt1 pair1 fst snd left right case zero suc rec →
     pair1 (t Tm1 var1 lam1 app1 tt1 pair1 fst snd left right case zero suc rec)
          (u Tm1 var1 lam1 app1 tt1 pair1 fst snd left right case zero suc rec)

fst1 : ∀{Γ A B} → Tm1 Γ (prod1 A B) → Tm1 Γ A; fst1
 = λ t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd left right case zero suc rec →
     fst1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd left right case zero suc rec)

snd1 : ∀{Γ A B} → Tm1 Γ (prod1 A B) → Tm1 Γ B; snd1
 = λ t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left right case zero suc rec →
     snd1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left right case zero suc rec)

left1 : ∀{Γ A B} → Tm1 Γ A → Tm1 Γ (sum1 A B); left1
 = λ t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right case zero suc rec →
     left1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right case zero suc rec)

right1 : ∀{Γ A B} → Tm1 Γ B → Tm1 Γ (sum1 A B); right1
 = λ t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case zero suc rec →
     right1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case zero suc rec)

case1 : ∀{Γ A B C} → Tm1 Γ (sum1 A B) → Tm1 Γ (arr1 A C) → Tm1 Γ (arr1 B C) → Tm1 Γ C; case1
 = λ t u v Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero suc rec →
     case1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero suc rec)
           (u Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero suc rec)
           (v Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero suc rec)

zero1  : ∀{Γ} → Tm1 Γ nat1; zero1
 = λ Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc rec → zero1

suc1 : ∀{Γ} → Tm1 Γ nat1 → Tm1 Γ nat1; suc1
 = λ t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec →
   suc1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec)

rec1 : ∀{Γ A} → Tm1 Γ nat1 → Tm1 Γ (arr1 nat1 (arr1 A A)) → Tm1 Γ A → Tm1 Γ A; rec1
 = λ t u v Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec1 →
     rec1 (t Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec1)
         (u Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec1)
         (v Tm1 var1 lam1 app1 tt1 pair1 fst1 snd1 left1 right1 case1 zero1 suc1 rec1)

v01 : ∀{Γ A} → Tm1 (snoc1 Γ A) A; v01
 = var1 vz1

v11 : ∀{Γ A B} → Tm1 (snoc1 (snoc1 Γ A) B) A; v11
 = var1 (vs1 vz1)

v21 : ∀{Γ A B C} → Tm1 (snoc1 (snoc1 (snoc1 Γ A) B) C) A; v21
 = var1 (vs1 (vs1 vz1))

v31 : ∀{Γ A B C D} → Tm1 (snoc1 (snoc1 (snoc1 (snoc1 Γ A) B) C) D) A; v31
 = var1 (vs1 (vs1 (vs1 vz1)))

tbool1 : Ty1; tbool1
 = sum1 top1 top1

true1 : ∀{Γ} → Tm1 Γ tbool1; true1
 = left1 tt1

tfalse1 : ∀{Γ} → Tm1 Γ tbool1; tfalse1
 = right1 tt1

ifthenelse1 : ∀{Γ A} → Tm1 Γ (arr1 tbool1 (arr1 A (arr1 A A))); ifthenelse1
 = lam1 (lam1 (lam1 (case1 v21 (lam1 v21) (lam1 v11))))

times41 : ∀{Γ A} → Tm1 Γ (arr1 (arr1 A A) (arr1 A A)); times41
  = lam1 (lam1 (app1 v11 (app1 v11 (app1 v11 (app1 v11 v01)))))

add1 : ∀{Γ} → Tm1 Γ (arr1 nat1 (arr1 nat1 nat1)); add1
 = lam1 (rec1 v01
       (lam1 (lam1 (lam1 (suc1 (app1 v11 v01)))))
       (lam1 v01))

mul1 : ∀{Γ} → Tm1 Γ (arr1 nat1 (arr1 nat1 nat1)); mul1
 = lam1 (rec1 v01
       (lam1 (lam1 (lam1 (app1 (app1 add1 (app1 v11 v01)) v01))))
       (lam1 zero1))

fact1 : ∀{Γ} → Tm1 Γ (arr1 nat1 nat1); fact1
 = lam1 (rec1 v01 (lam1 (lam1 (app1 (app1 mul1 (suc1 v11)) v01)))
        (suc1 zero1))
{-# OPTIONS --type-in-type #-}

Ty2 : Set
Ty2 =
   (Ty2         : Set)
   (nat top bot  : Ty2)
   (arr prod sum : Ty2 → Ty2 → Ty2)
 → Ty2

nat2 : Ty2; nat2 = λ _ nat2 _ _ _ _ _ → nat2
top2 : Ty2; top2 = λ _ _ top2 _ _ _ _ → top2
bot2 : Ty2; bot2 = λ _ _ _ bot2 _ _ _ → bot2

arr2 : Ty2 → Ty2 → Ty2; arr2
 = λ A B Ty2 nat2 top2 bot2 arr2 prod sum →
     arr2 (A Ty2 nat2 top2 bot2 arr2 prod sum) (B Ty2 nat2 top2 bot2 arr2 prod sum)

prod2 : Ty2 → Ty2 → Ty2; prod2
 = λ A B Ty2 nat2 top2 bot2 arr2 prod2 sum →
     prod2 (A Ty2 nat2 top2 bot2 arr2 prod2 sum) (B Ty2 nat2 top2 bot2 arr2 prod2 sum)

sum2 : Ty2 → Ty2 → Ty2; sum2
 = λ A B Ty2 nat2 top2 bot2 arr2 prod2 sum2 →
     sum2 (A Ty2 nat2 top2 bot2 arr2 prod2 sum2) (B Ty2 nat2 top2 bot2 arr2 prod2 sum2)

Con2 : Set; Con2
 = (Con2 : Set)
   (nil  : Con2)
   (snoc : Con2 → Ty2 → Con2)
 → Con2

nil2 : Con2; nil2
 = λ Con2 nil2 snoc → nil2

snoc2 : Con2 → Ty2 → Con2; snoc2
 = λ Γ A Con2 nil2 snoc2 → snoc2 (Γ Con2 nil2 snoc2) A

Var2 : Con2 → Ty2 → Set; Var2
 = λ Γ A →
   (Var2 : Con2 → Ty2 → Set)
   (vz  : ∀{Γ A} → Var2 (snoc2 Γ A) A)
   (vs  : ∀{Γ B A} → Var2 Γ A → Var2 (snoc2 Γ B) A)
 → Var2 Γ A

vz2 : ∀{Γ A} → Var2 (snoc2 Γ A) A; vz2
 = λ Var2 vz2 vs → vz2

vs2 : ∀{Γ B A} → Var2 Γ A → Var2 (snoc2 Γ B) A; vs2
 = λ x Var2 vz2 vs2 → vs2 (x Var2 vz2 vs2)

Tm2 : Con2 → Ty2 → Set; Tm2
 = λ Γ A →
   (Tm2  : Con2 → Ty2 → Set)
   (var   : ∀{Γ A} → Var2 Γ A → Tm2 Γ A)
   (lam   : ∀{Γ A B} → Tm2 (snoc2 Γ A) B → Tm2 Γ (arr2 A B))
   (app   : ∀{Γ A B} → Tm2 Γ (arr2 A B) → Tm2 Γ A → Tm2 Γ B)
   (tt    : ∀{Γ} → Tm2 Γ top2)
   (pair  : ∀{Γ A B} → Tm2 Γ A → Tm2 Γ B → Tm2 Γ (prod2 A B))
   (fst   : ∀{Γ A B} → Tm2 Γ (prod2 A B) → Tm2 Γ A)
   (snd   : ∀{Γ A B} → Tm2 Γ (prod2 A B) → Tm2 Γ B)
   (left  : ∀{Γ A B} → Tm2 Γ A → Tm2 Γ (sum2 A B))
   (right : ∀{Γ A B} → Tm2 Γ B → Tm2 Γ (sum2 A B))
   (case  : ∀{Γ A B C} → Tm2 Γ (sum2 A B) → Tm2 Γ (arr2 A C) → Tm2 Γ (arr2 B C) → Tm2 Γ C)
   (zero  : ∀{Γ} → Tm2 Γ nat2)
   (suc   : ∀{Γ} → Tm2 Γ nat2 → Tm2 Γ nat2)
   (rec   : ∀{Γ A} → Tm2 Γ nat2 → Tm2 Γ (arr2 nat2 (arr2 A A)) → Tm2 Γ A → Tm2 Γ A)
 → Tm2 Γ A

var2 : ∀{Γ A} → Var2 Γ A → Tm2 Γ A; var2
 = λ x Tm2 var2 lam app tt pair fst snd left right case zero suc rec →
     var2 x

lam2 : ∀{Γ A B} → Tm2 (snoc2 Γ A) B → Tm2 Γ (arr2 A B); lam2
 = λ t Tm2 var2 lam2 app tt pair fst snd left right case zero suc rec →
     lam2 (t Tm2 var2 lam2 app tt pair fst snd left right case zero suc rec)

app2 : ∀{Γ A B} → Tm2 Γ (arr2 A B) → Tm2 Γ A → Tm2 Γ B; app2
 = λ t u Tm2 var2 lam2 app2 tt pair fst snd left right case zero suc rec →
     app2 (t Tm2 var2 lam2 app2 tt pair fst snd left right case zero suc rec)
         (u Tm2 var2 lam2 app2 tt pair fst snd left right case zero suc rec)

tt2 : ∀{Γ} → Tm2 Γ top2; tt2
 = λ Tm2 var2 lam2 app2 tt2 pair fst snd left right case zero suc rec → tt2

pair2 : ∀{Γ A B} → Tm2 Γ A → Tm2 Γ B → Tm2 Γ (prod2 A B); pair2
 = λ t u Tm2 var2 lam2 app2 tt2 pair2 fst snd left right case zero suc rec →
     pair2 (t Tm2 var2 lam2 app2 tt2 pair2 fst snd left right case zero suc rec)
          (u Tm2 var2 lam2 app2 tt2 pair2 fst snd left right case zero suc rec)

fst2 : ∀{Γ A B} → Tm2 Γ (prod2 A B) → Tm2 Γ A; fst2
 = λ t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd left right case zero suc rec →
     fst2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd left right case zero suc rec)

snd2 : ∀{Γ A B} → Tm2 Γ (prod2 A B) → Tm2 Γ B; snd2
 = λ t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left right case zero suc rec →
     snd2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left right case zero suc rec)

left2 : ∀{Γ A B} → Tm2 Γ A → Tm2 Γ (sum2 A B); left2
 = λ t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right case zero suc rec →
     left2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right case zero suc rec)

right2 : ∀{Γ A B} → Tm2 Γ B → Tm2 Γ (sum2 A B); right2
 = λ t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case zero suc rec →
     right2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case zero suc rec)

case2 : ∀{Γ A B C} → Tm2 Γ (sum2 A B) → Tm2 Γ (arr2 A C) → Tm2 Γ (arr2 B C) → Tm2 Γ C; case2
 = λ t u v Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero suc rec →
     case2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero suc rec)
           (u Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero suc rec)
           (v Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero suc rec)

zero2  : ∀{Γ} → Tm2 Γ nat2; zero2
 = λ Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc rec → zero2

suc2 : ∀{Γ} → Tm2 Γ nat2 → Tm2 Γ nat2; suc2
 = λ t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec →
   suc2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec)

rec2 : ∀{Γ A} → Tm2 Γ nat2 → Tm2 Γ (arr2 nat2 (arr2 A A)) → Tm2 Γ A → Tm2 Γ A; rec2
 = λ t u v Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec2 →
     rec2 (t Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec2)
         (u Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec2)
         (v Tm2 var2 lam2 app2 tt2 pair2 fst2 snd2 left2 right2 case2 zero2 suc2 rec2)

v02 : ∀{Γ A} → Tm2 (snoc2 Γ A) A; v02
 = var2 vz2

v12 : ∀{Γ A B} → Tm2 (snoc2 (snoc2 Γ A) B) A; v12
 = var2 (vs2 vz2)

v22 : ∀{Γ A B C} → Tm2 (snoc2 (snoc2 (snoc2 Γ A) B) C) A; v22
 = var2 (vs2 (vs2 vz2))

v32 : ∀{Γ A B C D} → Tm2 (snoc2 (snoc2 (snoc2 (snoc2 Γ A) B) C) D) A; v32
 = var2 (vs2 (vs2 (vs2 vz2)))

tbool2 : Ty2; tbool2
 = sum2 top2 top2

true2 : ∀{Γ} → Tm2 Γ tbool2; true2
 = left2 tt2

tfalse2 : ∀{Γ} → Tm2 Γ tbool2; tfalse2
 = right2 tt2

ifthenelse2 : ∀{Γ A} → Tm2 Γ (arr2 tbool2 (arr2 A (arr2 A A))); ifthenelse2
 = lam2 (lam2 (lam2 (case2 v22 (lam2 v22) (lam2 v12))))

times42 : ∀{Γ A} → Tm2 Γ (arr2 (arr2 A A) (arr2 A A)); times42
  = lam2 (lam2 (app2 v12 (app2 v12 (app2 v12 (app2 v12 v02)))))

add2 : ∀{Γ} → Tm2 Γ (arr2 nat2 (arr2 nat2 nat2)); add2
 = lam2 (rec2 v02
       (lam2 (lam2 (lam2 (suc2 (app2 v12 v02)))))
       (lam2 v02))

mul2 : ∀{Γ} → Tm2 Γ (arr2 nat2 (arr2 nat2 nat2)); mul2
 = lam2 (rec2 v02
       (lam2 (lam2 (lam2 (app2 (app2 add2 (app2 v12 v02)) v02))))
       (lam2 zero2))

fact2 : ∀{Γ} → Tm2 Γ (arr2 nat2 nat2); fact2
 = lam2 (rec2 v02 (lam2 (lam2 (app2 (app2 mul2 (suc2 v12)) v02)))
        (suc2 zero2))
{-# OPTIONS --type-in-type #-}

Ty3 : Set
Ty3 =
   (Ty3         : Set)
   (nat top bot  : Ty3)
   (arr prod sum : Ty3 → Ty3 → Ty3)
 → Ty3

nat3 : Ty3; nat3 = λ _ nat3 _ _ _ _ _ → nat3
top3 : Ty3; top3 = λ _ _ top3 _ _ _ _ → top3
bot3 : Ty3; bot3 = λ _ _ _ bot3 _ _ _ → bot3

arr3 : Ty3 → Ty3 → Ty3; arr3
 = λ A B Ty3 nat3 top3 bot3 arr3 prod sum →
     arr3 (A Ty3 nat3 top3 bot3 arr3 prod sum) (B Ty3 nat3 top3 bot3 arr3 prod sum)

prod3 : Ty3 → Ty3 → Ty3; prod3
 = λ A B Ty3 nat3 top3 bot3 arr3 prod3 sum →
     prod3 (A Ty3 nat3 top3 bot3 arr3 prod3 sum) (B Ty3 nat3 top3 bot3 arr3 prod3 sum)

sum3 : Ty3 → Ty3 → Ty3; sum3
 = λ A B Ty3 nat3 top3 bot3 arr3 prod3 sum3 →
     sum3 (A Ty3 nat3 top3 bot3 arr3 prod3 sum3) (B Ty3 nat3 top3 bot3 arr3 prod3 sum3)

Con3 : Set; Con3
 = (Con3 : Set)
   (nil  : Con3)
   (snoc : Con3 → Ty3 → Con3)
 → Con3

nil3 : Con3; nil3
 = λ Con3 nil3 snoc → nil3

snoc3 : Con3 → Ty3 → Con3; snoc3
 = λ Γ A Con3 nil3 snoc3 → snoc3 (Γ Con3 nil3 snoc3) A

Var3 : Con3 → Ty3 → Set; Var3
 = λ Γ A →
   (Var3 : Con3 → Ty3 → Set)
   (vz  : ∀{Γ A} → Var3 (snoc3 Γ A) A)
   (vs  : ∀{Γ B A} → Var3 Γ A → Var3 (snoc3 Γ B) A)
 → Var3 Γ A

vz3 : ∀{Γ A} → Var3 (snoc3 Γ A) A; vz3
 = λ Var3 vz3 vs → vz3

vs3 : ∀{Γ B A} → Var3 Γ A → Var3 (snoc3 Γ B) A; vs3
 = λ x Var3 vz3 vs3 → vs3 (x Var3 vz3 vs3)

Tm3 : Con3 → Ty3 → Set; Tm3
 = λ Γ A →
   (Tm3  : Con3 → Ty3 → Set)
   (var   : ∀{Γ A} → Var3 Γ A → Tm3 Γ A)
   (lam   : ∀{Γ A B} → Tm3 (snoc3 Γ A) B → Tm3 Γ (arr3 A B))
   (app   : ∀{Γ A B} → Tm3 Γ (arr3 A B) → Tm3 Γ A → Tm3 Γ B)
   (tt    : ∀{Γ} → Tm3 Γ top3)
   (pair  : ∀{Γ A B} → Tm3 Γ A → Tm3 Γ B → Tm3 Γ (prod3 A B))
   (fst   : ∀{Γ A B} → Tm3 Γ (prod3 A B) → Tm3 Γ A)
   (snd   : ∀{Γ A B} → Tm3 Γ (prod3 A B) → Tm3 Γ B)
   (left  : ∀{Γ A B} → Tm3 Γ A → Tm3 Γ (sum3 A B))
   (right : ∀{Γ A B} → Tm3 Γ B → Tm3 Γ (sum3 A B))
   (case  : ∀{Γ A B C} → Tm3 Γ (sum3 A B) → Tm3 Γ (arr3 A C) → Tm3 Γ (arr3 B C) → Tm3 Γ C)
   (zero  : ∀{Γ} → Tm3 Γ nat3)
   (suc   : ∀{Γ} → Tm3 Γ nat3 → Tm3 Γ nat3)
   (rec   : ∀{Γ A} → Tm3 Γ nat3 → Tm3 Γ (arr3 nat3 (arr3 A A)) → Tm3 Γ A → Tm3 Γ A)
 → Tm3 Γ A

var3 : ∀{Γ A} → Var3 Γ A → Tm3 Γ A; var3
 = λ x Tm3 var3 lam app tt pair fst snd left right case zero suc rec →
     var3 x

lam3 : ∀{Γ A B} → Tm3 (snoc3 Γ A) B → Tm3 Γ (arr3 A B); lam3
 = λ t Tm3 var3 lam3 app tt pair fst snd left right case zero suc rec →
     lam3 (t Tm3 var3 lam3 app tt pair fst snd left right case zero suc rec)

app3 : ∀{Γ A B} → Tm3 Γ (arr3 A B) → Tm3 Γ A → Tm3 Γ B; app3
 = λ t u Tm3 var3 lam3 app3 tt pair fst snd left right case zero suc rec →
     app3 (t Tm3 var3 lam3 app3 tt pair fst snd left right case zero suc rec)
         (u Tm3 var3 lam3 app3 tt pair fst snd left right case zero suc rec)

tt3 : ∀{Γ} → Tm3 Γ top3; tt3
 = λ Tm3 var3 lam3 app3 tt3 pair fst snd left right case zero suc rec → tt3

pair3 : ∀{Γ A B} → Tm3 Γ A → Tm3 Γ B → Tm3 Γ (prod3 A B); pair3
 = λ t u Tm3 var3 lam3 app3 tt3 pair3 fst snd left right case zero suc rec →
     pair3 (t Tm3 var3 lam3 app3 tt3 pair3 fst snd left right case zero suc rec)
          (u Tm3 var3 lam3 app3 tt3 pair3 fst snd left right case zero suc rec)

fst3 : ∀{Γ A B} → Tm3 Γ (prod3 A B) → Tm3 Γ A; fst3
 = λ t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd left right case zero suc rec →
     fst3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd left right case zero suc rec)

snd3 : ∀{Γ A B} → Tm3 Γ (prod3 A B) → Tm3 Γ B; snd3
 = λ t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left right case zero suc rec →
     snd3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left right case zero suc rec)

left3 : ∀{Γ A B} → Tm3 Γ A → Tm3 Γ (sum3 A B); left3
 = λ t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right case zero suc rec →
     left3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right case zero suc rec)

right3 : ∀{Γ A B} → Tm3 Γ B → Tm3 Γ (sum3 A B); right3
 = λ t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case zero suc rec →
     right3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case zero suc rec)

case3 : ∀{Γ A B C} → Tm3 Γ (sum3 A B) → Tm3 Γ (arr3 A C) → Tm3 Γ (arr3 B C) → Tm3 Γ C; case3
 = λ t u v Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero suc rec →
     case3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero suc rec)
           (u Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero suc rec)
           (v Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero suc rec)

zero3  : ∀{Γ} → Tm3 Γ nat3; zero3
 = λ Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc rec → zero3

suc3 : ∀{Γ} → Tm3 Γ nat3 → Tm3 Γ nat3; suc3
 = λ t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec →
   suc3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec)

rec3 : ∀{Γ A} → Tm3 Γ nat3 → Tm3 Γ (arr3 nat3 (arr3 A A)) → Tm3 Γ A → Tm3 Γ A; rec3
 = λ t u v Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec3 →
     rec3 (t Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec3)
         (u Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec3)
         (v Tm3 var3 lam3 app3 tt3 pair3 fst3 snd3 left3 right3 case3 zero3 suc3 rec3)

v03 : ∀{Γ A} → Tm3 (snoc3 Γ A) A; v03
 = var3 vz3

v13 : ∀{Γ A B} → Tm3 (snoc3 (snoc3 Γ A) B) A; v13
 = var3 (vs3 vz3)

v23 : ∀{Γ A B C} → Tm3 (snoc3 (snoc3 (snoc3 Γ A) B) C) A; v23
 = var3 (vs3 (vs3 vz3))

v33 : ∀{Γ A B C D} → Tm3 (snoc3 (snoc3 (snoc3 (snoc3 Γ A) B) C) D) A; v33
 = var3 (vs3 (vs3 (vs3 vz3)))

tbool3 : Ty3; tbool3
 = sum3 top3 top3

true3 : ∀{Γ} → Tm3 Γ tbool3; true3
 = left3 tt3

tfalse3 : ∀{Γ} → Tm3 Γ tbool3; tfalse3
 = right3 tt3

ifthenelse3 : ∀{Γ A} → Tm3 Γ (arr3 tbool3 (arr3 A (arr3 A A))); ifthenelse3
 = lam3 (lam3 (lam3 (case3 v23 (lam3 v23) (lam3 v13))))

times43 : ∀{Γ A} → Tm3 Γ (arr3 (arr3 A A) (arr3 A A)); times43
  = lam3 (lam3 (app3 v13 (app3 v13 (app3 v13 (app3 v13 v03)))))

add3 : ∀{Γ} → Tm3 Γ (arr3 nat3 (arr3 nat3 nat3)); add3
 = lam3 (rec3 v03
       (lam3 (lam3 (lam3 (suc3 (app3 v13 v03)))))
       (lam3 v03))

mul3 : ∀{Γ} → Tm3 Γ (arr3 nat3 (arr3 nat3 nat3)); mul3
 = lam3 (rec3 v03
       (lam3 (lam3 (lam3 (app3 (app3 add3 (app3 v13 v03)) v03))))
       (lam3 zero3))

fact3 : ∀{Γ} → Tm3 Γ (arr3 nat3 nat3); fact3
 = lam3 (rec3 v03 (lam3 (lam3 (app3 (app3 mul3 (suc3 v13)) v03)))
        (suc3 zero3))
{-# OPTIONS --type-in-type #-}

Ty4 : Set
Ty4 =
   (Ty4         : Set)
   (nat top bot  : Ty4)
   (arr prod sum : Ty4 → Ty4 → Ty4)
 → Ty4

nat4 : Ty4; nat4 = λ _ nat4 _ _ _ _ _ → nat4
top4 : Ty4; top4 = λ _ _ top4 _ _ _ _ → top4
bot4 : Ty4; bot4 = λ _ _ _ bot4 _ _ _ → bot4

arr4 : Ty4 → Ty4 → Ty4; arr4
 = λ A B Ty4 nat4 top4 bot4 arr4 prod sum →
     arr4 (A Ty4 nat4 top4 bot4 arr4 prod sum) (B Ty4 nat4 top4 bot4 arr4 prod sum)

prod4 : Ty4 → Ty4 → Ty4; prod4
 = λ A B Ty4 nat4 top4 bot4 arr4 prod4 sum →
     prod4 (A Ty4 nat4 top4 bot4 arr4 prod4 sum) (B Ty4 nat4 top4 bot4 arr4 prod4 sum)

sum4 : Ty4 → Ty4 → Ty4; sum4
 = λ A B Ty4 nat4 top4 bot4 arr4 prod4 sum4 →
     sum4 (A Ty4 nat4 top4 bot4 arr4 prod4 sum4) (B Ty4 nat4 top4 bot4 arr4 prod4 sum4)

Con4 : Set; Con4
 = (Con4 : Set)
   (nil  : Con4)
   (snoc : Con4 → Ty4 → Con4)
 → Con4

nil4 : Con4; nil4
 = λ Con4 nil4 snoc → nil4

snoc4 : Con4 → Ty4 → Con4; snoc4
 = λ Γ A Con4 nil4 snoc4 → snoc4 (Γ Con4 nil4 snoc4) A

Var4 : Con4 → Ty4 → Set; Var4
 = λ Γ A →
   (Var4 : Con4 → Ty4 → Set)
   (vz  : ∀{Γ A} → Var4 (snoc4 Γ A) A)
   (vs  : ∀{Γ B A} → Var4 Γ A → Var4 (snoc4 Γ B) A)
 → Var4 Γ A

vz4 : ∀{Γ A} → Var4 (snoc4 Γ A) A; vz4
 = λ Var4 vz4 vs → vz4

vs4 : ∀{Γ B A} → Var4 Γ A → Var4 (snoc4 Γ B) A; vs4
 = λ x Var4 vz4 vs4 → vs4 (x Var4 vz4 vs4)

Tm4 : Con4 → Ty4 → Set; Tm4
 = λ Γ A →
   (Tm4  : Con4 → Ty4 → Set)
   (var   : ∀{Γ A} → Var4 Γ A → Tm4 Γ A)
   (lam   : ∀{Γ A B} → Tm4 (snoc4 Γ A) B → Tm4 Γ (arr4 A B))
   (app   : ∀{Γ A B} → Tm4 Γ (arr4 A B) → Tm4 Γ A → Tm4 Γ B)
   (tt    : ∀{Γ} → Tm4 Γ top4)
   (pair  : ∀{Γ A B} → Tm4 Γ A → Tm4 Γ B → Tm4 Γ (prod4 A B))
   (fst   : ∀{Γ A B} → Tm4 Γ (prod4 A B) → Tm4 Γ A)
   (snd   : ∀{Γ A B} → Tm4 Γ (prod4 A B) → Tm4 Γ B)
   (left  : ∀{Γ A B} → Tm4 Γ A → Tm4 Γ (sum4 A B))
   (right : ∀{Γ A B} → Tm4 Γ B → Tm4 Γ (sum4 A B))
   (case  : ∀{Γ A B C} → Tm4 Γ (sum4 A B) → Tm4 Γ (arr4 A C) → Tm4 Γ (arr4 B C) → Tm4 Γ C)
   (zero  : ∀{Γ} → Tm4 Γ nat4)
   (suc   : ∀{Γ} → Tm4 Γ nat4 → Tm4 Γ nat4)
   (rec   : ∀{Γ A} → Tm4 Γ nat4 → Tm4 Γ (arr4 nat4 (arr4 A A)) → Tm4 Γ A → Tm4 Γ A)
 → Tm4 Γ A

var4 : ∀{Γ A} → Var4 Γ A → Tm4 Γ A; var4
 = λ x Tm4 var4 lam app tt pair fst snd left right case zero suc rec →
     var4 x

lam4 : ∀{Γ A B} → Tm4 (snoc4 Γ A) B → Tm4 Γ (arr4 A B); lam4
 = λ t Tm4 var4 lam4 app tt pair fst snd left right case zero suc rec →
     lam4 (t Tm4 var4 lam4 app tt pair fst snd left right case zero suc rec)

app4 : ∀{Γ A B} → Tm4 Γ (arr4 A B) → Tm4 Γ A → Tm4 Γ B; app4
 = λ t u Tm4 var4 lam4 app4 tt pair fst snd left right case zero suc rec →
     app4 (t Tm4 var4 lam4 app4 tt pair fst snd left right case zero suc rec)
         (u Tm4 var4 lam4 app4 tt pair fst snd left right case zero suc rec)

tt4 : ∀{Γ} → Tm4 Γ top4; tt4
 = λ Tm4 var4 lam4 app4 tt4 pair fst snd left right case zero suc rec → tt4

pair4 : ∀{Γ A B} → Tm4 Γ A → Tm4 Γ B → Tm4 Γ (prod4 A B); pair4
 = λ t u Tm4 var4 lam4 app4 tt4 pair4 fst snd left right case zero suc rec →
     pair4 (t Tm4 var4 lam4 app4 tt4 pair4 fst snd left right case zero suc rec)
          (u Tm4 var4 lam4 app4 tt4 pair4 fst snd left right case zero suc rec)

fst4 : ∀{Γ A B} → Tm4 Γ (prod4 A B) → Tm4 Γ A; fst4
 = λ t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd left right case zero suc rec →
     fst4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd left right case zero suc rec)

snd4 : ∀{Γ A B} → Tm4 Γ (prod4 A B) → Tm4 Γ B; snd4
 = λ t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left right case zero suc rec →
     snd4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left right case zero suc rec)

left4 : ∀{Γ A B} → Tm4 Γ A → Tm4 Γ (sum4 A B); left4
 = λ t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right case zero suc rec →
     left4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right case zero suc rec)

right4 : ∀{Γ A B} → Tm4 Γ B → Tm4 Γ (sum4 A B); right4
 = λ t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case zero suc rec →
     right4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case zero suc rec)

case4 : ∀{Γ A B C} → Tm4 Γ (sum4 A B) → Tm4 Γ (arr4 A C) → Tm4 Γ (arr4 B C) → Tm4 Γ C; case4
 = λ t u v Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero suc rec →
     case4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero suc rec)
           (u Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero suc rec)
           (v Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero suc rec)

zero4  : ∀{Γ} → Tm4 Γ nat4; zero4
 = λ Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc rec → zero4

suc4 : ∀{Γ} → Tm4 Γ nat4 → Tm4 Γ nat4; suc4
 = λ t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec →
   suc4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec)

rec4 : ∀{Γ A} → Tm4 Γ nat4 → Tm4 Γ (arr4 nat4 (arr4 A A)) → Tm4 Γ A → Tm4 Γ A; rec4
 = λ t u v Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec4 →
     rec4 (t Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec4)
         (u Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec4)
         (v Tm4 var4 lam4 app4 tt4 pair4 fst4 snd4 left4 right4 case4 zero4 suc4 rec4)

v04 : ∀{Γ A} → Tm4 (snoc4 Γ A) A; v04
 = var4 vz4

v14 : ∀{Γ A B} → Tm4 (snoc4 (snoc4 Γ A) B) A; v14
 = var4 (vs4 vz4)

v24 : ∀{Γ A B C} → Tm4 (snoc4 (snoc4 (snoc4 Γ A) B) C) A; v24
 = var4 (vs4 (vs4 vz4))

v34 : ∀{Γ A B C D} → Tm4 (snoc4 (snoc4 (snoc4 (snoc4 Γ A) B) C) D) A; v34
 = var4 (vs4 (vs4 (vs4 vz4)))

tbool4 : Ty4; tbool4
 = sum4 top4 top4

true4 : ∀{Γ} → Tm4 Γ tbool4; true4
 = left4 tt4

tfalse4 : ∀{Γ} → Tm4 Γ tbool4; tfalse4
 = right4 tt4

ifthenelse4 : ∀{Γ A} → Tm4 Γ (arr4 tbool4 (arr4 A (arr4 A A))); ifthenelse4
 = lam4 (lam4 (lam4 (case4 v24 (lam4 v24) (lam4 v14))))

times44 : ∀{Γ A} → Tm4 Γ (arr4 (arr4 A A) (arr4 A A)); times44
  = lam4 (lam4 (app4 v14 (app4 v14 (app4 v14 (app4 v14 v04)))))

add4 : ∀{Γ} → Tm4 Γ (arr4 nat4 (arr4 nat4 nat4)); add4
 = lam4 (rec4 v04
       (lam4 (lam4 (lam4 (suc4 (app4 v14 v04)))))
       (lam4 v04))

mul4 : ∀{Γ} → Tm4 Γ (arr4 nat4 (arr4 nat4 nat4)); mul4
 = lam4 (rec4 v04
       (lam4 (lam4 (lam4 (app4 (app4 add4 (app4 v14 v04)) v04))))
       (lam4 zero4))

fact4 : ∀{Γ} → Tm4 Γ (arr4 nat4 nat4); fact4
 = lam4 (rec4 v04 (lam4 (lam4 (app4 (app4 mul4 (suc4 v14)) v04)))
        (suc4 zero4))
{-# OPTIONS --type-in-type #-}

Ty5 : Set
Ty5 =
   (Ty5         : Set)
   (nat top bot  : Ty5)
   (arr prod sum : Ty5 → Ty5 → Ty5)
 → Ty5

nat5 : Ty5; nat5 = λ _ nat5 _ _ _ _ _ → nat5
top5 : Ty5; top5 = λ _ _ top5 _ _ _ _ → top5
bot5 : Ty5; bot5 = λ _ _ _ bot5 _ _ _ → bot5

arr5 : Ty5 → Ty5 → Ty5; arr5
 = λ A B Ty5 nat5 top5 bot5 arr5 prod sum →
     arr5 (A Ty5 nat5 top5 bot5 arr5 prod sum) (B Ty5 nat5 top5 bot5 arr5 prod sum)

prod5 : Ty5 → Ty5 → Ty5; prod5
 = λ A B Ty5 nat5 top5 bot5 arr5 prod5 sum →
     prod5 (A Ty5 nat5 top5 bot5 arr5 prod5 sum) (B Ty5 nat5 top5 bot5 arr5 prod5 sum)

sum5 : Ty5 → Ty5 → Ty5; sum5
 = λ A B Ty5 nat5 top5 bot5 arr5 prod5 sum5 →
     sum5 (A Ty5 nat5 top5 bot5 arr5 prod5 sum5) (B Ty5 nat5 top5 bot5 arr5 prod5 sum5)

Con5 : Set; Con5
 = (Con5 : Set)
   (nil  : Con5)
   (snoc : Con5 → Ty5 → Con5)
 → Con5

nil5 : Con5; nil5
 = λ Con5 nil5 snoc → nil5

snoc5 : Con5 → Ty5 → Con5; snoc5
 = λ Γ A Con5 nil5 snoc5 → snoc5 (Γ Con5 nil5 snoc5) A

Var5 : Con5 → Ty5 → Set; Var5
 = λ Γ A →
   (Var5 : Con5 → Ty5 → Set)
   (vz  : ∀{Γ A} → Var5 (snoc5 Γ A) A)
   (vs  : ∀{Γ B A} → Var5 Γ A → Var5 (snoc5 Γ B) A)
 → Var5 Γ A

vz5 : ∀{Γ A} → Var5 (snoc5 Γ A) A; vz5
 = λ Var5 vz5 vs → vz5

vs5 : ∀{Γ B A} → Var5 Γ A → Var5 (snoc5 Γ B) A; vs5
 = λ x Var5 vz5 vs5 → vs5 (x Var5 vz5 vs5)

Tm5 : Con5 → Ty5 → Set; Tm5
 = λ Γ A →
   (Tm5  : Con5 → Ty5 → Set)
   (var   : ∀{Γ A} → Var5 Γ A → Tm5 Γ A)
   (lam   : ∀{Γ A B} → Tm5 (snoc5 Γ A) B → Tm5 Γ (arr5 A B))
   (app   : ∀{Γ A B} → Tm5 Γ (arr5 A B) → Tm5 Γ A → Tm5 Γ B)
   (tt    : ∀{Γ} → Tm5 Γ top5)
   (pair  : ∀{Γ A B} → Tm5 Γ A → Tm5 Γ B → Tm5 Γ (prod5 A B))
   (fst   : ∀{Γ A B} → Tm5 Γ (prod5 A B) → Tm5 Γ A)
   (snd   : ∀{Γ A B} → Tm5 Γ (prod5 A B) → Tm5 Γ B)
   (left  : ∀{Γ A B} → Tm5 Γ A → Tm5 Γ (sum5 A B))
   (right : ∀{Γ A B} → Tm5 Γ B → Tm5 Γ (sum5 A B))
   (case  : ∀{Γ A B C} → Tm5 Γ (sum5 A B) → Tm5 Γ (arr5 A C) → Tm5 Γ (arr5 B C) → Tm5 Γ C)
   (zero  : ∀{Γ} → Tm5 Γ nat5)
   (suc   : ∀{Γ} → Tm5 Γ nat5 → Tm5 Γ nat5)
   (rec   : ∀{Γ A} → Tm5 Γ nat5 → Tm5 Γ (arr5 nat5 (arr5 A A)) → Tm5 Γ A → Tm5 Γ A)
 → Tm5 Γ A

var5 : ∀{Γ A} → Var5 Γ A → Tm5 Γ A; var5
 = λ x Tm5 var5 lam app tt pair fst snd left right case zero suc rec →
     var5 x

lam5 : ∀{Γ A B} → Tm5 (snoc5 Γ A) B → Tm5 Γ (arr5 A B); lam5
 = λ t Tm5 var5 lam5 app tt pair fst snd left right case zero suc rec →
     lam5 (t Tm5 var5 lam5 app tt pair fst snd left right case zero suc rec)

app5 : ∀{Γ A B} → Tm5 Γ (arr5 A B) → Tm5 Γ A → Tm5 Γ B; app5
 = λ t u Tm5 var5 lam5 app5 tt pair fst snd left right case zero suc rec →
     app5 (t Tm5 var5 lam5 app5 tt pair fst snd left right case zero suc rec)
         (u Tm5 var5 lam5 app5 tt pair fst snd left right case zero suc rec)

tt5 : ∀{Γ} → Tm5 Γ top5; tt5
 = λ Tm5 var5 lam5 app5 tt5 pair fst snd left right case zero suc rec → tt5

pair5 : ∀{Γ A B} → Tm5 Γ A → Tm5 Γ B → Tm5 Γ (prod5 A B); pair5
 = λ t u Tm5 var5 lam5 app5 tt5 pair5 fst snd left right case zero suc rec →
     pair5 (t Tm5 var5 lam5 app5 tt5 pair5 fst snd left right case zero suc rec)
          (u Tm5 var5 lam5 app5 tt5 pair5 fst snd left right case zero suc rec)

fst5 : ∀{Γ A B} → Tm5 Γ (prod5 A B) → Tm5 Γ A; fst5
 = λ t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd left right case zero suc rec →
     fst5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd left right case zero suc rec)

snd5 : ∀{Γ A B} → Tm5 Γ (prod5 A B) → Tm5 Γ B; snd5
 = λ t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left right case zero suc rec →
     snd5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left right case zero suc rec)

left5 : ∀{Γ A B} → Tm5 Γ A → Tm5 Γ (sum5 A B); left5
 = λ t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right case zero suc rec →
     left5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right case zero suc rec)

right5 : ∀{Γ A B} → Tm5 Γ B → Tm5 Γ (sum5 A B); right5
 = λ t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case zero suc rec →
     right5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case zero suc rec)

case5 : ∀{Γ A B C} → Tm5 Γ (sum5 A B) → Tm5 Γ (arr5 A C) → Tm5 Γ (arr5 B C) → Tm5 Γ C; case5
 = λ t u v Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero suc rec →
     case5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero suc rec)
           (u Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero suc rec)
           (v Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero suc rec)

zero5  : ∀{Γ} → Tm5 Γ nat5; zero5
 = λ Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc rec → zero5

suc5 : ∀{Γ} → Tm5 Γ nat5 → Tm5 Γ nat5; suc5
 = λ t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec →
   suc5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec)

rec5 : ∀{Γ A} → Tm5 Γ nat5 → Tm5 Γ (arr5 nat5 (arr5 A A)) → Tm5 Γ A → Tm5 Γ A; rec5
 = λ t u v Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec5 →
     rec5 (t Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec5)
         (u Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec5)
         (v Tm5 var5 lam5 app5 tt5 pair5 fst5 snd5 left5 right5 case5 zero5 suc5 rec5)

v05 : ∀{Γ A} → Tm5 (snoc5 Γ A) A; v05
 = var5 vz5

v15 : ∀{Γ A B} → Tm5 (snoc5 (snoc5 Γ A) B) A; v15
 = var5 (vs5 vz5)

v25 : ∀{Γ A B C} → Tm5 (snoc5 (snoc5 (snoc5 Γ A) B) C) A; v25
 = var5 (vs5 (vs5 vz5))

v35 : ∀{Γ A B C D} → Tm5 (snoc5 (snoc5 (snoc5 (snoc5 Γ A) B) C) D) A; v35
 = var5 (vs5 (vs5 (vs5 vz5)))

tbool5 : Ty5; tbool5
 = sum5 top5 top5

true5 : ∀{Γ} → Tm5 Γ tbool5; true5
 = left5 tt5

tfalse5 : ∀{Γ} → Tm5 Γ tbool5; tfalse5
 = right5 tt5

ifthenelse5 : ∀{Γ A} → Tm5 Γ (arr5 tbool5 (arr5 A (arr5 A A))); ifthenelse5
 = lam5 (lam5 (lam5 (case5 v25 (lam5 v25) (lam5 v15))))

times45 : ∀{Γ A} → Tm5 Γ (arr5 (arr5 A A) (arr5 A A)); times45
  = lam5 (lam5 (app5 v15 (app5 v15 (app5 v15 (app5 v15 v05)))))

add5 : ∀{Γ} → Tm5 Γ (arr5 nat5 (arr5 nat5 nat5)); add5
 = lam5 (rec5 v05
       (lam5 (lam5 (lam5 (suc5 (app5 v15 v05)))))
       (lam5 v05))

mul5 : ∀{Γ} → Tm5 Γ (arr5 nat5 (arr5 nat5 nat5)); mul5
 = lam5 (rec5 v05
       (lam5 (lam5 (lam5 (app5 (app5 add5 (app5 v15 v05)) v05))))
       (lam5 zero5))

fact5 : ∀{Γ} → Tm5 Γ (arr5 nat5 nat5); fact5
 = lam5 (rec5 v05 (lam5 (lam5 (app5 (app5 mul5 (suc5 v15)) v05)))
        (suc5 zero5))
{-# OPTIONS --type-in-type #-}

Ty6 : Set
Ty6 =
   (Ty6         : Set)
   (nat top bot  : Ty6)
   (arr prod sum : Ty6 → Ty6 → Ty6)
 → Ty6

nat6 : Ty6; nat6 = λ _ nat6 _ _ _ _ _ → nat6
top6 : Ty6; top6 = λ _ _ top6 _ _ _ _ → top6
bot6 : Ty6; bot6 = λ _ _ _ bot6 _ _ _ → bot6

arr6 : Ty6 → Ty6 → Ty6; arr6
 = λ A B Ty6 nat6 top6 bot6 arr6 prod sum →
     arr6 (A Ty6 nat6 top6 bot6 arr6 prod sum) (B Ty6 nat6 top6 bot6 arr6 prod sum)

prod6 : Ty6 → Ty6 → Ty6; prod6
 = λ A B Ty6 nat6 top6 bot6 arr6 prod6 sum →
     prod6 (A Ty6 nat6 top6 bot6 arr6 prod6 sum) (B Ty6 nat6 top6 bot6 arr6 prod6 sum)

sum6 : Ty6 → Ty6 → Ty6; sum6
 = λ A B Ty6 nat6 top6 bot6 arr6 prod6 sum6 →
     sum6 (A Ty6 nat6 top6 bot6 arr6 prod6 sum6) (B Ty6 nat6 top6 bot6 arr6 prod6 sum6)

Con6 : Set; Con6
 = (Con6 : Set)
   (nil  : Con6)
   (snoc : Con6 → Ty6 → Con6)
 → Con6

nil6 : Con6; nil6
 = λ Con6 nil6 snoc → nil6

snoc6 : Con6 → Ty6 → Con6; snoc6
 = λ Γ A Con6 nil6 snoc6 → snoc6 (Γ Con6 nil6 snoc6) A

Var6 : Con6 → Ty6 → Set; Var6
 = λ Γ A →
   (Var6 : Con6 → Ty6 → Set)
   (vz  : ∀{Γ A} → Var6 (snoc6 Γ A) A)
   (vs  : ∀{Γ B A} → Var6 Γ A → Var6 (snoc6 Γ B) A)
 → Var6 Γ A

vz6 : ∀{Γ A} → Var6 (snoc6 Γ A) A; vz6
 = λ Var6 vz6 vs → vz6

vs6 : ∀{Γ B A} → Var6 Γ A → Var6 (snoc6 Γ B) A; vs6
 = λ x Var6 vz6 vs6 → vs6 (x Var6 vz6 vs6)

Tm6 : Con6 → Ty6 → Set; Tm6
 = λ Γ A →
   (Tm6  : Con6 → Ty6 → Set)
   (var   : ∀{Γ A} → Var6 Γ A → Tm6 Γ A)
   (lam   : ∀{Γ A B} → Tm6 (snoc6 Γ A) B → Tm6 Γ (arr6 A B))
   (app   : ∀{Γ A B} → Tm6 Γ (arr6 A B) → Tm6 Γ A → Tm6 Γ B)
   (tt    : ∀{Γ} → Tm6 Γ top6)
   (pair  : ∀{Γ A B} → Tm6 Γ A → Tm6 Γ B → Tm6 Γ (prod6 A B))
   (fst   : ∀{Γ A B} → Tm6 Γ (prod6 A B) → Tm6 Γ A)
   (snd   : ∀{Γ A B} → Tm6 Γ (prod6 A B) → Tm6 Γ B)
   (left  : ∀{Γ A B} → Tm6 Γ A → Tm6 Γ (sum6 A B))
   (right : ∀{Γ A B} → Tm6 Γ B → Tm6 Γ (sum6 A B))
   (case  : ∀{Γ A B C} → Tm6 Γ (sum6 A B) → Tm6 Γ (arr6 A C) → Tm6 Γ (arr6 B C) → Tm6 Γ C)
   (zero  : ∀{Γ} → Tm6 Γ nat6)
   (suc   : ∀{Γ} → Tm6 Γ nat6 → Tm6 Γ nat6)
   (rec   : ∀{Γ A} → Tm6 Γ nat6 → Tm6 Γ (arr6 nat6 (arr6 A A)) → Tm6 Γ A → Tm6 Γ A)
 → Tm6 Γ A

var6 : ∀{Γ A} → Var6 Γ A → Tm6 Γ A; var6
 = λ x Tm6 var6 lam app tt pair fst snd left right case zero suc rec →
     var6 x

lam6 : ∀{Γ A B} → Tm6 (snoc6 Γ A) B → Tm6 Γ (arr6 A B); lam6
 = λ t Tm6 var6 lam6 app tt pair fst snd left right case zero suc rec →
     lam6 (t Tm6 var6 lam6 app tt pair fst snd left right case zero suc rec)

app6 : ∀{Γ A B} → Tm6 Γ (arr6 A B) → Tm6 Γ A → Tm6 Γ B; app6
 = λ t u Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec →
     app6 (t Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec)
         (u Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec)

tt6 : ∀{Γ} → Tm6 Γ top6; tt6
 = λ Tm6 var6 lam6 app6 tt6 pair fst snd left right case zero suc rec → tt6

pair6 : ∀{Γ A B} → Tm6 Γ A → Tm6 Γ B → Tm6 Γ (prod6 A B); pair6
 = λ t u Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec →
     pair6 (t Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec)
          (u Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec)

fst6 : ∀{Γ A B} → Tm6 Γ (prod6 A B) → Tm6 Γ A; fst6
 = λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd left right case zero suc rec →
     fst6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd left right case zero suc rec)

snd6 : ∀{Γ A B} → Tm6 Γ (prod6 A B) → Tm6 Γ B; snd6
 = λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left right case zero suc rec →
     snd6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left right case zero suc rec)

left6 : ∀{Γ A B} → Tm6 Γ A → Tm6 Γ (sum6 A B); left6
 = λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right case zero suc rec →
     left6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right case zero suc rec)

right6 : ∀{Γ A B} → Tm6 Γ B → Tm6 Γ (sum6 A B); right6
 = λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case zero suc rec →
     right6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case zero suc rec)

case6 : ∀{Γ A B C} → Tm6 Γ (sum6 A B) → Tm6 Γ (arr6 A C) → Tm6 Γ (arr6 B C) → Tm6 Γ C; case6
 = λ t u v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec →
     case6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)
           (u Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)
           (v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)

zero6  : ∀{Γ} → Tm6 Γ nat6; zero6
 = λ Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc rec → zero6

suc6 : ∀{Γ} → Tm6 Γ nat6 → Tm6 Γ nat6; suc6
 = λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec →
   suc6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec)

rec6 : ∀{Γ A} → Tm6 Γ nat6 → Tm6 Γ (arr6 nat6 (arr6 A A)) → Tm6 Γ A → Tm6 Γ A; rec6
 = λ t u v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6 →
     rec6 (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)
         (u Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)
         (v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)

v06 : ∀{Γ A} → Tm6 (snoc6 Γ A) A; v06
 = var6 vz6

v16 : ∀{Γ A B} → Tm6 (snoc6 (snoc6 Γ A) B) A; v16
 = var6 (vs6 vz6)

v26 : ∀{Γ A B C} → Tm6 (snoc6 (snoc6 (snoc6 Γ A) B) C) A; v26
 = var6 (vs6 (vs6 vz6))

v36 : ∀{Γ A B C D} → Tm6 (snoc6 (snoc6 (snoc6 (snoc6 Γ A) B) C) D) A; v36
 = var6 (vs6 (vs6 (vs6 vz6)))

tbool6 : Ty6; tbool6
 = sum6 top6 top6

true6 : ∀{Γ} → Tm6 Γ tbool6; true6
 = left6 tt6

tfalse6 : ∀{Γ} → Tm6 Γ tbool6; tfalse6
 = right6 tt6

ifthenelse6 : ∀{Γ A} → Tm6 Γ (arr6 tbool6 (arr6 A (arr6 A A))); ifthenelse6
 = lam6 (lam6 (lam6 (case6 v26 (lam6 v26) (lam6 v16))))

times46 : ∀{Γ A} → Tm6 Γ (arr6 (arr6 A A) (arr6 A A)); times46
  = lam6 (lam6 (app6 v16 (app6 v16 (app6 v16 (app6 v16 v06)))))

add6 : ∀{Γ} → Tm6 Γ (arr6 nat6 (arr6 nat6 nat6)); add6
 = lam6 (rec6 v06
       (lam6 (lam6 (lam6 (suc6 (app6 v16 v06)))))
       (lam6 v06))

mul6 : ∀{Γ} → Tm6 Γ (arr6 nat6 (arr6 nat6 nat6)); mul6
 = lam6 (rec6 v06
       (lam6 (lam6 (lam6 (app6 (app6 add6 (app6 v16 v06)) v06))))
       (lam6 zero6))

fact6 : ∀{Γ} → Tm6 Γ (arr6 nat6 nat6); fact6
 = lam6 (rec6 v06 (lam6 (lam6 (app6 (app6 mul6 (suc6 v16)) v06)))
        (suc6 zero6))
{-# OPTIONS --type-in-type #-}

Ty7 : Set
Ty7 =
   (Ty7         : Set)
   (nat top bot  : Ty7)
   (arr prod sum : Ty7 → Ty7 → Ty7)
 → Ty7

nat7 : Ty7; nat7 = λ _ nat7 _ _ _ _ _ → nat7
top7 : Ty7; top7 = λ _ _ top7 _ _ _ _ → top7
bot7 : Ty7; bot7 = λ _ _ _ bot7 _ _ _ → bot7

arr7 : Ty7 → Ty7 → Ty7; arr7
 = λ A B Ty7 nat7 top7 bot7 arr7 prod sum →
     arr7 (A Ty7 nat7 top7 bot7 arr7 prod sum) (B Ty7 nat7 top7 bot7 arr7 prod sum)

prod7 : Ty7 → Ty7 → Ty7; prod7
 = λ A B Ty7 nat7 top7 bot7 arr7 prod7 sum →
     prod7 (A Ty7 nat7 top7 bot7 arr7 prod7 sum) (B Ty7 nat7 top7 bot7 arr7 prod7 sum)

sum7 : Ty7 → Ty7 → Ty7; sum7
 = λ A B Ty7 nat7 top7 bot7 arr7 prod7 sum7 →
     sum7 (A Ty7 nat7 top7 bot7 arr7 prod7 sum7) (B Ty7 nat7 top7 bot7 arr7 prod7 sum7)

Con7 : Set; Con7
 = (Con7 : Set)
   (nil  : Con7)
   (snoc : Con7 → Ty7 → Con7)
 → Con7

nil7 : Con7; nil7
 = λ Con7 nil7 snoc → nil7

snoc7 : Con7 → Ty7 → Con7; snoc7
 = λ Γ A Con7 nil7 snoc7 → snoc7 (Γ Con7 nil7 snoc7) A

Var7 : Con7 → Ty7 → Set; Var7
 = λ Γ A →
   (Var7 : Con7 → Ty7 → Set)
   (vz  : ∀{Γ A} → Var7 (snoc7 Γ A) A)
   (vs  : ∀{Γ B A} → Var7 Γ A → Var7 (snoc7 Γ B) A)
 → Var7 Γ A

vz7 : ∀{Γ A} → Var7 (snoc7 Γ A) A; vz7
 = λ Var7 vz7 vs → vz7

vs7 : ∀{Γ B A} → Var7 Γ A → Var7 (snoc7 Γ B) A; vs7
 = λ x Var7 vz7 vs7 → vs7 (x Var7 vz7 vs7)

Tm7 : Con7 → Ty7 → Set; Tm7
 = λ Γ A →
   (Tm7  : Con7 → Ty7 → Set)
   (var   : ∀{Γ A} → Var7 Γ A → Tm7 Γ A)
   (lam   : ∀{Γ A B} → Tm7 (snoc7 Γ A) B → Tm7 Γ (arr7 A B))
   (app   : ∀{Γ A B} → Tm7 Γ (arr7 A B) → Tm7 Γ A → Tm7 Γ B)
   (tt    : ∀{Γ} → Tm7 Γ top7)
   (pair  : ∀{Γ A B} → Tm7 Γ A → Tm7 Γ B → Tm7 Γ (prod7 A B))
   (fst   : ∀{Γ A B} → Tm7 Γ (prod7 A B) → Tm7 Γ A)
   (snd   : ∀{Γ A B} → Tm7 Γ (prod7 A B) → Tm7 Γ B)
   (left  : ∀{Γ A B} → Tm7 Γ A → Tm7 Γ (sum7 A B))
   (right : ∀{Γ A B} → Tm7 Γ B → Tm7 Γ (sum7 A B))
   (case  : ∀{Γ A B C} → Tm7 Γ (sum7 A B) → Tm7 Γ (arr7 A C) → Tm7 Γ (arr7 B C) → Tm7 Γ C)
   (zero  : ∀{Γ} → Tm7 Γ nat7)
   (suc   : ∀{Γ} → Tm7 Γ nat7 → Tm7 Γ nat7)
   (rec   : ∀{Γ A} → Tm7 Γ nat7 → Tm7 Γ (arr7 nat7 (arr7 A A)) → Tm7 Γ A → Tm7 Γ A)
 → Tm7 Γ A

var7 : ∀{Γ A} → Var7 Γ A → Tm7 Γ A; var7
 = λ x Tm7 var7 lam app tt pair fst snd left right case zero suc rec →
     var7 x

lam7 : ∀{Γ A B} → Tm7 (snoc7 Γ A) B → Tm7 Γ (arr7 A B); lam7
 = λ t Tm7 var7 lam7 app tt pair fst snd left right case zero suc rec →
     lam7 (t Tm7 var7 lam7 app tt pair fst snd left right case zero suc rec)

app7 : ∀{Γ A B} → Tm7 Γ (arr7 A B) → Tm7 Γ A → Tm7 Γ B; app7
 = λ t u Tm7 var7 lam7 app7 tt pair fst snd left right case zero suc rec →
     app7 (t Tm7 var7 lam7 app7 tt pair fst snd left right case zero suc rec)
         (u Tm7 var7 lam7 app7 tt pair fst snd left right case zero suc rec)

tt7 : ∀{Γ} → Tm7 Γ top7; tt7
 = λ Tm7 var7 lam7 app7 tt7 pair fst snd left right case zero suc rec → tt7

pair7 : ∀{Γ A B} → Tm7 Γ A → Tm7 Γ B → Tm7 Γ (prod7 A B); pair7
 = λ t u Tm7 var7 lam7 app7 tt7 pair7 fst snd left right case zero suc rec →
     pair7 (t Tm7 var7 lam7 app7 tt7 pair7 fst snd left right case zero suc rec)
          (u Tm7 var7 lam7 app7 tt7 pair7 fst snd left right case zero suc rec)

fst7 : ∀{Γ A B} → Tm7 Γ (prod7 A B) → Tm7 Γ A; fst7
 = λ t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd left right case zero suc rec →
     fst7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd left right case zero suc rec)

snd7 : ∀{Γ A B} → Tm7 Γ (prod7 A B) → Tm7 Γ B; snd7
 = λ t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left right case zero suc rec →
     snd7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left right case zero suc rec)

left7 : ∀{Γ A B} → Tm7 Γ A → Tm7 Γ (sum7 A B); left7
 = λ t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right case zero suc rec →
     left7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right case zero suc rec)

right7 : ∀{Γ A B} → Tm7 Γ B → Tm7 Γ (sum7 A B); right7
 = λ t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case zero suc rec →
     right7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case zero suc rec)

case7 : ∀{Γ A B C} → Tm7 Γ (sum7 A B) → Tm7 Γ (arr7 A C) → Tm7 Γ (arr7 B C) → Tm7 Γ C; case7
 = λ t u v Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero suc rec →
     case7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero suc rec)
           (u Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero suc rec)
           (v Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero suc rec)

zero7  : ∀{Γ} → Tm7 Γ nat7; zero7
 = λ Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc rec → zero7

suc7 : ∀{Γ} → Tm7 Γ nat7 → Tm7 Γ nat7; suc7
 = λ t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec →
   suc7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec)

rec7 : ∀{Γ A} → Tm7 Γ nat7 → Tm7 Γ (arr7 nat7 (arr7 A A)) → Tm7 Γ A → Tm7 Γ A; rec7
 = λ t u v Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec7 →
     rec7 (t Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec7)
         (u Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec7)
         (v Tm7 var7 lam7 app7 tt7 pair7 fst7 snd7 left7 right7 case7 zero7 suc7 rec7)

v07 : ∀{Γ A} → Tm7 (snoc7 Γ A) A; v07
 = var7 vz7

v17 : ∀{Γ A B} → Tm7 (snoc7 (snoc7 Γ A) B) A; v17
 = var7 (vs7 vz7)

v27 : ∀{Γ A B C} → Tm7 (snoc7 (snoc7 (snoc7 Γ A) B) C) A; v27
 = var7 (vs7 (vs7 vz7))

v37 : ∀{Γ A B C D} → Tm7 (snoc7 (snoc7 (snoc7 (snoc7 Γ A) B) C) D) A; v37
 = var7 (vs7 (vs7 (vs7 vz7)))

tbool7 : Ty7; tbool7
 = sum7 top7 top7

true7 : ∀{Γ} → Tm7 Γ tbool7; true7
 = left7 tt7

tfalse7 : ∀{Γ} → Tm7 Γ tbool7; tfalse7
 = right7 tt7

ifthenelse7 : ∀{Γ A} → Tm7 Γ (arr7 tbool7 (arr7 A (arr7 A A))); ifthenelse7
 = lam7 (lam7 (lam7 (case7 v27 (lam7 v27) (lam7 v17))))

times47 : ∀{Γ A} → Tm7 Γ (arr7 (arr7 A A) (arr7 A A)); times47
  = lam7 (lam7 (app7 v17 (app7 v17 (app7 v17 (app7 v17 v07)))))

add7 : ∀{Γ} → Tm7 Γ (arr7 nat7 (arr7 nat7 nat7)); add7
 = lam7 (rec7 v07
       (lam7 (lam7 (lam7 (suc7 (app7 v17 v07)))))
       (lam7 v07))

mul7 : ∀{Γ} → Tm7 Γ (arr7 nat7 (arr7 nat7 nat7)); mul7
 = lam7 (rec7 v07
       (lam7 (lam7 (lam7 (app7 (app7 add7 (app7 v17 v07)) v07))))
       (lam7 zero7))

fact7 : ∀{Γ} → Tm7 Γ (arr7 nat7 nat7); fact7
 = lam7 (rec7 v07 (lam7 (lam7 (app7 (app7 mul7 (suc7 v17)) v07)))
        (suc7 zero7))

max_stars_repo_name: int-index/smalltt

max_issues_repo_name: int-index/smalltt

max_forks_repo_name: int-index/smalltt


text:
module IdemInvo where

open import Relation.Binary.PropositionalEquality

module MainResult
  (A : Set)
  (f : A → A)
  (idem : ∀ x → f (f x) ≡ f x)
  (invo : ∀ x → f (f x) ≡ x)
  where

  -- an idempotent and involutive function is an identity function
  iden : ∀ x → f x ≡ x
  iden x = trans (sym (idem x)) (invo x)

max_stars_repo_name: zaklogician/IdemInvo

max_issues_repo_name: zaklogician/IdemInvo

max_forks_repo_name: zaklogician/IdemInvo


text:
postulate
  I : Set

data Box (A : Set) : Set where
  [_] : A → Box A

variable
  @0 i : I
  @0 b : Box I

data D : @0 Box I → Set where
  d : D [ i ] → D [ i ]

variable
  @0 x : D b

data P : @0 D b → Set where
  p : P (d x)

works : ∀ {i} {@0 x : D [ i ]} → P (d x)
works = p

fails : ∀ {@0 i} {@0 x : D [ i ]} → P (d x)
fails = p


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.FunExtEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ : Level

-- Function extensionality is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {f g : (x : A) → B x} where
  private
    fib : (p : f ≡ g) → fiber funExt p
    fib p = (funExt⁻ p , refl)

    funExt-fiber-isContr : (p : f ≡ g) → (fi : fiber funExt p) → fib p ≡ fi
    funExt-fiber-isContr p (h , eq) i = (funExt⁻ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt-isEquiv : isEquiv funExt
  equiv-proof funExt-isEquiv p = (fib p , funExt-fiber-isContr p)

  funExtEquiv : (∀ x → f x ≡ g x) ≃ (f ≡ g)
  funExtEquiv = (funExt {B = B} , funExt-isEquiv)

  funExtPath : (∀ x → f x ≡ g x) ≡ (f ≡ g)
  funExtPath = ua funExtEquiv

-- Function extensionality for binary functions
funExt₂ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
            {f g : (x : A) → (y : B x) → C x y}
          → ((x : A) (y : B x) → f x y ≡ g x y) → f ≡ g
funExt₂ p i x y = p x y i

-- Function extensionality for binary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
         {f g : (x : A) → (y : B x) → C x y} where
  private
    appl₂ : f ≡ g → ∀ x y → f x y ≡ g x y
    appl₂ eq x y i = eq i x y

    fib : (p : f ≡ g) → fiber funExt₂ p
    fib p = (appl₂ p , refl)

    funExt₂-fiber-isContr : (p : f ≡ g) → (fi : fiber funExt₂ p) → fib p ≡ fi
    funExt₂-fiber-isContr p (h , eq) i = (appl₂ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt₂-isEquiv : isEquiv funExt₂
  equiv-proof funExt₂-isEquiv p = (fib p , funExt₂-fiber-isContr p)

  funExt₂Equiv : (∀ x y → f x y ≡ g x y) ≃ (f ≡ g)
  funExt₂Equiv = (funExt₂ , funExt₂-isEquiv)

  funExt₂Path : (∀ x y → f x y ≡ g x y) ≡ (f ≡ g)
  funExt₂Path = ua funExt₂Equiv

-- Function extensionality for ternary functions
funExt₃ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
          {D : (x : A) → (y : B x) → C x y → Type ℓ₃}
          {f g : (x : A) → (y : B x) → (z : C x y) → D x y z}
        → ((x : A) (y : B x) (z : C x y) → f x y z ≡ g x y z) → f ≡ g
funExt₃ p i x y z = p x y z i

-- Function extensionality for ternary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
         {D : (x : A) → (y : B x) → C x y → Type ℓ₃}
         {f g : (x : A) → (y : B x) → (z : C x y) → D x y z} where
  private
    appl₃ : f ≡ g → ∀ x y z → f x y z ≡ g x y z
    appl₃ eq x y z i = eq i x y z

    fib : (p : f ≡ g) → fiber funExt₃ p
    fib p = (appl₃ p , refl)

    funExt₃-fiber-isContr : (p : f ≡ g) → (fi : fiber funExt₃ p) → fib p ≡ fi
    funExt₃-fiber-isContr p (h , eq) i = (appl₃ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt₃-isEquiv : isEquiv funExt₃
  equiv-proof funExt₃-isEquiv p = (fib p , funExt₃-fiber-isContr p)

  funExt₃Equiv : (∀ x y z → f x y z ≡ g x y z) ≃ (f ≡ g)
  funExt₃Equiv = (funExt₃ , funExt₃-isEquiv)

  funExt₃Path : (∀ x y z → f x y z ≡ g x y z) ≡ (f ≡ g)
  funExt₃Path = ua funExt₃Equiv

-- Puzzle: Can one generalize this to n-ary functions?

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module Categories.Object.Coproduct {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Function using (_$_)

open Category 𝒞

open import Categories.Morphism.Reasoning 𝒞
open import Categories.Morphism 𝒞

open HomReasoning

private
  variable
    A B C D : Obj
    f g h : A ⇒ B

record Coproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  infix 10 [_,_]

  field
    A+B   : Obj
    i₁    : A ⇒ A+B
    i₂    : B ⇒ A+B
    [_,_] : A ⇒ C → B ⇒ C → A+B ⇒ C

    inject₁ : [ f , g ] ∘ i₁ ≈ f
    inject₂ : [ f , g ] ∘ i₂ ≈ g
    unique   : h ∘ i₁ ≈ f → h ∘ i₂ ≈ g → [ f , g ] ≈ h

  g-η : [ f ∘ i₁ , f ∘ i₂ ] ≈ f
  g-η = unique Equiv.refl Equiv.refl

  η : [ i₁ , i₂ ] ≈ id
  η = unique identityˡ identityˡ

  []-cong₂ : ∀ {C} → {f f′ : A ⇒ C} {g g′ : B ⇒ C} → f ≈ f′ → g ≈ g′ → [ f , g ] ≈ [ f′ , g′ ]
  []-cong₂ f≈f′ g≈g′ = unique (inject₁ ○ ⟺ f≈f′) (inject₂ ○ ⟺ g≈g′)

  ∘-distribˡ-[] : ∀ {f : A ⇒ C} {g : B ⇒ C} {q : C ⇒ D} → q ∘ [ f , g ] ≈ [ q ∘ f , q ∘ g ]
  ∘-distribˡ-[] = ⟺ $ unique (pullʳ inject₁) (pullʳ inject₂)

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: FintanH/agda-categories

max_forks_repo_name: FintanH/agda-categories


text:
{-# OPTIONS --without-K #-}

module Pitch where

open import Data.Bool       using (Bool; false; true)
open import Data.Integer    using (ℤ; +_; -[1+_])
open import Data.Fin        using (Fin; toℕ; #_; _≟_) renaming (zero to fz; suc to fs)
open import Data.Maybe      using (Maybe; just; nothing) renaming (map to mmap)
open import Data.Nat        using (ℕ; suc; _+_; _*_; _∸_; _≡ᵇ_)
open import Data.Nat.DivMod using (_mod_; _div_)
open import Data.Product    using (_×_; _,_; proj₁)
open import Data.Vec        using (Vec; []; _∷_; map; lookup; replicate; _[_]%=_; toList)
open import Function        using (_∘_)

open import Relation.Nullary using (yes; no)

open import BitVec          using (BitVec; insert)
open import Lemmas          using (revMod; -_mod_; -_div_)
open import Util            using (findIndex)

-- Position of a pitch on an absolute scale
-- 0 is C(-1) on the international scale (where C4 is middle C)
-- or C0 on the Midi scale (where C5 is middle C)
-- Pitch is intentially set to match Midi pitch.
-- However it is fine to let 0 represent some other note and
-- translate appropriately at the end.
data Pitch : Set where
  pitch : ℕ → Pitch

unpitch : Pitch → ℕ
unpitch (pitch p) = p

-- Number of notes in the chromatic scale.
chromaticScaleSize : ℕ
chromaticScaleSize = 12

-- Number of notes in the diatonic scale.
diatonicScaleSize : ℕ
diatonicScaleSize = 7

-- Position of a pitch within an octave, in the range [0..chromaticScaleSize-1].
data PitchClass : Set where
  pitchClass : Fin chromaticScaleSize → PitchClass

unPitchClass : PitchClass → Fin chromaticScaleSize
unPitchClass (pitchClass p) = p

Scale : ℕ → Set
Scale = Vec PitchClass

-- Which octave one is in.
data Octave : Set where
  octave : ℕ → Octave

unoctave : Octave → ℕ
unoctave (octave n) = n

PitchOctave : Set
PitchOctave = PitchClass × Octave

relativeToAbsolute : PitchOctave → Pitch
relativeToAbsolute (pitchClass n , octave o) =
  pitch (o * chromaticScaleSize + (toℕ n))

absoluteToRelative : Pitch → PitchOctave
absoluteToRelative (pitch  n) =
  (pitchClass (n mod chromaticScaleSize) , octave (n div chromaticScaleSize))

pitchToClass : Pitch → PitchClass
pitchToClass = proj₁ ∘ absoluteToRelative

majorScale harmonicMinorScale : Scale diatonicScaleSize
majorScale         = map pitchClass (# 0 ∷ # 2 ∷ # 4 ∷ # 5 ∷ # 7 ∷ # 9 ∷ # 11 ∷ [])
harmonicMinorScale = map pitchClass (# 0 ∷ # 2 ∷ # 3 ∷ # 5 ∷ # 7 ∷ # 8 ∷ # 11 ∷ [])

indexInScale : {n : ℕ} → Vec PitchClass n → Fin chromaticScaleSize → Maybe (Fin n)
indexInScale []         p = nothing
indexInScale (pc ∷ pcs) p with (unPitchClass pc ≟ p)
... | yes _ = just fz
... | no  _ = mmap fs (indexInScale pcs p)

data DiatonicDegree : Set where
  diatonicDegree : Fin diatonicScaleSize → DiatonicDegree

undd : DiatonicDegree → Fin diatonicScaleSize
undd (diatonicDegree d) = d

infix 4 _≡ᵈ_
_≡ᵈ_ : DiatonicDegree → DiatonicDegree → Bool
diatonicDegree d ≡ᵈ diatonicDegree e = toℕ d ≡ᵇ toℕ e

-- round down
pitchClassToDegreeMajor : PitchClass → DiatonicDegree
pitchClassToDegreeMajor (pitchClass fz)                                                        = diatonicDegree (# 0)
pitchClassToDegreeMajor (pitchClass (fs fz))                                                   = diatonicDegree (# 0)
pitchClassToDegreeMajor (pitchClass (fs (fs fz)))                                              = diatonicDegree (# 1)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs fz))))                                         = diatonicDegree (# 1)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs fz)))))                                    = diatonicDegree (# 2)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs fz))))))                               = diatonicDegree (# 3)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs fz)))))))                          = diatonicDegree (# 3)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs (fs fz))))))))                     = diatonicDegree (# 4)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))                = diatonicDegree (# 4)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))))           = diatonicDegree (# 5)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))      = diatonicDegree (# 5)
pitchClassToDegreeMajor (pitchClass (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))) = diatonicDegree (# 6)

degreeToPitchClassMajor : DiatonicDegree → PitchClass
degreeToPitchClassMajor (diatonicDegree fz)                               = pitchClass (# 0)
degreeToPitchClassMajor (diatonicDegree (fs fz))                          = pitchClass (# 2)
degreeToPitchClassMajor (diatonicDegree (fs (fs fz)))                     = pitchClass (# 4)
degreeToPitchClassMajor (diatonicDegree (fs (fs (fs fz))))                = pitchClass (# 5)
degreeToPitchClassMajor (diatonicDegree (fs (fs (fs (fs fz)))))           = pitchClass (# 7)
degreeToPitchClassMajor (diatonicDegree (fs (fs (fs (fs (fs fz))))))      = pitchClass (# 9)
degreeToPitchClassMajor (diatonicDegree (fs (fs (fs (fs (fs (fs fz))))))) = pitchClass (# 11)

pitchToDegreeCMajor : Pitch → DiatonicDegree
pitchToDegreeCMajor = pitchClassToDegreeMajor ∘ pitchToClass

d1 d2 d3 d4 d5 d6 d7 : DiatonicDegree
d1 = diatonicDegree (# 0)
d2 = diatonicDegree (# 1)
d3 = diatonicDegree (# 2)
d4 = diatonicDegree (# 3)
d5 = diatonicDegree (# 4)
d6 = diatonicDegree (# 5)
d7 = diatonicDegree (# 6)

thirdUp : DiatonicDegree → DiatonicDegree
thirdUp (diatonicDegree d) = diatonicDegree ((toℕ d + 2) mod diatonicScaleSize)

scaleSize : {n : ℕ} → Scale n → ℕ
scaleSize {n} _ = n

transposePitch : ℤ → Pitch → Pitch
transposePitch (+_     k) (pitch n) = pitch (n + k)
transposePitch (-[1+_] k) (pitch n) = pitch (n ∸ suc k)

-- Set of pitch classes represented as a bit vector.
PitchClassSet : Set
PitchClassSet = BitVec chromaticScaleSize

addToPitchClassSet : PitchClass → PitchClassSet → PitchClassSet
addToPitchClassSet (pitchClass p) ps = insert p ps

-- Standard Midi pitches

-- first argument is relative pitch within octave
-- second argument is octave (C5 = middle C for Midi)
standardMidiPitch : Fin chromaticScaleSize → ℕ → Pitch
standardMidiPitch p o = relativeToAbsolute (pitchClass p , octave o)

c c♯ d d♯ e f f♯ g g♯ a b♭ b : ℕ → Pitch
c  = standardMidiPitch (# 0)
c♯ = standardMidiPitch (# 1)
d  = standardMidiPitch (# 2)
d♯ = standardMidiPitch (# 3)
e  = standardMidiPitch (# 4)
f  = standardMidiPitch (# 5)
f♯ = standardMidiPitch (# 6)
g  = standardMidiPitch (# 7)
g♯ = standardMidiPitch (# 8)
a  = standardMidiPitch (# 9)
b♭ = standardMidiPitch (# 10)
b  = standardMidiPitch (# 11)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module Base.Prelude.Unit where

open import Data.Unit using (tt)         renaming (⊤ to ⊤ᵖ) public
open import Base.Free using (Free; pure)

⊤ : (S : Set) (P : S → Set) → Set
⊤ _ _ = ⊤ᵖ

pattern Tt = pure tt

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler