text:
------------------------------------------------------------------------
-- Preimages
------------------------------------------------------------------------

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

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module Preimage
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq as Bijection hiding (id; _∘_)
open Derived-definitions-and-properties eq
open import H-level eq as H-level
open import Injection eq hiding (id; _∘_)
open import Logical-equivalence using (module _⇔_)
open import Prelude
open import Surjection eq hiding (id; _∘_)

-- The preimage of y under f is denoted by f ⁻¹ y.

infix 5 _⁻¹_

_⁻¹_ : ∀ {a b} {A : Type a} {B : Type b} → (A → B) → B → Type (a ⊔ b)
f ⁻¹ y = ∃ λ x → f x ≡ y

-- Preimages under the identity function are contractible. (Note that
-- Singleton x is equal to id ⁻¹ x.)

id⁻¹-contractible : ∀ {a} {A : Type a} (y : A) →
                    Contractible (id ⁻¹ y)
id⁻¹-contractible = singleton-contractible

-- _⁻¹_ respects extensional equality of functions.

respects-extensional-equality :
  ∀ {a b} {A : Type a} {B : Type b} {f g : A → B} {y} →
  (∀ x → f x ≡ g x) → (f ⁻¹ y) ↔ (g ⁻¹ y)
respects-extensional-equality {f = f} {g} {y} f≡g = record
  { surjection = record
    { logical-equivalence = record
      { to   = to′
      ; from = from′
      }
    ; right-inverse-of = right-inverse-of
    }
  ; left-inverse-of = left-inverse-of
  }
  where
  to′ : f ⁻¹ y → g ⁻¹ y
  to′ (x , fx≡y) = x , (
    g x  ≡⟨ sym $ f≡g x ⟩
    f x  ≡⟨ fx≡y ⟩∎
    y    ∎)

  from′ : g ⁻¹ y → f ⁻¹ y
  from′ (x , gx≡y) = x , (
    f x  ≡⟨ f≡g x ⟩
    g x  ≡⟨ gx≡y ⟩∎
    y    ∎)

  abstract
    right-inverse-of : ∀ p → to′ (from′ p) ≡ p
    right-inverse-of = λ g⁻¹y → cong (_,_ (proj₁ g⁻¹y)) (
      let p = f≡g (proj₁ g⁻¹y); q = proj₂ g⁻¹y in
      trans (sym p) (trans p q)  ≡⟨ sym $ trans-assoc _ _ _ ⟩
      trans (trans (sym p) p) q  ≡⟨ cong (λ p → trans p q) (trans-symˡ _) ⟩
      trans (refl _) q           ≡⟨ trans-reflˡ _ ⟩∎
      q                          ∎)

    left-inverse-of : ∀ p → from′ (to′ p) ≡ p
    left-inverse-of = λ f⁻¹y → cong (_,_ (proj₁ f⁻¹y))
      let p = f≡g (proj₁ f⁻¹y); q = proj₂ f⁻¹y in
      trans p (trans (sym p) q)  ≡⟨ sym $ trans-assoc _ _ _ ⟩
      trans (trans p (sym p)) q  ≡⟨ cong (λ p → trans p q) (trans-symʳ _) ⟩
      trans (refl _) q           ≡⟨ trans-reflˡ _ ⟩∎
      q                          ∎

-- Split surjections can be lifted to preimages.

lift-surjection :
  ∀ {a b} {A : Type a} {B : Type b} (A↠B : A ↠ B) → let open _↠_ A↠B in
  ∀ {y} → (from ∘ to ⁻¹ y) ↠ (from ⁻¹ y)
lift-surjection {A = A} {B} A↠B {y} = record
  { logical-equivalence = record
    { to   = drop-∘
    ; from = add-∘
    }
  ; right-inverse-of = right-inv
  }
  where
  open _↠_ A↠B

  -- Given a preimage under (f ∘ g) a preimage under f can be
  -- constructed.

  drop-∘ : (from ∘ to) ⁻¹ y → from ⁻¹ y
  drop-∘ = Σ-map to id

  -- If f is a left inverse of g then the other direction also
  -- holds.

  abstract
    add-∘-lemma : ∀ {x} → from x ≡ y → from (to (from x)) ≡ y
    add-∘-lemma {x} from-x≡y =
      from (to (from x))  ≡⟨ cong from (right-inverse-of x) ⟩
      from x              ≡⟨ from-x≡y ⟩∎
      y                   ∎

  add-∘ : from ⁻¹ y → (from ∘ to) ⁻¹ y
  add-∘ (x , from-x≡y) = (from x , add-∘-lemma from-x≡y)

  abstract

    -- add-∘ is a right inverse of drop-∘.

    right-inv : (from⁻¹y : from ⁻¹ y) → drop-∘ (add-∘ from⁻¹y) ≡ from⁻¹y
    right-inv (x , from-x≡y) =
        (to (from x) , trans (cong from (right-inverse-of x)) from-x≡y)  ≡⟨ sym $ lemma (right-inverse-of x) from-x≡y ⟩∎
        (x           , from-x≡y)                                         ∎
      where
      lemma : ∀ {x y z} {f : B → A}
              (y≡x : y ≡ x) (p : f x ≡ z) →
              _≡_ {A = f ⁻¹ z} (x , p) (y , trans (cong f y≡x) p)
      lemma {z = z} {f} = elim
        (λ {y x} y≡x → (p : f x ≡ z) →
           _≡_ {A = f ⁻¹ z} (x , p) (y , trans (cong f y≡x) p))
        (λ x p → cong (_,_ x) (
           p                          ≡⟨ sym $ trans-reflˡ _ ⟩
           trans (refl (f x)) p       ≡⟨ cong (λ q → trans q p) (sym (cong-refl f)) ⟩∎
           trans (cong f (refl x)) p  ∎))

-- A consequence of the lemmas above is that preimages under a
-- bijection are contractible.

bijection⁻¹-contractible :
  ∀ {a b} {A : Type a} {B : Type b} (A↔B : A ↔ B) → let open _↔_ A↔B in
  ∀ y → Contractible (to ⁻¹ y)
bijection⁻¹-contractible A↔B =
  H-level.respects-surjection surj 0 ∘ id⁻¹-contractible
  where
  open _↔_ (Bijection.inverse A↔B)

  surj : ∀ {y} → id ⁻¹ y ↠ from ⁻¹ y
  surj {y} =
    id ⁻¹ y         ↠⟨ _↔_.surjection $
                         respects-extensional-equality (sym ∘ left-inverse-of) ⟩
    from ∘ to ⁻¹ y  ↠⟨ lift-surjection surjection ⟩□
    from ⁻¹ y       □

abstract

  -- Preimages under an injection into a set are propositional.

  injection⁻¹-propositional :
    ∀ {a b} {A : Type a} {B : Type b} (A↣B : A ↣ B) →
    let open _↣_ A↣B in
    Is-set B →
    ∀ y → Is-proposition (to ⁻¹ y)
  injection⁻¹-propositional A↣B B-set y (x₁ , tox₁≡y) (x₂ , tox₂≡y) =
    Σ-≡,≡→≡ (injective (to x₁  ≡⟨ tox₁≡y ⟩
                        y      ≡⟨ sym tox₂≡y ⟩∎
                        to x₂  ∎))
            (subst (λ x → to x ≡ y)
                   (injective (trans tox₁≡y (sym tox₂≡y)))
                   tox₁≡y                                   ≡⟨ B-set _ _ ⟩∎
             tox₂≡y                                         ∎)
    where
    open _↣_ A↣B

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Money where

import Agda.Builtin.IO as Builtin using (IO)
import Data.Rational as ℚ using (_+_; _*_)
open import Codata.Musical.Notation using (♯_)
open import Data.Nat using (ℕ; suc)
open import Data.Integer as ℤ using (+_)
open import Data.List using (List; []; _∷_)
open import Data.Rational as ℚ using (ℚ; 0ℚ; _/_)
open import Data.String using (String)
open import Data.Unit using (⊤)
open import Function using (_∘_) renaming (_$_ to _$$_)
open import IO using (putStrLn; IO; _>>_; run; sequence)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_)
open import Relation.Binary using (Decidable)
open import Relation.Nullary using (yes; no)
open import Codata.Musical.Colist as Colist using (fromList)
open Colist renaming (_∷_ to _::_)

data Currency : Set where
  € : Currency
  £ : Currency
  $ : Currency
  ¥ : Currency

data Money : Currency → Set where
  mkMoney : {c : Currency} → ℚ → Money c

noMoney : Money $
noMoney = mkMoney (+ 0 / 1)

_+_ : {c : Currency} → Money c → Money c → Money c
mkMoney x₁ + mkMoney x₂ =  mkMoney (x₁ ℚ.+ x₂)
infix 30 _+_

_*_ : {c : Currency} → ℚ → Money c → Money c
x * mkMoney y = mkMoney (x ℚ.* y)

record SomeMoney : Set where
  field
    currency : Currency
    money : Money currency

mkSomeMoney : Currency → ℚ → SomeMoney
mkSomeMoney currency amount = record { currency = currency; money = mkMoney amount }

record Trade : Set where
  constructor mkTrade
  field
    tPrice : SomeMoney
    tQty : ℚ

data Equal? (c₁ c₂ : Currency) : Set where
  eq : c₁ ≡ c₂ → Equal? c₁ c₂
  neq : c₁ ≢ c₂ → Equal? c₁ c₂

infix 4 _≟_
_≟_ : Decidable {A = Currency} _≡_
€ ≟ € = yes refl
€ ≟ £ = no (λ ())
€ ≟ $ = no (λ ())
€ ≟ ¥ = no (λ ())
£ ≟ € = no (λ ())
£ ≟ £ = yes refl
£ ≟ $ = no (λ ())
£ ≟ ¥ = no (λ ())
$ ≟ € = no (λ ())
$ ≟ £ = no (λ ())
$ ≟ $ = yes refl
$ ≟ ¥ = no (λ ())
¥ ≟ € = no (λ ())
¥ ≟ £ = no (λ ())
¥ ≟ $ = no (λ ())
¥ ≟ ¥ = yes refl

sumNotions : {c : Currency} → List Trade → Money c
sumNotions [] = mkMoney 0ℚ
sumNotions {c} (record { tPrice = record { currency = currency; money = money }; tQty = tQty } ∷ xs) with  c ≟ currency
... | yes refl = (tQty * money) +  sumNotions xs
... | no _ = sumNotions xs

_/1 : ℕ → ℚ
n /1 =  + n / 1

testTrades : List Trade
testTrades =
    mkTrade (mkSomeMoney £ (1 /1)) (100 /1)
  ∷ mkTrade (mkSomeMoney £ (2 /1)) (200 /1)
  ∷ mkTrade (mkSomeMoney $ (3 /1)) (300 /1)
  ∷ mkTrade (mkSomeMoney ¥ (5 /1)) (50 /1)
  ∷ []

open import Text.Printf using (printf)

showℚ : ℚ → String
showℚ record {numerator = n; denominator-1 = 0} = printf "%d" n
showℚ record {numerator = n; denominator-1 = d} = printf "%d/%u" n (suc d)

showCurrency : Currency → String
showCurrency € = "€"
showCurrency £ = "£"
showCurrency $ = "$"
showCurrency ¥ = "¥"

showMoney : {c : Currency} → Money c → String
showMoney {c} (mkMoney amount) = (printf "%s %s") (showCurrency c) (showℚ amount)

main : Builtin.IO (Colist ⊤)
main = run ∘ sequence ∘ fromList $$
    putStrLn "Hello, World!"
  ∷ putStrLn (showMoney $$ sumNotions {€} testTrades)
  ∷ putStrLn (showMoney $$ sumNotions {£} testTrades)
  ∷ putStrLn (showMoney $$ sumNotions {$} testTrades)
  ∷ putStrLn (showMoney $$ sumNotions {¥} testTrades)
  ∷ []

ext: agda

max_stars_repo_name: neosimsim/money-typed

max_issues_repo_name: neosimsim/money-typed

max_forks_repo_name: neosimsim/money-typed


text:
import cedille-options
module elab-util (options : cedille-options.options) where

open import general-util
open import cedille-types
open import syntax-util
open import type-util
open import ctxt
open import conversion
open import constants
open import instances
open import subst
open import rename
open import rewriting
open import free-vars
open import toplevel-state options {IO}
open import datatype-util
open import bohm-out

rename-validify : string → string
rename-validify = 𝕃char-to-string ∘ (h ∘ string-to-𝕃char) where
  validify-char : char → 𝕃 char
  validify-char '/' = [ '-' ]
  validify-char '.' = [ '-' ]
  validify-char c with
    (c =char 'a')  ||
    (c =char 'z')  ||
    (c =char 'A')  ||
    (c =char 'Z')  ||
    (c =char '\'') ||
    (c =char '-')  ||
    (c =char '_')  ||
    is-digit c     ||
    (c =char qual-local-chr)  ||
    (('a' <char c) && (c <char 'z')) ||
    (('A' <char c) && (c <char 'Z'))
  ...| tt = [ c ]
  ...| ff = 'Z' :: string-to-𝕃char (ℕ-to-string (toNat c)) ++ [ 'Z' ]
  h : 𝕃 char → 𝕃 char
  h [] = []
  h (c :: cs) = validify-char c ++ h cs

-- Returns a fresh variable name by adding primes and replacing invalid characters
fresh-var' : string → (string → 𝔹) → string
fresh-var' x f = fresh-h f (rename-validify x)

rename-new_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename-new ignored-var from Γ for f = f $ fresh-var' "x" (ctxt-binds-var Γ)
rename-new x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ)

rename_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename ignored-var from Γ for f = f ignored-var
rename x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ)

get-renaming : renamectxt → var → var → var × renamectxt
get-renaming ρₓ xₒ x = let x' = fresh-var' x (renamectxt-in-field ρₓ) in x' , renamectxt-insert ρₓ xₒ x'

rename_-_from_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - ignored-var from ρₓ for f = f ignored-var ρₓ
rename xₒ - x from ρₓ for f = uncurry f $ get-renaming ρₓ xₒ x

rename_-_lookup_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - x lookup ρₓ for f with renamectxt-lookup ρₓ xₒ
...| nothing = rename xₒ - x from ρₓ for f
...| just x' = f x' ρₓ

rename_from_and_for_ : ∀ {X : Set} → var → ctxt → renamectxt → (var → ctxt → renamectxt → X) → X
rename ignored-var from Γ and ρ for f = f ignored-var Γ ρ
rename x from Γ and ρ for f =
  let x' = fresh-var' x (λ x → ctxt-binds-var Γ x || renamectxt-in-field ρ x) in
  f x' (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x')

module reindexing (Γ : ctxt) (D I mn : var) (isₒ : indices) (psₜ : params) where

  rnm : Set
  rnm = qualif × stringset

  rnm-insert : rnm → var → var → rnm
  rnm-insert (q , s) xₒ xₙ = trie-insert q xₒ (xₙ , []) , stringset-insert s xₙ

  rnm-add : rnm → var → var → args → rnm
  rnm-add (q , s) xₒ xₙ as = trie-insert q xₒ (xₙ , as) , stringset-insert s xₙ

  rnm-binds : rnm → var → 𝔹
  rnm-binds (q , s) x = trie-contains q x || trie-contains s x

  reindex-fresh-var : rnm → trie indices → var → var
  reindex-fresh-var ρₓ is ignored-var = ignored-var
  reindex-fresh-var ρₓ is x =
    fresh-h (λ x' → ctxt-binds-var Γ x' || trie-contains is x' || rnm-binds ρₓ x') x

  rename-indices' : rnm → trie indices → indices
  rename-indices' ρₓ is = foldr {B = renamectxt → rnm → indices}
    (λ {(Index x atk) f r ρₓ →
       let x' = reindex-fresh-var ρₓ is x in
       Index x' (substh Γ r empty-trie -tk atk) :: f (renamectxt-insert r x x') (rnm-insert ρₓ x x')})
    (λ r ρₓ → []) isₒ empty-renamectxt ρₓ

  reindex-t : Set → Set
  reindex-t X = rnm → trie indices → X → X

  {-# TERMINATING #-}
  reindex : ∀ {ed} → reindex-t ⟦ ed ⟧

  rc-is : rnm → indices → rnm
  rc-is = foldr λ {(Index x atk) ρₓ → rnm-insert ρₓ x x}

  is-index-var : maybe tpkd → 𝔹
  is-index-var (just (Tkt (TpVar x))) = x =string I
  is-index-var _ = ff

  reindex {TERM} ρₓ is (AppEr t (Var x)) with trie-lookup is x
  ...| nothing = AppEr (reindex ρₓ is t) $ reindex ρₓ is $ Var x
  ...| just is' = indices-to-apps is' $ reindex ρₓ is t
  reindex {TERM} ρₓ is (App t t') =
    App (reindex ρₓ is t) (reindex ρₓ is t')
  reindex {TERM} ρₓ is (AppE t tT) =
    AppE (reindex ρₓ is t) (reindex ρₓ is -tT tT)
  reindex {TERM} ρₓ is (Beta t t') =
    Beta (reindex ρₓ is t) (reindex ρₓ is t')
  reindex {TERM} ρₓ is (Delta b? T t) =
    Delta (b? >>=c λ t₁ t₂ → just (reindex ρₓ is t₁ , reindex ρₓ is t₂))
          (reindex ρₓ is T) (reindex ρₓ is t)
  reindex {TERM} ρₓ is (Hole pi) =
    Hole pi
  reindex {TERM} ρₓ is (IotaPair t₁ t₂ x Tₓ) =
    let x' = reindex-fresh-var ρₓ is x in
    IotaPair (reindex ρₓ is t₁) (reindex ρₓ is t₂) x'
      (reindex (rnm-insert ρₓ x x') is Tₓ)
  reindex {TERM} ρₓ is (IotaProj t n) =
    IotaProj (reindex ρₓ is t) n
  reindex {TERM} ρₓ is (Lam me x tk? t) with is-index-var tk?
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    Lam me x' (reindex ρₓ is -tk_ <$> tk?) (reindex (rnm-insert ρₓ x x') is t)
  ...| tt with rename-indices' ρₓ is
  ...| isₙ = indices-to-lams isₙ $ reindex (rc-is ρₓ isₙ) (trie-insert is x isₙ) t
  reindex {TERM} ρₓ is (LetTm me x T? t t') =
    let x' = reindex-fresh-var ρₓ is x in
    LetTm me x' (reindex ρₓ is <$> T?) (reindex ρₓ is t) (reindex (rnm-insert ρₓ x x') is t')
  reindex {TERM} ρₓ is (LetTp x k T t) =
    let x' = reindex-fresh-var ρₓ is x in
    LetTp x' (reindex ρₓ is k) (reindex ρₓ is T) (reindex (rnm-insert ρₓ x x') is t)
  reindex {TERM} ρₓ is (Phi t₌ t₁ t₂) =
    Phi (reindex ρₓ is t₌) (reindex ρₓ is t₁) (reindex ρₓ is t₂)
  reindex {TERM} ρₓ is (Rho t₌ x Tₓ t) =
    let x' = reindex-fresh-var ρₓ is x in
    Rho (reindex ρₓ is t) x' (reindex (rnm-insert ρₓ x x') is Tₓ) (reindex ρₓ is t)
  reindex {TERM} ρₓ is (VarSigma t) =
    VarSigma (reindex ρₓ is t)
  reindex {TERM} ρₓ is (Var x) =
    maybe-else' (trie-lookup (fst ρₓ) x) (Var x) (uncurry (apps-term ∘ Var))
  reindex {TERM} ρₓ is (Mu μ t Tₘ? f~ cs) = Var "template-mu-not-allowed"
  reindex {TERM} ρₓ is (Sigma μ t Tₘ? f~ cs) = Var "template-sigma-not-allowed"

  reindex {TYPE} ρₓ is (TpAbs me x atk T) with is-index-var (just atk)
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    TpAbs me x' (reindex ρₓ is -tk atk) (reindex (rnm-insert ρₓ x x') is T)
  ...| tt = let isₙ = rename-indices' ρₓ is in
    indices-to-alls isₙ $ reindex (rc-is ρₓ isₙ) (trie-insert is x isₙ) T
  reindex {TYPE} ρₓ is (TpEq t₁ t₂) =
    TpEq (reindex ρₓ is t₁) (reindex ρₓ is t₂)
  reindex {TYPE} ρₓ is (TpIota x T T') =
    let x' = reindex-fresh-var ρₓ is x in
    TpIota x' (reindex ρₓ is T) (reindex (rnm-insert ρₓ x x') is T')
  reindex {TYPE} ρₓ is (TpAppTm T (Var x)) with trie-lookup is x
  ...| nothing = TpAppTm (reindex ρₓ is T) $ reindex ρₓ is $ Var x
  ...| just is' = indices-to-tpapps is' $ reindex ρₓ is T
  reindex {TYPE} ρₓ is (TpApp T tT) =
    TpApp (reindex ρₓ is T) (reindex ρₓ is -tT tT)
  reindex {TYPE} ρₓ is (TpHole pi) =
    TpHole pi
  reindex {TYPE} ρₓ is (TpLam x atk T) with is-index-var (just atk)
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    TpLam x' (reindex ρₓ is -tk atk) (reindex (rnm-insert ρₓ x x') is T)
  ...| tt = let isₙ = rename-indices' ρₓ is in
    indices-to-tplams isₙ $ reindex (rc-is ρₓ isₙ) (trie-insert is x isₙ) T
  reindex {TYPE} ρₓ is (TpVar x) =
    maybe-else' (trie-lookup (fst ρₓ) x) (TpVar x) (uncurry (apps-type ∘ TpVar))

  reindex {KIND} ρₓ is (KdAbs x atk k) with is-index-var (just atk)
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    KdAbs x' (reindex ρₓ is -tk atk) (reindex (rnm-insert ρₓ x x') is k)
  ...| tt = let isₙ = rename-indices' ρₓ is in
    indices-to-kind isₙ $ reindex (rc-is ρₓ isₙ) (trie-insert is x isₙ) k
  reindex {KIND} ρₓ is (KdHole pi) =
    KdHole pi
  reindex {KIND} ρₓ is KdStar =
    KdStar

  reindex-cmd : rnm → trie indices → cmd → cmd × rnm
  reindex-cmd ρₓ is (CmdImport (Import p? fp mnᵢ q? as)) =
    CmdImport (Import p? fp mnᵢ q? (reindex ρₓ is -arg_ <$> as)) , ρₓ
  reindex-cmd ρₓ is (CmdDefTerm x t) =
    let x' = D ^ "/" ^ x in
    CmdDefTerm x' (lam-expand-term psₜ $ reindex ρₓ is t) ,
    rnm-add ρₓ (mn # x) (ctxt.mn Γ # x') (params-to-args psₜ)
  reindex-cmd ρₓ is (CmdDefType x k T) =
    let x' = D ^ "/" ^ x in
    CmdDefType x' (abs-expand-kind psₜ $ reindex ρₓ is k)
                  (lam-expand-type psₜ $ reindex ρₓ is T) ,
    rnm-add ρₓ (mn # x) (ctxt.mn Γ # x') (params-to-args psₜ)
  reindex-cmd ρₓ is (CmdDefKind x ps k) =
    CmdDefKind x ps k , ρₓ
  reindex-cmd ρₓ is (CmdDefData es x ps k cs) =
    CmdDefData es x ps k cs , ρₓ

  reindex-cmds : cmds → cmds
  reindex-cmds cs =
    foldr {B = rnm → cmds}
      (λ c rec ρₓ → elim reindex-cmd ρₓ empty-trie c for λ c ρₓ → c :: rec ρₓ)
      (λ ρₓ → []) cs (empty-trie , empty-stringset)

{- we have to erase params to work around a situation like

data MyData (x : {β ≃ β}) : ★ =
| MyCtr : MyData.

erased-problem : ∀ x : {β ≃ β}. MyData x ➔ MyData β{λ x. x} =
  Λ x. λ d. μ' d { MyCtr ➔ MyCtr β{λ x. x} }.
  ^----------------------------------------^
... because the indicated term would elaborate to something like

Λ x. λ d. FixInd x ·MyData d ...
^-^              ^

and "x" is bound by an erased lambda, but is an unerased arg to FixInd!
(similar situations arise with fix-in/fix-out and with module parameters)
-}

reindex-file : ctxt → (D I modname : var) → indices → params → cmds → cmds
reindex-file Γ D I mn is ps cs =
  let ps' = params-set-erased Erased (ctxt.ps Γ ++ ps)
      open reindexing (add-params-to-ctxt ps' Γ) D I mn is ps' in
  reindex-cmds cs

mendler-elab-mu : ctxt → datatype-info → var → term → type → cases → term
mendler-elab-mu-pure : ctxt → datatype-info → var → term → cases → term

mendler-elab-sigma : ctxt → datatype-info → maybe term → term → type → cases → term
mendler-elab-sigma-pure : ctxt → datatype-info → maybe term → term → cases → term

-- Maps over expression, elaborating all mu-terms
{-# TERMINATING #-}
choose-mu : ∀ {ed} → ctxt → renamectxt → ⟦ ed ⟧ → ⟦ ed ⟧
choose-mu {TERM} Γ ρ (App tm tm') =
  App (choose-mu Γ ρ tm) (choose-mu Γ ρ tm')
choose-mu {TERM} Γ ρ (AppE tm tT) =
  AppE (choose-mu Γ ρ tm) (choose-mu Γ ρ -tT tT)
choose-mu {TERM} Γ ρ (Beta tm tm') =
  Beta (choose-mu Γ ρ tm) (choose-mu Γ ρ tm')
choose-mu {TERM} Γ ρ (Delta b? tp tm) =
  maybe-else' (b? >>=c λ t₁ t₂ →
               make-contradiction
                 (hnf Γ unfold-all (choose-mu Γ ρ t₁))
                 (hnf Γ unfold-all (choose-mu Γ ρ t₂)))
    (Delta nothing (choose-mu Γ ρ tp) (choose-mu Γ ρ tm)) λ f →
  rename "x" from Γ and ρ for λ x' _ _ →
  Delta (just (tt-term , ff-term)) (choose-mu Γ ρ tp)
    (Rho (choose-mu Γ ρ tm) x' (TpEq (App f (Var x')) ff-term) (Beta ff-term id-term))
choose-mu {TERM} Γ ρ (Hole pi) =
  Hole pi
choose-mu {TERM} Γ ρ (IotaPair tm₁ tm₂ x Tₓ) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  IotaPair (choose-mu Γ ρ tm₁) (choose-mu Γ ρ tm₂) x' (choose-mu Γ' ρ' Tₓ)
choose-mu {TERM} Γ ρ (IotaProj tm n) =
  IotaProj (choose-mu Γ ρ tm) n
choose-mu {TERM} Γ ρ (Lam e x tk? tm) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  Lam e x' (choose-mu Γ ρ -tk_ <$> tk?) (choose-mu Γ' ρ' tm)
choose-mu {TERM} Γ ρ (LetTm e x tp? tm tm') =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  LetTm e x' (choose-mu Γ ρ <$> tp?) (choose-mu Γ ρ tm) (choose-mu Γ' ρ' tm')
choose-mu {TERM} Γ ρ (LetTp x k T t) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  LetTp x' (choose-mu Γ ρ k) (choose-mu Γ ρ T) (choose-mu Γ' ρ' t)
choose-mu {TERM} Γ ρ (Phi tm₌ tm₁ tm₂) =
  Phi (choose-mu Γ ρ tm₌) (choose-mu Γ ρ tm₁) (choose-mu Γ ρ tm₂)
choose-mu {TERM} Γ ρ (Rho tm₌ x Tₓ tm) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  Rho (choose-mu Γ ρ tm₌) x' (choose-mu Γ' ρ' Tₓ) (choose-mu Γ ρ tm)
choose-mu {TERM} Γ ρ (VarSigma tm) =
  VarSigma (choose-mu Γ ρ tm)
choose-mu {TERM} Γ ρ (Mu x t tp? t~ ms) =
  choose-mu Γ ρ
    (maybe-else' tp?
      (mendler-elab-mu-pure Γ t~ x t ms)
      (λ tp → mendler-elab-mu Γ t~ x t tp ms))
choose-mu {TERM} Γ ρ (Sigma mt t tp? t~ ms) =
  choose-mu Γ ρ
    (maybe-else' tp?
      (mendler-elab-sigma-pure Γ t~ mt t ms)
      (λ tp → mendler-elab-sigma Γ t~ mt t tp ms))
choose-mu {TERM} Γ ρ (Var x) =
  Var (renamectxt-rep ρ x)
choose-mu {TYPE} Γ ρ (TpAbs e x tk tp) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  TpAbs e x' (choose-mu Γ ρ -tk tk) (choose-mu Γ' ρ' tp)
choose-mu {TYPE} Γ ρ (TpIota x tp₁ tp₂) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  TpIota x' (choose-mu Γ ρ tp₁) (choose-mu Γ' ρ' tp₂)
choose-mu {TYPE} Γ ρ (TpApp tp tT) =
  TpApp (choose-mu Γ ρ tp) (choose-mu Γ ρ -tT tT)
choose-mu {TYPE} Γ ρ (TpEq tmₗ tmᵣ) =
  TpEq (choose-mu Γ ρ tmₗ) (choose-mu Γ ρ tmᵣ)
choose-mu {TYPE} Γ ρ (TpHole pi) =
  TpHole pi
choose-mu {TYPE} Γ ρ (TpLam x tk tp) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  TpLam x' (choose-mu Γ ρ -tk tk) (choose-mu Γ' ρ' tp)
choose-mu {TYPE} Γ ρ (TpVar x) =
  TpVar (renamectxt-rep ρ x)
choose-mu {KIND} Γ ρ (KdAbs x tk kd) =
  rename x from Γ and ρ for λ x' Γ' ρ' →
  KdAbs x' (choose-mu Γ ρ -tk tk) (choose-mu Γ' ρ' kd)
choose-mu {KIND} Γ ρ (KdHole pi) =
  KdHole pi
choose-mu {KIND} Γ ρ KdStar =
  KdStar

-- Adds all Dₓ's encoding defs to the ctxt
ctxt-open-encoding-defs : var → ctxt → maybe ctxt
ctxt-open-encoding-defs Dₓ Γ =
  trie-lookup (ctxt.μ~ Γ) Dₓ >>=r λ xs →
  let tmd = λ t → term-def nothing opacity-open (just t) (TpHole pi-gen)
      tpd = λ T → type-def nothing opacity-open (just T) (KdHole pi-gen) in
  record Γ {
    i = foldr (uncurry λ x tT i →
          trie-insert i x
            (either-else' tT
              (tmd ∘ hnf (record Γ {i = i}) unfold-head)
              (tpd ∘ hnf (record Γ {i = i}) unfold-head-elab) ,
             missing-location)) (ctxt.i Γ) xs
  }

ctxt-open-all-encoding-defs : ctxt → ctxt
ctxt-open-all-encoding-defs Γ =
  foldr (λ Dₓ Γ → maybe-else Γ id $ ctxt-open-encoding-defs Dₓ Γ)
    Γ (trie-strings (ctxt.μ~ Γ))

mk-ctr-fmap-t : Set → Set
mk-ctr-fmap-t X = ctxt → (var × type × term) → X
{-# TERMINATING #-}
mk-ctr-fmap-η+ : mk-ctr-fmap-t (term → type → term)
mk-ctr-fmap-η- : mk-ctr-fmap-t (term → type → term)
mk-ctr-fmap-η? : 𝔹 → mk-ctr-fmap-t (term → type → term)
mk-ctr-fmap-η= : 𝔹 → mk-ctr-fmap-t (term → type → term)
mk-ctr-fmapₖ-η+ : mk-ctr-fmap-t (type → kind → type)
mk-ctr-fmapₖ-η- : mk-ctr-fmap-t (type → kind → type)
mk-ctr-fmapₖ-η? : 𝔹 → mk-ctr-fmap-t (type → kind → type)

-- TODO: Join fmap+ and fmap- into one function, to handle this for both strictly positive and strictly negative parameter occurrences in other datatypes
mk-ctr-fmap-η= f Γ x @ (Aₓ , Bₓ , castₓ) body T with decompose-ctr-type Γ T
...| TpVar x'' , as , rs =
  maybe-else' (data-lookup (add-params-to-ctxt as Γ) x'' rs) ((if f then mk-ctr-fmap-η+ else mk-ctr-fmap-η-) Γ x body T) λ where
    d @ (mk-data-info X _ asₚ asᵢ ps kᵢ k cs csₚₛ eds gds) →
      params-to-lams (if f then as else (substh-params Γ empty-renamectxt (trie-single Aₓ (, Bₓ)) as)) $
      let Γ' = add-params-to-ctxt as Γ
          recₓ = fresh-var Γ' "fmap"
          Γ' = ctxt-var-decl recₓ Γ'
          is = kind-to-indices Γ k
          uₓ = fresh-var (add-indices-to-ctxt is Γ') "u"
          vₓ = fresh-var (add-indices-to-ctxt is Γ') "v"
          Γ'' = ctxt-var-decl vₓ $ ctxt-var-decl uₓ $ add-indices-to-ctxt is Γ' in
      LetTm tt uₓ nothing
        (Mu recₓ
          (foldl
            (λ {(Param me x'' (Tkt T)) body →
                  (if me then AppEr body else App body) $
                     mk-ctr-fmap-η? (~ f) Γ' x (Var x'') T;
                (Param _ x'' (Tkk k)) body →
                  AppTp body $ mk-ctr-fmapₖ-η? (~ f) Γ' x (TpVar x'') k})
            body as)
          (just (indices-to-tplams is $
            TpLam uₓ (Tkt $ indices-to-tpapps is $ recompose-tpapps (args-to-tmtps asₚ) (TpVar X)) $
              TpIota vₓ (subst Γ'' Bₓ Aₓ (recompose-tpapps (args-to-tmtps asₚ) (TpVar X)))
                (TpEq (Var vₓ) (Var uₓ)))) d $
          flip map (map-snd (rename-var Γ'' (mu-Type/ recₓ) X) <$> inst-ctrs Γ'' ps asₚ cs) $ uncurry λ cₓ T → case decompose-ctr-type Γ T of λ where
            (Tₕ , as , rs) →
              Case cₓ (map (λ {(Param me x tk) → CaseArg me x (just tk)}) as)
                (let Xₚₛ = recompose-tpapps (args-to-tmtps asₚ) (TpVar X)
                     cg = mu-Type/ recₓ , Xₚₛ ,
                          (indices-to-lams is $ Lam ff vₓ (just (Tkt (indices-to-tpapps is (TpVar (mu-Type/ recₓ))))) (Phi (IotaProj (App (indices-to-apps is (Var recₓ)) (Var vₓ)) ι2) (IotaProj (App (indices-to-apps is (Var recₓ)) (Var vₓ)) ι1) (Var vₓ)))
                     t = foldl
                           (λ {(Param me x'' (Tkt T)) body →
                                 (if me then AppEr body else App body) $
                                   mk-ctr-fmap-η? f Γ' x (mk-ctr-fmap-η? ff Γ' cg (Var x'') T) (subst Γ'' Xₚₛ (mu-Type/ recₓ) T);
                               (Param _ x'' (Tkk k)) body →
                                 AppTp body $ mk-ctr-fmapₖ-η? f Γ' x (mk-ctr-fmapₖ-η? ff Γ' cg (TpVar x'') k) (subst Γ'' Xₚₛ (mu-Type/ recₓ) k)})
                           (subst (add-params-to-ctxt as Γ) Bₓ Aₓ (recompose-apps asₚ (Var cₓ))) as
                     tₑ = erase t in
                 IotaPair t (Beta tₑ tₑ) vₓ (TpEq (Var vₓ) tₑ))
                rs)
        (Phi (IotaProj (Var uₓ) ι2) (IotaProj (Var uₓ) ι1) (erase (params-to-apps as body)))
--  maybe-else' (ctxt-open-encoding-defs x'' Γ) (f Γ x body T)
--    λ Γ → f Γ x body (hnf-ctr Γ (fst x) T)
...| _ = (if f then mk-ctr-fmap-η+ else mk-ctr-fmap-η-) Γ x body T

mk-ctr-fmap-η? f Γ x body T with is-free-in (fst x) T
...| tt = mk-ctr-fmap-η= f Γ x body T
...| ff = body

mk-ctr-fmapₖ-η? f Γ x body k with is-free-in (fst x) k
...| tt = (if f then mk-ctr-fmapₖ-η+ else mk-ctr-fmapₖ-η-) Γ x body k
...| ff = body

mk-ctr-fmap-η+ Γ x @ (Aₓ , Bₓ , _) body T with decompose-ctr-type Γ T
...| Tₕ , as , _ =
  params-to-lams as $
  let Γ' = add-params-to-ctxt as Γ
      tₓ' = case Tₕ of λ where
              (TpIota x'' T₁ T₂) body →
                let t₁ = mk-ctr-fmap-η+ Γ' x (IotaProj body ι1) T₁
                    t₂ = mk-ctr-fmap-η+ Γ' x (IotaProj body ι2) (subst Γ' t₁ x'' T₂) in
                IotaPair t₁ t₂ x'' T₂
              _ body → body
  in
  tₓ' $ foldl
    (λ {(Param me x'' (Tkt T)) body →
          (if me then AppEr body else App body) $
            mk-ctr-fmap-η? ff Γ' x (Var x'') T;
        (Param _ x'' (Tkk k)) body →
          AppTp body $ mk-ctr-fmapₖ-η? ff Γ' x (TpVar x'') k})
    body as

mk-ctr-fmap-η- Γ xₒ @ (Aₓ , Bₓ , castₓ) body T with decompose-ctr-type Γ T
...| TpVar x'' , as , rs =
  params-to-lams (substh-params Γ empty-renamectxt (trie-single Aₓ (, Bₓ)) as) $
  let Γ' = add-params-to-ctxt as Γ in
  if x'' =string Aₓ
    then App (recompose-apps (tmtps-to-args Erased rs) castₓ)
    else id $
  foldl (λ {(Param me x'' (Tkt T)) body →
              (if me then AppEr body else App body) $
                 mk-ctr-fmap-η? tt Γ' xₒ (Var x'') T;
            (Param me x'' (Tkk k)) body →
              AppTp body $ mk-ctr-fmapₖ-η? tt Γ' xₒ (TpVar x'') k}) body as
...| TpIota x'' T₁ T₂ , as , [] =
  let Γ' = add-params-to-ctxt as Γ
      tₒ = foldl (λ where
            (Param me x'' (Tkt T)) body →
              (if me then AppEr body else App body) $
                mk-ctr-fmap-η? tt Γ' xₒ (Var x'') T
            (Param me x'' (Tkk k)) body →
              AppTp body $ mk-ctr-fmapₖ-η? tt Γ' xₒ (TpVar x'') k
           ) body as
      t₁ = mk-ctr-fmap-η? ff Γ' xₒ (IotaProj tₒ ι1) T₁
      t₂ = mk-ctr-fmap-η? ff Γ' xₒ (IotaProj tₒ ι2) ([ Γ' - t₁ / x'' ] T₂) in
  params-to-lams (substh-params Γ empty-renamectxt (trie-single Aₓ (, Bₓ)) as) $
  IotaPair t₁ t₂ x'' (subst (ctxt-var-decl x'' Γ') Bₓ Aₓ T₂)
...| Tₕ , as , rs = body

mk-ctr-fmapₖ-η+ Γ xₒ @ (Aₓ , Bₓ , castₓ) body k =
  let is = kind-to-indices Γ k in
  indices-to-tplams is $
  let Γ' = add-indices-to-ctxt is Γ in
  foldl
    (λ {(Index x'' (Tkt T)) → flip TpAppTm $ mk-ctr-fmap-η?  ff Γ' xₒ (Var x'') T;
        (Index x'' (Tkk k)) → flip TpAppTp $ mk-ctr-fmapₖ-η? ff Γ' xₒ (TpVar x'') k})
    body is

mk-ctr-fmapₖ-η- Γ xₒ @ (Aₓ , Bₓ , castₓ) body k with kind-to-indices Γ k
...| is =
  indices-to-tplams is $
  let Γ' = add-indices-to-ctxt is Γ in
  foldl (λ {(Index x'' (Tkt T)) → flip TpAppTm $ mk-ctr-fmap-η? tt Γ' xₒ (Var x'') T;
            (Index x'' (Tkk k)) → flip TpApp $ Ttp $ mk-ctr-fmapₖ-η? tt Γ' xₒ (TpVar x'') k})
    body is

mk-def : term → term
mk-def t = Phi (Beta t id-term) t (erase t)

top-type : type
top-type = TpEq id-term id-term

-- Index telescoping parameter
pattern IdxTele Iₓ = Param tt Iₓ (Tkk KdStar) :: []
pattern EncArgIdx I = ArgTp I
pattern EncArgCast Cast = ArgTp Cast
pattern EncArgCastIn cast-in = Arg cast-in
pattern EncArgCastOut cast-out = Arg cast-out
pattern EncArgCastIs cast-is = Arg cast-is
pattern EncArgFunctor Functor = ArgTp Functor
pattern EncArgFunctorIn functor-in = Arg functor-in
pattern EncArgFunctorOut functor-out = Arg functor-out
pattern EncArgFix Fix = ArgTp Fix
pattern EncArgFixIn fix-in = Arg fix-in
pattern EncArgFixOut fix-out = Arg fix-out
pattern EncArgLambek1 lambek1 = Arg lambek1
pattern EncArgLambek2 lambek2 = Arg lambek2
pattern EncArgFixInd fix-ind = Arg fix-ind
pattern EncArgs I Cast cast-in cast-out cast-is Functor functor-in functor-out
                Fix fix-in fix-out lambek1 lambek2 fix-ind =
  EncArgIdx I ::
  EncArgCast Cast ::
  EncArgCastIn cast-in ::
  EncArgCastOut cast-out ::
  EncArgCastIs cast-is ::
  EncArgFunctor Functor ::
  EncArgFunctorIn functor-in ::
  EncArgFunctorOut functor-out ::
  EncArgFix Fix ::
  EncArgFixIn fix-in ::
  EncArgFixOut fix-out ::
  EncArgLambek1 lambek1 ::
  EncArgLambek2 lambek2 ::
  EncArgFixInd fix-ind :: []

pattern EncImp fp I Cast cast-in cast-out cast-is Functor functor-in functor-out
               Fix fix-in fix-out lambek1 lambek2 fix-ind =
  CmdImport (Import _ fp _ _ (EncArgs
      I Cast cast-in cast-out cast-is Functor functor-in functor-out
      Fix fix-in fix-out lambek1 lambek2 fix-ind))

encode-datatype : ctxt → encoding-defs → datatype → encoding-defs
encode-datatype Γ eds @ (mk-enc-defs ecs _
                               Cast cast-in cast-out cast-is
                               Functor functor-in functor-out
                               Fix fix-in fix-out
                               lambek1 lambek2 fix-ind)
                  (Data Dₓ' ps is cs) =
  record eds {gcs = [: TypeF-cmd ⌟ IndF-cmd ⌟ fmap-cmd ⌟
                       D-cmd ⌟ Is-cmd ⌟ is-cmd ⌟ to-cmd ⌟
                       map ctr-cmd cs~ :] }
  where

  Γₚₛ = ctxt.ps Γ
  psₜ = params-set-erased Erased (Γₚₛ ++ ps)

  app-ps = params-to-apps psₜ ∘ Var
  tpapp-ps = params-to-tpapps psₜ ∘ TpVar

--  Cast = tpapp-ps Castₓ
--  cast-in = app-ps cast-inₓ
--  cast-out = app-ps cast-outₓ
--  cast-is = app-ps cast-isₓ
--  Functor = tpapp-ps Functorₓ
--  functor-in = app-ps functor-inₓ
--  functor-out = app-ps functor-outₓ
--  Fix = tpapp-ps Fixₓ
--  fix-in = app-ps fix-inₓ
--  fix-out = app-ps fix-outₓ
--  lambek1 = app-ps lambek1ₓ
--  lambek2 = app-ps lambek2ₓ
--  fix-ind = app-ps fix-indₓ

  mn = ctxt.mn Γ

  Γ' = add-params-to-ctxt psₜ Γ

  Dₓ = mn # Dₓ'
  cs~ = map-snd (subst Γ' (params-to-tpapps psₜ (TpVar Dₓ)) Dₓ) <$> cs
  cs' = map-snd (rename-var Γ' Dₓ Dₓ') <$> cs

  topᵢ = indices-to-kind is $ KdAbs ignored-var (Tkt top-type) KdStar

  mk-ctr-eterm : params → ctr → term
  mk-ctr-eterm ps (Ctr x _) =
    let xs = erase-params ps in
    Beta id-term $ foldr
      mlam
      (foldl (flip App ∘ Var) (Var x) xs)
      (map fst cs)

  mk-ctr-etype : ctxt → ctr → var → type
  mk-ctr-etype Γ (Ctr x T) X with decompose-ctr-type (ctxt-var-decl X Γ) T
  ...| Tₕ , as , rs =
    params-to-alls as $
    let rs' = if length rs =ℕ length psₜ + length is then drop (length psₜ) rs else rs in
    TpAppTm (recompose-tpapps rs' $ TpVar X) $ mk-ctr-eterm as (Ctr x T)

  {-
  for the datatype
    data Dₓ (p₁ : P₁) (p₂ : P₂)... : Π i₁ : I₁. Π i₂ : I₂. ... ★ =
      | c₁ : Π/∀ a₁ : A₁. Π/∀ a₂ : A₂. ... (Dₓ r₁ r₂...)
      | c₂ : ... .
  produce the functor type
  ∀ X : Π i₁ : I₁. Π i₂ : I₂. ... Π _ : Top. ★.
    (Π/∀ a₁ : A₁. Π/∀ a₂ : A₂. ... (X r₁ r₂ β<λ x. x>{λ c₁. λ c₂. ... |c₁ a₁ a₂...|})) →
     ... →
    X i₁ i₂... ιₓ
  -}
  mk-ftype2 : ctxt → (asᵢ : 𝕃 tmtp) → (ιₓ : var) → ctrs → type
  mk-ftype2 Γ asᵢ ιₓ cs =
    let Γ = ctxt-var-decl ιₓ Γ in
    rename "X" from Γ for λ X →
    TpAbs tt X (Tkk topᵢ) $
    foldr
      (λ c → TpAbs ff ignored-var $ Tkt $ mk-ctr-etype Γ c X)
      (TpAppTm (recompose-tpapps asᵢ $ TpVar X) $ Var ιₓ)
      cs

  mk-ctr-fterm : ctxt → ctr → ctrs → (as : params) → (rs : 𝕃 tmtp) → term
  mk-ctr-fterm Γ' (Ctr x' T) cs as rs =
    let Γ' = add-params-to-ctxt as Γ' in
    rename "X" from Γ' for λ Xₓ →
    rename "x" from Γ' for λ xₓ →
    let tkₓ = just (Tkk (indices-to-kind is (KdAbs ignored-var (Tkt top-type) KdStar)))
        fₜ = λ x T → Lam ff x (just (Tkt (mk-ctr-etype (ctxt-var-decl Xₓ Γ') (Ctr x T) Xₓ)))
        t = Lam tt Xₓ tkₓ (foldr (uncurry fₜ) (params-to-apps as (Var x')) cs) in
    IotaPair (Beta id-term (erase t)) t xₓ (mk-ftype2 (ctxt-var-decl xₓ Γ') rs xₓ cs)

  mk-ctr-ftype : ctxt → ctr → ctrs → var → type
  mk-ctr-ftype Γ (Ctr x T) cs X with decompose-ctr-type (ctxt-var-decl X Γ) T
  ...| Tₕ , as , rs =
    params-to-alls as $
    TpAppTm (recompose-tpapps rs $ TpVar X) $ mk-ctr-fterm (ctxt-var-decl X Γ) (Ctr x T) cs as rs

  Is/D = tpapp-ps (data-Is/ Dₓ)
  is/D = app-ps (data-is/ Dₓ)
  to/D = app-ps (data-to/ Dₓ)
  TypeF/D = tpapp-ps (data-TypeF/ Dₓ)
  IndF/D = tpapp-ps (data-IndF/ Dₓ)
  fmap/D = app-ps (data-fmap/ Dₓ)
  D = tpapp-ps Dₓ
  kᵢ = indices-to-kind is KdStar
  tkᵢ = Tkk kᵢ
  jtkᵢ = just tkᵢ

  decl-Γ : ctxt → 𝕃 var → ctxt
  decl-Γ = foldr ctxt-var-decl

  {-
  λ p₁ : P₁. λ p₂ : P₂. ...
    λ Dₓ : Π i₁ : I₁. Π i₂ : I₂. ... ★.
      λ i₁ : I₁. λ i₂ : I₂. ...
        ι ιₓ : Top. mk-ftype2 (ctxt-var-decl ιₓ Γ') ιₓ cs.
    -}
  TypeF-cmd = CmdDefType (data-TypeF/ Dₓ')
                (params-to-kind psₜ $ KdAbs ignored-var tkᵢ kᵢ) $
    let Γ' = add-indices-to-ctxt is Γ' in
    rename "x" from Γ' for λ ιₓ →
    params-to-tplams psₜ $
      TpLam Dₓ' (Tkk $ indices-to-kind is KdStar) $
        indices-to-tplams is $
          TpIota ιₓ top-type $ mk-ftype2 (ctxt-var-decl ιₓ Γ') (indices-to-tmtps is) ιₓ cs'

  fmap-cmd = CmdDefTerm (data-fmap/ Dₓ') $
    let Γ' = add-indices-to-ctxt is Γ' in
    rename "A" from Γ' for λ Aₓ →
    rename "B" from Γ' for λ Bₓ →
    rename "c" from Γ' for λ cₓ →
    rename "x" from Γ' for λ xₓ →
    rename "X" from Γ' for λ Xₓ →
    params-to-lams psₜ $
    let cs-a = map-snd (rename-var Γ' Dₓ Aₓ) <$> cs
        cs-b = map-snd (rename-var Γ' Dₓ Bₓ) <$> cs in
    AppEr (AppTp functor-in TypeF/D) $
    Lam tt Aₓ jtkᵢ $
    Lam tt Bₓ jtkᵢ $
    Lam tt cₓ (just (Tkt (TpAppTp (TpAppTp Cast (TpVar Aₓ)) (TpVar Bₓ)))) $
    AppEr (AppEr (AppTp (AppTp cast-in (TpAppTp TypeF/D (TpVar Aₓ)))
                                       (TpAppTp TypeF/D (TpVar Bₓ)))
      (indices-to-lams is $
       Lam ff xₓ (just (Tkt (indices-to-tpapps is (TpAppTp TypeF/D (TpVar Aₓ))))) $
       IotaPair (IotaProj (Var xₓ) ι1)
         (Lam tt Xₓ (just (Tkk topᵢ)) $
          flip (foldr $ uncurry λ x T → Lam ff x (just (Tkt
                 (mk-ctr-etype (decl-Γ Γ' [: Aₓ ⌟ Bₓ ⌟ cₓ ⌟ xₓ ⌟ Xₓ :]) (x , T) Xₓ)))) cs-b $
          foldl
            (flip App ∘ uncurry
              (λ bodyₓ T →
                mk-ctr-fmap-η?
                  tt
                  (decl-Γ Γ' [: Aₓ ⌟ Bₓ ⌟ cₓ ⌟ xₓ ⌟ Xₓ :])
                  (Aₓ , TpVar Bₓ , AppEr (AppTp (AppTp cast-out (TpVar Aₓ)) (TpVar Bₓ)) (Var cₓ))
                  (Var bodyₓ)
                  (hnf-ctr (decl-Γ Γ' [: Aₓ ⌟ Bₓ ⌟ cₓ ⌟ xₓ ⌟ Xₓ :]) Aₓ T)))
            (AppTp (IotaProj (Var xₓ) ι2) (TpVar Xₓ)) cs-a)
         xₓ (mk-ftype2 (decl-Γ Γ' [: Aₓ ⌟ Bₓ ⌟ cₓ ⌟ xₓ :]) (indices-to-tmtps is) xₓ cs-b)))
      (Beta id-term id-term)

  IndF-cmd = CmdDefTerm (data-IndF/ Dₓ') $
    params-to-lams psₜ $
    Lam tt Dₓ' jtkᵢ $
    indices-to-lams is $
    let Γ' = add-indices-to-ctxt is Γ' in
    rename "x" from Γ' for λ xₓ →
    rename "y" from Γ' for λ yₓ →
    rename "e" from Γ' for λ eₓ →
    rename "X" from Γ' for λ Xₓ →
    let T = indices-to-tpapps is (TpAppTp TypeF/D (TpVar Dₓ'))
        Γ' = ctxt-var-decl xₓ (ctxt-var-decl Xₓ Γ') in
    Lam ff xₓ (just $ Tkt T) $
    Lam tt Xₓ (just $ Tkk $ indices-to-kind is $ KdAbs ignored-var (Tkt T) KdStar) $
    flip (foldr λ c → Lam ff (fst c) (just (Tkt (mk-ctr-ftype Γ' c cs' Xₓ)))) cs' $
    flip AppEr (Beta (Var xₓ) id-term) $
    flip AppEr (Var xₓ) $
    let Γ' = decl-Γ Γ' [: xₓ ⌟ yₓ ⌟ eₓ ⌟ Xₓ :] in
    flip (foldl $ uncurry λ x' T' →
      case decompose-ctr-type Γ' T' of λ where
        (Tₕ , as , rs) →
          flip App $
          params-to-lams as $
          Lam tt yₓ (just (Tkt (recompose-tpapps rs (TpAppTp TypeF/D Tₕ)))) $
          Lam tt eₓ (just (Tkt (TpEq (Var yₓ) (mk-ctr-eterm as (Ctr x' T'))))) $
          params-to-apps as $
          Var x') cs' $
    AppTp (IotaProj (Var xₓ) ι2) $
    indices-to-tplams is $
    TpLam xₓ (Tkt top-type) $
    TpAbs tt yₓ (Tkt T) $
    TpAbs tt eₓ (Tkt $ TpEq (Var yₓ) (Var xₓ)) $
    TpAppTm (indices-to-tpapps is $ TpVar Xₓ) $
    Phi (Var eₓ) (Var yₓ) (Var xₓ)

  D-cmd = CmdDefType Dₓ' (params-to-kind (Γₚₛ ++ ps) kᵢ) $
    params-to-tplams (Γₚₛ ++ ps) $
    TpAppTm (TpApp Fix (Ttp TypeF/D)) fmap/D

  is-projn : ctxt → type → type → term → type
  is-projn Γ Tₘ Tₙ t =
    rename "i" from Γ for λ iₓ →
    TpIota iₓ
      (indices-to-alls is
        (TpAbs ff ignored-var (Tkt (indices-to-tpapps is Tₘ))
          (indices-to-tpapps is Tₙ)))
      (TpEq (Var iₓ) t)

  is-proj1 = λ Γ T → is-projn Γ T D id-term
  is-proj2 = λ Γ T → is-projn Γ T (TpAppTp TypeF/D T) fix-out

  is-proj' : ctxt → var → term → term
  is-proj' Γ Xₓ mu =
    rename "c" from Γ for λ cₓ →
    rename "o" from Γ for λ oₓ →
    let t = App (AppTp mu (is-proj1 (decl-Γ Γ (cₓ :: oₓ :: [])) (TpVar Xₓ)))
              (Lam ff cₓ (just (Tkt (is-proj1 (decl-Γ Γ (cₓ :: oₓ :: [])) (TpVar Xₓ))))
                (Lam ff oₓ (just (Tkt (is-proj2 (decl-Γ Γ (cₓ :: oₓ :: [])) (TpVar Xₓ))))
                  (Var cₓ))) in
    Phi (IotaProj t ι2) (IotaProj t ι1) id-term

  Is-cmd = CmdDefType (data-Is/ Dₓ') (params-to-kind (Γₚₛ ++ ps) $ KdAbs ignored-var tkᵢ KdStar) $
    params-to-tplams (Γₚₛ ++ ps) $
    rename "X" from Γ' for λ Xₓ →
    rename "Y" from Γ' for λ Yₓ →
    TpLam Xₓ tkᵢ $
    TpAbs tt Yₓ (Tkk KdStar) $
    TpAbs ff ignored-var
      (Tkt (TpAbs ff ignored-var (Tkt (is-proj1 (decl-Γ Γ' (Xₓ :: Yₓ :: [])) (TpVar Xₓ))) $
            TpAbs ff ignored-var (Tkt (is-proj2 (decl-Γ Γ' (Xₓ :: Yₓ :: [])) (TpVar Xₓ))) $
            TpVar Yₓ))
      (TpVar Yₓ)

  is-cmd = CmdDefTerm (data-is/ Dₓ') $
    params-to-lams (Γₚₛ ++ ps) $
    rename "Y" from Γ' for λ Yₓ →
    rename "f" from Γ' for λ fₓ →
    rename "x" from Γ' for λ xₓ →
    let pair = λ t → IotaPair t (Beta (erase t) (erase t)) xₓ (TpEq (Var xₓ) (erase t)) in
    Lam tt Yₓ (just (Tkk KdStar)) $
    Lam ff fₓ (just (Tkt (TpAbs ff ignored-var (Tkt (is-proj1 (ctxt-var-decl Yₓ Γ') D)) $
                          TpAbs ff ignored-var (Tkt (is-proj2 (ctxt-var-decl Yₓ Γ') D)) $
                          TpVar Yₓ))) $
    App (App (Var fₓ) (pair (indices-to-lams is (Lam ff xₓ (just (Tkt (indices-to-tpapps is D))) (Var xₓ)))))
        (pair (AppEr (AppTp fix-out TypeF/D) fmap/D))

  to-cmd = CmdDefTerm (data-to/ Dₓ') $
    rename "Y"  from Γ' for λ Yₓ  →
    rename "mu" from Γ' for λ muₓ →
    params-to-lams (Γₚₛ ++ ps) $
    Lam tt Yₓ jtkᵢ $
    Lam tt muₓ (just (Tkt (TpApp Is/D (Ttp (TpVar Yₓ))))) $
    is-proj' (decl-Γ Γ' (Yₓ :: muₓ :: [])) Yₓ (Var muₓ)

  ctr-cmd : ctr → cmd
  ctr-cmd (Ctr x' T) with subst Γ' D Dₓ' T
  ...| T' with decompose-ctr-type Γ' T'
  ...| Tₕ , as , rs = CmdDefTerm x' $
    let Γ' = add-params-to-ctxt as Γ'
        rs = drop (length (Γₚₛ ++ ps)) rs in
    params-to-lams (Γₚₛ ++ ps) $
    params-to-lams as $
    App (recompose-apps (tmtps-to-args tt rs) $
          AppEr (AppTp fix-in TypeF/D) fmap/D) $
    mk-ctr-fterm Γ' (Ctr x' T) cs~ as rs

init-encoding : ctxt → file → datatype → string ⊎ encoding-defs
init-encoding Γ (Module mn (IdxTele Iₓ) mcs) d @ (Data Dₓ ps is cs) =
  case reverse (reindex-file Γ Dₓ Iₓ mn is ps mcs) of λ where
    (EncImp fp Iₓ'
        Cast cast-in cast-out cast-is
        Functor functor-in functor-out
        Fix fix-in fix-out
        lambek1 lambek2 fix-ind :: mcs) →
      err⊎-guard (~ conv-type Γ Iₓ' (TpVar Iₓ))
        "Index telescoping argument to last import differs from the parameter" >>
      return (encode-datatype Γ (mk-enc-defs (reverse mcs) []
                          Cast cast-in cast-out cast-is
                          Functor functor-in functor-out
                          Fix fix-in fix-out
                          lambek1 lambek2 fix-ind) d)
    (CmdImport (Import p? fn mn q? as) :: mcsᵣ) →
      inj₁ $ "Expected 14 import args, but got" ^ rope-to-string (strRun Γ (args-to-string as))
    mcsᵣ →
      inj₁ "Datatype encodings must end with import ~/.cedille/Template.ced"
  where open import to-string options
init-encoding Γ (Module mn mps mcs) (Data Dₓ ps is cs) =
  inj₁ $ "Datatype encodings must have a single module parameter of kind star, " ^
         "for index telescoping"

mendler-elab-mu-pure Γ (mk-data-info _ _ _ _ _ _ _ _ _ eds ecs) xₒ t ms =
  let fix-ind = erase (encoding-defs.fix-ind eds)
      msf = λ t → foldl
                    (λ {(Case mₓ cas mₜ asₜₚ) t →
                          App t (case-args-to-lams cas mₜ)})
                    t ms in
    rename xₒ from Γ for λ x →
    rename "y" from Γ for λ yₓ →
      let subst-msf = subst-renamectxt Γ
            (renamectxt-insert* empty-renamectxt ((xₒ , x) :: (yₓ , yₓ) :: [])) ∘ msf in
        App (App fix-ind t) (Lam ff x nothing $ Lam ff yₓ nothing $ subst-msf (Var yₓ))

mendler-elab-mu Γ (mk-data-info X Xₒ asₚ asᵢ ps kᵢ k cs csₚₛ (mk-enc-defs ecs gcs Cast cast-in cast-out cast-is Functor functor-in functor-out Fix fix-in fix-out lambek1 lambek2 fix-ind) (mk-encd-defs Is/Dₓ is/Dₓ to/Dₓ TypeF/Dₓ indF/Dₓ fmap/Dₓ)) x t Tₘ ms =
  let is = kind-to-indices Γ k
      Γᵢₛ = add-indices-to-ctxt is $ add-params-to-ctxt ps $ add-params-to-ctxt (ctxt.ps Γ) Γ
      is/X? = unless (X =string Xₒ) (Var (mu-isType/' Xₒ))
      app-ps = recompose-apps (args-set-erased tt asₚ) ∘ Var
      tpapp-ps = recompose-tpapps (args-to-tmtps asₚ) ∘ TpVar
      app-ps' = inst-term Γ ps asₚ
      tpapp-ps' = inst-type Γ ps asₚ
      fmap/D = app-ps fmap/Dₓ
      TypeF/D = tpapp-ps TypeF/Dₓ
      indF/D = app-ps indF/Dₓ
      Cast = tpapp-ps' Cast
      cast-out = app-ps' cast-out
      Functor = tpapp-ps' Functor
      functor-in = app-ps' functor-in
      functor-out = app-ps' functor-out
      Fix = tpapp-ps' Fix
      fix-in = app-ps' fix-in
      fix-out = app-ps' fix-out
      lambek1 = app-ps' lambek1
      fix-ind = app-ps' fix-ind
      Xₜₚ = recompose-tpapps (args-to-tmtps asₚ) (TpVar X)
      Xₒₜₚ = if Xₒ =string X then Xₜₚ else TpVar Xₒ
      toₓ = rename "to" from Γᵢₛ for id
      outₓ = rename "out" from Γᵢₛ for id
      to-tp = λ R → TpAppTp (TpAppTp Cast R) Xₜₚ
      out-tp = λ R → TpIota outₓ (indices-to-alls is (TpAbs ff ignored-var (Tkt (indices-to-tpapps is R)) (indices-to-tpapps is (TpAppTp TypeF/D R)))) (TpEq (Var outₓ) fix-out)
      ms' : trie term
      ms' = foldr (λ c σ → case c of λ {(Case x cas t asₜₚ) →
                let Γ' = add-caseArgs-to-ctxt cas Γᵢₛ in
                trie-insert σ x $
                rename "y" from Γ' for λ yₓ →
                rename "e" from Γ' for λ eₓ →
                rename "x" from Γ' for λ xₓ →
                case-args-to-lams cas $
                Lam tt yₓ (just (Tkt (recompose-tpapps (drop (length asₚ) asₜₚ) Xₜₚ))) $
                Lam tt eₓ (just (Tkt (TpEq (App fix-in (foldr (uncurry λ x T → Lam ff (snd (split-var x)) nothing) (foldl (λ ca t → case ca of λ {(CaseArg ff x _) → App t (Var (snd (split-var x))); _ → t}) (Var (snd (split-var x))) cas) cs)) (Var yₓ)))) $
                Rho (VarSigma (Var eₓ)) xₓ (TpAppTm (recompose-tpapps (drop (length asₚ) asₜₚ) Tₘ) (Var xₓ)) t})
              empty-trie ms
      in-fix = λ is/X? T asᵢ t →
        (App (recompose-apps asᵢ (AppEr (AppTp fix-in TypeF/D) fmap/D)) (maybe-else' is/X? t λ is/X →
        App (recompose-apps asᵢ (AppEr (AppTp (AppTp cast-out (TpAppTp TypeF/D T)) (TpAppTp TypeF/D Xₜₚ)) (AppEr (AppTp (AppTp fmap/D T) Xₜₚ) (App (AppTp is/X (to-tp T)) (Lam ff "to" (just (Tkt (to-tp T))) $ Lam ff "out" (just (Tkt (out-tp T))) $ Var "to"))))) t))
      app-lambek = λ is/X? t T asᵢ body → AppEr (AppEr body (in-fix is/X? T asᵢ t))
        (App (recompose-apps asᵢ (AppEr (AppTp lambek1 TypeF/D) fmap/D)) (in-fix is/X? T asᵢ t)) in
  rename "x" from Γᵢₛ for λ xₓ →
  rename "y" from Γᵢₛ for λ yₓ →
  rename "y'" from ctxt-var-decl yₓ Γᵢₛ for λ y'ₓ →
  rename "z" from Γᵢₛ for λ zₓ →
  rename "e" from Γᵢₛ for λ eₓ →
  rename "X" from Γᵢₛ for λ Xₓ →
  maybe-else (Var "1") id $
  foldl {B = maybe (term → term)} -- Agda hangs without this implicit argument...?
    (uncurry λ x Tₓ rec → rec >>= λ rec → trie-lookup ms' x >>= λ t →
      just λ tₕ → App (rec tₕ) t) (just λ t → t) cs >>= λ msf →
  maybe-else (just $ Var "2") just $
  just
    (let Rₓ = mu-Type/ x
         isRₓ = mu-isType/ x
         fcₜ = AppEr (AppTp (AppTp cast-out (TpAppTp TypeF/D (TpVar Rₓ))) (TpAppTp TypeF/D Xₜₚ))
                 (AppEr (AppTp (AppTp fmap/D (TpVar Rₓ)) Xₜₚ) (Var toₓ))
         Tₘₐ = TpLam Rₓ (Tkk (indices-to-kind is KdStar)) Tₘ
         Tₘ-fmap = rename "A" from Γᵢₛ for λ Aₓ →
                  rename "B" from Γᵢₛ for λ Bₓ →
                  rename "c" from Γᵢₛ for λ cₓ →
                  rename "d" from Γᵢₛ for λ dₓ →
                  rename "q" from Γᵢₛ for λ qₓ →
                  let Γ' = foldr ctxt-var-decl Γ (Aₓ :: Bₓ :: cₓ :: dₓ :: qₓ :: [])
                      Tₘₐ' = TpAppTm (indices-to-tpapps is (TpAppTp Tₘₐ (TpVar Aₓ))) (Var dₓ)
                      Tₘₐₕ = hnf-ctr Γ' Aₓ Tₘₐ' in
                  Lam tt Aₓ (just (Tkk k)) $
                  Lam tt Bₓ (just (Tkk k)) $
                  Lam tt cₓ (just (Tkt (TpAppTp (TpAppTp Cast (TpVar Aₓ)) (TpVar Bₓ)))) $
                  indices-to-lams is $
                  Lam tt dₓ (just (Tkt (indices-to-tpapps is Xₜₚ))) $
                  IotaPair (Lam ff qₓ (just (Tkt Tₘₐ')) (mk-ctr-fmap-η? ff Γ' (Aₓ , TpVar Bₓ , AppEr (AppTp (AppTp cast-out (TpVar Aₓ)) (TpVar Bₓ)) (Var cₓ)) (Var qₓ) Tₘₐₕ)) (Beta id-term id-term) qₓ (TpEq (Var qₓ) id-term)
    in
    App (AppEr (AppTp (App (recompose-apps (tmtps-to-args tt asᵢ) (AppEr (AppTp fix-ind TypeF/D) fmap/D)) t) Tₘₐ) Tₘ-fmap)
      (Lam tt Rₓ (just (Tkk k)) $
       Lam tt toₓ (just (Tkt (to-tp (TpVar Rₓ)))) $
       Lam tt outₓ (just (Tkt (out-tp (TpVar Rₓ)))) $
       Lam ff x (just (Tkt (indices-to-alls is (TpAbs ff xₓ (Tkt (indices-to-tpapps is (TpVar Rₓ))) (TpAppTm (indices-to-tpapps is Tₘ) (App (indices-to-apps is (AppEr (AppTp (AppTp cast-out (TpVar Rₓ)) Xₜₚ) (Var toₓ))) (Var xₓ))))))) $
       indices-to-lams is $
       Lam ff yₓ (just (Tkt (indices-to-tpapps is (TpAppTp TypeF/D (TpVar Rₓ))))) $
       LetTm tt isRₓ nothing
           (Lam tt Xₓ (just (Tkk KdStar)) $
            Lam ff xₓ (just (Tkt (TpAbs ff ignored-var (Tkt (to-tp (TpVar Rₓ)))
                                   (TpAbs ff ignored-var (Tkt (out-tp (TpVar Rₓ)))
                                     (TpVar Xₓ))))) $
            App (App (Var xₓ) (Var toₓ)) (Var outₓ))
       (app-lambek (just $ Var isRₓ) (Var yₓ) (TpVar Rₓ) (indices-to-args is) $ msf
         (AppTp (Phi (Beta (Var yₓ) id-term) (App (indices-to-apps is (AppTp indF/D (TpVar Rₓ))) (Var yₓ)) (Var yₓ))
           (indices-to-tplams is $
            TpLam yₓ (Tkt $ indices-to-tpapps is (TpAppTp TypeF/D (TpVar Rₓ))) $
            TpAbs tt y'ₓ (Tkt $ indices-to-tpapps is Xₜₚ) $
            TpAbs tt eₓ (Tkt $ TpEq (App fix-in (Var yₓ)) (Var y'ₓ)) $
             TpAppTm (indices-to-tpapps is Tₘ) (Phi (Var eₓ)
               (App (indices-to-apps is (AppEr (AppTp fix-in TypeF/D) fmap/D))
                    (App (indices-to-apps is fcₜ) (Var yₓ)))
               (Var y'ₓ)))))))

mendler-elab-sigma-pure Γ (mk-data-info _ _ _ _ _ _ _ _ _ eds ecs) x? t ms =
  let fix-out = erase (encoding-defs.fix-out eds)
      msf = λ t → foldl
                    (λ {(Case mₓ cas mₜ asₜₚ) t →
                          App t (case-args-to-lams cas mₜ)})
                    t ms in
  msf (App fix-out t)

mendler-elab-sigma Γ (mk-data-info X Xₒ asₚ asᵢ ps kᵢ k cs csₚₛ (mk-enc-defs ecs gcs Cast cast-in cast-out cast-is Functor functor-in functor-out Fix fix-in fix-out lambek1 lambek2 fix-ind) (mk-encd-defs Is/Dₓ is/Dₓ to/Dₓ TypeF/Dₓ indF/Dₓ fmap/Dₓ)) mt t Tₘ ms =
  let is = kind-to-indices Γ k
      Γᵢₛ = add-indices-to-ctxt is $ add-params-to-ctxt ps $ add-params-to-ctxt (ctxt.ps Γ) Γ
      is/X? = mt
      app-ps = recompose-apps (args-set-erased tt asₚ) ∘ Var
      tpapp-ps = recompose-tpapps (args-to-tmtps asₚ) ∘ TpVar
      app-ps' = inst-term Γ ps asₚ
      tpapp-ps' = inst-type Γ ps asₚ
      fmap/D = app-ps fmap/Dₓ
      TypeF/D = tpapp-ps TypeF/Dₓ
      to/D = recompose-apps asₚ (Var to/Dₓ)
      indF/D = app-ps indF/Dₓ
      Cast = tpapp-ps' Cast
      cast-out = app-ps' cast-out
      functor-out = app-ps' functor-out
      Fix = tpapp-ps' Fix
      fix-in = app-ps' fix-in
      fix-out = app-ps' fix-out
      lambek1 = app-ps' lambek1
      Xₜₚ = recompose-tpapps (args-to-tmtps asₚ) (TpVar X)
      Xₒₜₚ = if Xₒ =string X then Xₜₚ else TpVar Xₒ
      toₓ = rename "to" from Γᵢₛ for id
      outₓ = rename "out" from Γᵢₛ for id
      to-tp = λ R → TpAppTp (TpAppTp Cast R) Xₜₚ
      out-tp = λ R → TpIota outₓ (indices-to-alls is (TpAbs ff ignored-var (Tkt (indices-to-tpapps is R)) (indices-to-tpapps is (TpAppTp TypeF/D R)))) (TpEq (Var outₓ) fix-out)
      ms' : trie term
      ms' = foldr (λ c σ → case c of λ {(Case x cas t asₜₚ) →
                let Γ' = add-caseArgs-to-ctxt cas Γᵢₛ in
                trie-insert σ x $
                rename "y" from Γ' for λ yₓ →
                rename "e" from Γ' for λ eₓ →
                rename "x" from Γ' for λ xₓ →
                case-args-to-lams cas $
                Lam tt yₓ (just (Tkt (recompose-tpapps (drop (length asₚ) asₜₚ) Xₜₚ))) $
                Lam tt eₓ (just (Tkt (TpEq (App fix-in (foldr (uncurry λ x T → Lam ff (snd (split-var x)) nothing) (foldl (λ ca t → case ca of λ {(CaseArg ff x _) → App t (Var (snd (split-var x))); _ → t}) (Var (snd (split-var x))) cas) cs)) (Var yₓ)))) $
                Rho (VarSigma (Var eₓ)) xₓ (TpAppTm (recompose-tpapps (drop (length asₚ) asₜₚ) Tₘ) (Var xₓ)) t})
              empty-trie ms
      in-fix = λ is/X? T asᵢ t →
        (maybe-else' (is/X? ||-maybe mt) t λ is/X → App (recompose-apps asᵢ (AppEr (AppTp (AppTp cast-out T) Xₜₚ) (App (AppTp is/X (to-tp T)) (Lam ff "to" (just (Tkt (to-tp T))) $ Lam ff "out" (just (Tkt (out-tp T))) $ Var "to")))) t)
      app-lambek = λ is/X? t T asᵢ body → AppEr (AppEr body (in-fix is/X? T asᵢ t))
        (App (recompose-apps asᵢ (AppEr (AppTp lambek1 TypeF/D) fmap/D)) (in-fix is/X? T asᵢ t)) in
  rename "x" from Γᵢₛ for λ xₓ →
  rename "y" from Γᵢₛ for λ yₓ →
  rename "y'" from ctxt-var-decl yₓ Γᵢₛ for λ y'ₓ →
  rename "z" from Γᵢₛ for λ zₓ →
  rename "e" from Γᵢₛ for λ eₓ →
  rename "X" from Γᵢₛ for λ Xₓ →
  maybe-else (Var "1") id $
  foldl {B = maybe (term → term)} -- Agda hangs without this implicit argument...?
    (uncurry λ x Tₓ rec → rec >>= λ rec → trie-lookup ms' x >>= λ t →
      just λ tₕ → App (rec tₕ) t) (just λ t → t) cs >>= λ msf →
  maybe-else (just $ Var "2") just $
  just $
    (app-lambek is/X? t Xₒₜₚ
             (tmtps-to-args tt asᵢ) (msf
      (let Tₛ = maybe-else' is/X? Xₜₚ λ _ → Xₒₜₚ
           fcₜ = maybe-else' is/X? id λ is/X → App $ indices-to-apps is $
             AppEr (AppTp (AppTp cast-out (TpAppTp TypeF/D Tₛ)) (TpAppTp TypeF/D Xₜₚ))
               (AppEr (AppTp (AppTp (AppEr (AppTp functor-out TypeF/D) fmap/D) Tₛ) Xₜₚ) (App (AppTp is/X (to-tp Tₛ)) (Lam ff "to" (just (Tkt (to-tp Tₛ))) $ Lam ff "out" (just (Tkt (out-tp Tₛ))) $ Var "to")))
           out = maybe-else' is/X? (AppEr (AppTp fix-out TypeF/D) fmap/D) λ is/X →
             let i = App (AppTp is/X (TpIota xₓ (indices-to-alls is (TpAbs ff ignored-var (Tkt (indices-to-tpapps is Tₛ)) (indices-to-tpapps is (TpAppTp TypeF/D Tₛ)))) (TpEq (Var xₓ) fix-out))) (Lam ff "to" (just (Tkt (to-tp Tₛ))) $ Lam ff "out" (just (Tkt (out-tp Tₛ))) $ Var "out") in
             Phi (IotaProj i ι2) (IotaProj i ι1) fix-out in
      AppTp (App (recompose-apps (tmtps-to-args tt asᵢ) (AppTp indF/D Tₛ)) (App (recompose-apps (tmtps-to-args tt asᵢ) out) t))
        (indices-to-tplams is $ TpLam yₓ (Tkt $ indices-to-tpapps is (TpAppTp TypeF/D Tₛ)) $
           TpAbs tt y'ₓ (Tkt $ indices-to-tpapps is Xₜₚ) $
           TpAbs tt eₓ (Tkt (TpEq (App fix-in (Var yₓ)) (Var y'ₓ))) $
           TpAppTm (indices-to-tpapps is Tₘ) (Phi (Var eₓ)
             (App (indices-to-apps is (AppEr (AppTp fix-in TypeF/D) fmap/D)) (fcₜ (Var yₓ))) (Var y'ₓ))))))

{- ################################ IO ################################ -}

-- set show-qualified-vars to tt to show if there are bugs in parameter code, because
-- they should always be captured by the scope and unqualified as a binder name
open import to-string (record options {during-elaboration = tt; show-qualified-vars = tt; erase-types = ff; pretty-print = tt})

{-# TERMINATING #-}
cmds-to-string : (newline-before-after : 𝔹) → params → cmds → strM
cmd-to-string : params → cmd → strM
cmd-to-string ps (CmdDefTerm x t) = strBreak 2
  0 [ strVar x >>str strAdd " =" ]
  2 [ to-stringh (lam-expand-term ps t) >>str strAdd "." ]
cmd-to-string ps (CmdDefType x k T) = strBreak 3
  0 [ strVar x >>str strAdd " :" ]
  (3 + string-length x) [ to-stringh (abs-expand-kind ps k) >>str strAdd " =" ]
  2 [ to-stringh (lam-expand-type ps T)  >>str strAdd "." ]
cmd-to-string ps (CmdDefKind x psₖ k) = strBreak 2
  0 [ strVar x ]
  2 [ params-to-string'' (ps ++ psₖ) (to-stringh k) >>str strAdd "." ]
cmd-to-string ps (CmdDefData eds x psₓ k cs) =
  cmds-to-string ff ps (encoding-defs.ecs eds) >>str
  strList 2
    (strBreak 2
      0 [ strAdd "data " >>str strVar x ]
      (5 + string-length x) [ params-to-string'' (ps ++ psₓ)
                                (strAdd ": " >>str to-stringh k) ] ::
     map (uncurry λ x T → strBreak 2
       0 [ strAdd "| " >>str strVar x >>str strAdd " :" ]
       (5 + string-length x) [ to-stringh T ]) cs) >>str strAdd "."
cmd-to-string ps (CmdImport (Import p? fp mn q? as)) =
  strAdd "import " >>str
  strAdd mn >>str
  maybe-else' q? strEmpty (λ x → strAdd " as " >>str strAdd x) >>str
  args-to-string as >>str
  strAdd "."

cmds-to-string b-a ps =
  let b-a-tt : cmd → strM → strM
      b-a-tt = λ c cs → strLine >>str strLine >>str cmd-to-string ps c >>str cs
      b-a-ff : cmd → strM → strM
      b-a-ff = λ c cs → cmd-to-string ps c >>str cs >>str strLine >>str strLine in
  foldr (if b-a then b-a-tt else b-a-ff) strEmpty

file-to-string : file → strM
file-to-string (Module mn ps cs) =
  strAdd "module " >>str
  strAdd mn >>str
  strAdd "." >>str
  cmds-to-string tt [] cs
  --cmds-to-string tt ps cs

record elab-info : Set where
  constructor mk-elab-info
  field
    τ : toplevel-state
    ρ : renamectxt
    φ : renamectxt × trie file
    ν : trie stringset -- dependency mapping

new-elab-info : toplevel-state → elab-info
new-elab-info ts = mk-elab-info ts empty-renamectxt (empty-renamectxt , empty-trie) empty-trie

ts-def : toplevel-state → var → tmtp → toplevel-state
ts-def ts x tT =
  let Γ = toplevel-state.Γ ts
      i = ctxt.i Γ
      d = either-else' tT
            (λ t → term-def nothing opacity-open (just t) (TpHole pi-gen))
            (λ T → type-def nothing opacity-open (just T) (KdHole pi-gen)) in
  record ts { Γ = record Γ { i = trie-insert i x (d , missing-location) } }

add-dep : elab-info → var → elab-info
add-dep (mk-elab-info τ ρ φ ν) mnᵢ =
  let fp = ctxt.fn (toplevel-state.Γ τ)
      mnᵢ-is = stringset-strings (trie-lookup-else empty-trie ν mnᵢ)
      mn-is = trie-lookup-else empty-trie ν fp in
  mk-elab-info τ ρ φ (trie-insert ν fp (foldr (flip stringset-insert) (stringset-insert mn-is mnᵢ) mnᵢ-is))

set-fn : elab-info → filepath → elab-info
set-fn (mk-elab-info τ ρ φ ν) fn = mk-elab-info (record τ { Γ = record (toplevel-state.Γ τ) { fn = fn } }) ρ φ ν

set-mn : elab-info → var → elab-info
set-mn (mk-elab-info τ ρ φ ν) mn = mk-elab-info (record τ { Γ = record (toplevel-state.Γ τ) { mn = mn } }) ρ φ ν

get-fn : elab-info → filepath
get-fn = ctxt.fn ∘' toplevel-state.Γ ∘' elab-info.τ

get-mn : elab-info → var
get-mn = ctxt.mn ∘' toplevel-state.Γ ∘' elab-info.τ

get-deps : elab-info → filepath → file → file
get-deps (mk-elab-info τ ρ φ ν) fp (Module mn ps es) =
  Module mn ps (foldr (λ x → CmdImport (Import ff x (renamectxt-rep (fst φ) x) nothing []) ::_) es (stringset-strings (trie-lookup-else empty-stringset ν fp)))

{-# TERMINATING #-}
elab-file : elab-info → filepath → elab-info × var
elab-cmds : elab-info → params → cmds → elab-info × cmds
elab-cmds ei ps [] = ei , []
elab-cmds ei@(mk-elab-info τ ρ φ ν) ps (CmdDefTerm x t :: csᵣ) =
  rename (get-mn ei # x) - x from ρ for λ x' ρ' →
  let t' = choose-mu (toplevel-state.Γ τ) ρ (params-to-lams ps t) in
  elim elab-cmds (mk-elab-info (ts-def τ x' (Ttm t')) ρ' φ ν) ps csᵣ for λ ei csᵣ →
  ei , CmdDefTerm x' t' :: csᵣ
elab-cmds ei@(mk-elab-info τ ρ φ ν) ps (CmdDefType x k T :: csᵣ) =
  rename (get-mn ei # x) - x from ρ for λ x' ρ' →
  let k' = choose-mu (toplevel-state.Γ τ) ρ (params-to-kind ps k)
      T' = choose-mu (toplevel-state.Γ τ) ρ (params-to-tplams ps T) in
  elim elab-cmds (mk-elab-info (ts-def τ x' (Ttp T')) ρ' φ ν) ps csᵣ for λ ei csᵣ →
  ei , CmdDefType x' k' T' :: csᵣ
elab-cmds ei ps (CmdDefKind x psₖ k :: csᵣ) =
  elab-cmds ei ps csᵣ
elab-cmds ei ps (CmdDefData es x psₓ k cs :: csᵣ) =
  elim elab-cmds ei [] (encoding-defs.ecs es) for λ ei ecs →
  elim elab-cmds ei [] (encoding-defs.gcs es) for λ ei gcs →
  elim elab-cmds ei ps csᵣ for λ ei rcs →
  ei , ecs ++ gcs ++ rcs
elab-cmds ei ps (CmdImport (Import p? fp mn' q? as) :: csᵣ) =
  let fpₒ = get-fn ei; mnₒ = get-mn ei in
  elim elab-file ei fp for λ ei mn'' →
  elab-cmds (add-dep (set-mn (set-fn ei fpₒ) mnₒ) fp) ps csᵣ

elab-file ei @ (mk-elab-info τ ρ φ ν) fp with trie-contains (snd φ) fp
...| tt = ei , renamectxt-rep (fst φ) fp
...| ff with get-include-elt-if τ fp >>= include-elt.ast~
...| nothing = ei , "error"
...| just (Module mn ps es) =
  let p = elab-cmds (record (set-mn (set-fn ei fp) mn) { ν = trie-insert (elab-info.ν ei) fp empty-trie }) ps es
      (mk-elab-info τ ρ φ ν) = fst p
      es' = snd p
      τ = record τ { Γ = record (toplevel-state.Γ τ) { ps = ps } } in
  rename fp - mn from fst φ for λ mn' φ' →
  mk-elab-info τ ρ (φ' , trie-insert (snd φ) fp (Module mn' ps es')) ν , mn'

elab-write-all : elab-info → (to : filepath) → IO ⊤
elab-write-all ei@(mk-elab-info τ ρ φ ν) to =
  let Γ = toplevel-state.Γ τ
      print = strRun Γ ∘ file-to-string in
  foldr'
    (createDirectoryIfMissing ff to)
    (uncurry λ fₒ fₛ io →
       let fₘ = renamectxt-rep (fst φ) fₒ
           fₙ = combineFileNames to (fₘ ^ ".cdle") in
       io >> writeRopeToFile fₙ (print (get-deps ei fₒ fₛ)))
    (trie-mappings (snd φ))

elab-all : toplevel-state → (from to : filepath) → IO ⊤
elab-all ts fm to =
  elab-write-all (fst (elab-file (new-elab-info ts) fm)) to >>
  putStrLn ("0")


text:
open import Nat
open import Prelude
open import List
open import core
open import judgemental-erase
open import checks

module constructability where
  -- we construct expressions and types by induction on their
  -- structure. for each sub term, we call the relevant theorem, then
  -- assemble the results with carefully chosen lists of actions that allow
  -- us to call the appropriate zipper lemmas and maintain well-typedness
  -- at every stage of the contruction.
  --
  -- the proof term at each stage except subsumption is, morally, just the
  -- mapping of the fragment of the action semantics used by the constructs
  -- in the list in the current formation context into the list monoid.

  -- construction of types
  construct-type : (t : τ̇) → Σ[ L ∈ List action ] runtype (▹ ⦇-⦈ ◃) L (▹ t ◃)
  construct-type num  = [ construct num ] , DoType TMConNum DoRefl
  construct-type ⦇-⦈ = [ del ]           , DoType TMDel DoRefl
  construct-type (t1 ==> t2) with construct-type t1 | construct-type t2
  ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct arrow :: l2 ++ [ move parent ] ,
                                 runtype++ ih1
                                   (DoType TMConArrow
                                     (runtype++ (ziplem-tmarr2 ih2)
                                       (DoType TMArrParent2 DoRefl)))

  mutual
    -- construction of expressions in synthetic positions
    construct-synth : {Γ : ·ctx} {t : τ̇} {e : ė} → (Γ ⊢ e => t) →
                                  Σ[ L ∈ List action ]
                                     runsynth Γ ▹ ⦇-⦈ ◃ ⦇-⦈ L ▹ e ◃ t
      -- the three base cases
    construct-synth (SVar x) = [ construct (var _) ]    , DoSynth (SAConVar x) DoRefl
    construct-synth SNum =     [ construct (numlit _) ] , DoSynth SAConNumlit DoRefl
    construct-synth SEHole =   [ del ]                  , DoSynth SADel DoRefl

      -- the inductive cases
    construct-synth {t = t} (SAsc x) with construct-type t | construct-ana x
    ... | (l1 , ih1) | (l2 , ih2) = construct asc :: (l1 ++ move parent :: move (child 1) :: (l2 ++ [ move parent ])) ,
                                    DoSynth SAConAsc
                                        (runsynth++ (ziplem-asc2 ETTop ETTop ih1)
                                         (DoSynth (SAMove EMAscParent2)
                                          (DoSynth (SAMove EMAscChild1)
                                           (runsynth++ (ziplem-asc1 ih2)
                                            (DoSynth (SAMove EMAscParent1) DoRefl)))))

    construct-synth (SAp e1 m e2) with construct-synth e1 | construct-ana e2
    ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct ap :: (l2 ++ [ move parent ]) ,
                                    runsynth++ ih1
                                        (DoSynth (SAConApArr m)
                                         (runsynth++ (ziplem-ap2 e1 m ih2)
                                          (DoSynth (SAMove EMApParent2) DoRefl)))

    construct-synth (SPlus e1 e2 ) with construct-ana e1 | construct-ana e2
    ... | (l1 , ih1) | (l2 , ih2) = construct plus :: (l2 ++ move parent :: move (child 1) :: (l1 ++ [ move parent ])) ,
                                    DoSynth (SAConPlus1 TCHole2)
                                        (runsynth++ (ziplem-plus2 ih2)
                                         (DoSynth (SAMove EMPlusParent2)
                                          (DoSynth (SAMove EMPlusChild1)
                                           (runsynth++ (ziplem-plus1 ih1)
                                            (DoSynth (SAMove EMPlusParent1) DoRefl)))))

    construct-synth (SNEHole wt) with construct-synth wt
    ... | (l , ih) = l ++ construct nehole :: move parent :: [] ,
                     runsynth++ ih
                         (DoSynth SAConNEHole (DoSynth (SAMove EMNEHoleParent) DoRefl))

    -- construction of expressions in analytic positions
    construct-ana : {Γ : ·ctx} {t : τ̇} {e : ė} → (Γ ⊢ e <= t) →
                                Σ[ L ∈ List action ]
                                   runana Γ ▹ ⦇-⦈ ◃ L ▹ e ◃ t
    construct-ana (ASubsume x c) with construct-synth x
    ... | (l , ih) = construct nehole :: l ++ (move parent :: finish :: []) ,
                     DoAna (AASubsume EETop SEHole SAConNEHole TCHole1)
                      (runana++  (ziplem-nehole-b SEHole c ih)
                        (DoAna (AAMove EMNEHoleParent)
                          (DoAna (AAFinish (ASubsume x c)) DoRefl)))

    construct-ana (ALam a m e) with construct-ana e
    ... | (l , ih) = construct (lam _) :: (l ++ [ move parent ]) ,
                     DoAna (AAConLam1 a m)
                         (runana++ (ziplem-lam a m ih)
                          (DoAna (AAMove EMLamParent) DoRefl))


text:
-- Andreas, 2015-05-02 Integrate copatterns with with.

{-# OPTIONS --copatterns #-}

open import Common.Prelude hiding (map)
open import Common.Product
open import Common.Equality

dup : {A : Set} → A → A × A
proj₁ (dup a) = a
proj₂ (dup a) with a
proj₂ (dup a) | x = x

record Stream (A : Set) : Set where
  coinductive
  constructor delay
  field
    force : A × Stream A
open Stream

map : ∀{A B} → (A → B) → Stream A → Stream B
force (map f s) with force s
... | a , as = f a , map f as

zipWith : ∀{A B C} → (A → B → C) → Stream A → Stream B → Stream C
force (zipWith f s t) with force s | force t
... | a , as | b , bs = f a b , zipWith f as bs

interleave : ∀{A} (s t : Stream A) → Stream A
force (interleave s t) with force s
... | a , as = a , interleave t as

mutual
  evens : ∀{A} (s : Stream A) → Stream A
  force (evens s) with force s
  ... | a , as = a , odds as

  odds : ∀{A} (s : Stream A) → Stream A
  odds s with force s
  ... | a , as = evens as

take : ∀{A} (n : Nat) (s : Stream A) → List A
take 0       s = []
take (suc n) s with force s
... | a , as = a ∷ take n as

record Bisim {A B} (R : A → B → Set) (s : Stream A) (t : Stream B) : Set where
  coinductive
  constructor ~delay
  field
    ~force : let a , as = force s
                 b , bs = force t
             in  R a b × Bisim R as bs
open Bisim

SEq : ∀{A} (s t : Stream A) → Set
SEq = Bisim (_≡_)

~refl : ∀{A} (s : Stream A) → SEq s s
~force (~refl s) with force s
... | a , as = refl , ~refl as

~sym : ∀{A}{s t : Stream A} → SEq s t → SEq t s
~force (~sym p) with ~force p
... | q , r = sym q , ~sym r

~sym' : ∀{A} {s t : Stream A} → SEq s t → SEq t s
~force (~sym' {s = s} {t} p) with force s | force t | ~force p
... | a , as | b , bs | r , q rewrite r = refl , ~sym' q

-- ~sym' : ∀{A} {s t : Stream A} → SEq s t → SEq t s
-- ~force (~sym' {s = s} {t} p) with force s | force t | ~force p
-- ... | x | y | q , r = {!x!} -- C-c C-c prints internal with-name

~trans : ∀{A}{r s t : Stream A} → SEq r s → SEq s t → SEq r t
~force (~trans p q) with ~force p | ~force q
... | ph , pt | qh , qt = trans ph qh , ~trans pt qt

~take : ∀{A} (s t : Stream A) (p : SEq s t) (n : Nat) → take n s ≡ take n t
~take s t p zero = refl
~take s t p (suc n) with force s | force t | ~force p
~take s t p (suc n) | a , as | .a , bs | refl , q rewrite ~take as bs q n = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.FinData.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat using (ℕ; zero; suc)
open import Cubical.Data.Bool.Base
open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    A B : Type ℓ

data Fin : ℕ → Type₀ where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

¬Fin0 : ¬ Fin 0
¬Fin0 ()

_==_ : ∀ {n} → Fin n → Fin n → Bool
zero == zero   = true
zero == suc _  = false
suc _ == zero  = false
suc m == suc n = m == n

predFin : {n : ℕ} → Fin (suc (suc n)) → Fin (suc n)
predFin zero = zero
predFin (suc x) = x

foldrFin : ∀ {n} → (A → B → B) → B → (Fin n → A) → B
foldrFin {n = zero}  _ b _ = b
foldrFin {n = suc n} f b l = f (l zero) (foldrFin f b (l ∘ suc))

elim
  : ∀(P : ∀{k} → Fin k → Type ℓ)
  → (∀{k} → P {suc k} zero)
  → (∀{k} → {fn : Fin k} → P fn → P (suc fn))
  → {k : ℕ} → (fn : Fin k) → P fn

elim P fz fs {zero} = ⊥.rec ∘ ¬Fin0
elim P fz fs {suc k} zero = fz
elim P fz fs {suc k} (suc fj) = fs (elim P fz fs fj)

rec : ∀{k} → (a0 aS : A) → Fin k → A
rec a0 aS zero = a0
rec a0 aS (suc x) = aS

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:
------------------------------------------------------------------------
-- Semi-heterogeneous vector equality
------------------------------------------------------------------------

module Data.Vec.Equality where

open import Data.Vec
open import Data.Nat using (suc)
open import Data.Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

module Equality (S : Setoid) where

  private
    open module SS = Setoid S
      using () renaming (_≈_ to _≊_; carrier to A)

  infix 4 _≈_

  data _≈_ : ∀ {n¹} → Vec A n¹ →
             ∀ {n²} → Vec A n² → Set where
    []-cong  : [] ≈ []
    _∷-cong_ : ∀ {x¹ n¹} {xs¹ : Vec A n¹}
                 {x² n²} {xs² : Vec A n²}
                 (x¹≈x² : x¹ ≊ x²) (xs¹≈xs² : xs¹ ≈ xs²) →
                 x¹ ∷ xs¹ ≈ x² ∷ xs²

  length-equal : ∀ {n¹} {xs¹ : Vec A n¹}
                   {n²} {xs² : Vec A n²} →
                 xs¹ ≈ xs² → n¹ ≡ n²
  length-equal []-cong        = PropEq.refl
  length-equal (_ ∷-cong eq₂) = PropEq.cong suc $ length-equal eq₂

  refl : ∀ {n} (xs : Vec A n) → xs ≈ xs
  refl []       = []-cong
  refl (x ∷ xs) = SS.refl ∷-cong refl xs

  sym : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
        xs ≈ ys → ys ≈ xs
  sym []-cong                = []-cong
  sym (x¹≡x² ∷-cong xs¹≈xs²) = SS.sym x¹≡x² ∷-cong sym xs¹≈xs²

  trans : ∀ {n m l} {xs : Vec A n} {ys : Vec A m} {zs : Vec A l} →
          xs ≈ ys → ys ≈ zs → xs ≈ zs
  trans []-cong            []-cong            = []-cong
  trans (x≈y ∷-cong xs≈ys) (y≈z ∷-cong ys≈zs) =
    SS.trans x≈y y≈z ∷-cong trans xs≈ys ys≈zs

  _++-cong_ : ∀ {n₁¹ n₂¹} {xs₁¹ : Vec A n₁¹} {xs₂¹ : Vec A n₂¹}
                {n₁² n₂²} {xs₁² : Vec A n₁²} {xs₂² : Vec A n₂²} →
              xs₁¹ ≈ xs₁² → xs₂¹ ≈ xs₂² →
              xs₁¹ ++ xs₂¹ ≈ xs₁² ++ xs₂²
  []-cong          ++-cong eq₃ = eq₃
  (eq₁ ∷-cong eq₂) ++-cong eq₃ = eq₁ ∷-cong (eq₂ ++-cong eq₃)

module DecidableEquality (D : DecSetoid) where

  private module DS = DecSetoid D
  open DS using () renaming (_≟_ to _≟′_ ; carrier to A)
  open Equality DS.setoid
  open import Relation.Nullary

  _≟_ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Dec (xs ≈ ys)
  _≟_ []       []       = yes []-cong
  _≟_ []       (y ∷ ys) = no (λ())
  _≟_ (x ∷ xs) []       = no (λ())
  _≟_ (x ∷ xs) (y ∷ ys) with xs ≟ ys | x ≟′ y
  ... | yes xs≈ys | yes x≊y = yes (x≊y ∷-cong xs≈ys)
  ... | no ¬xs≈ys | _       = no helper
    where
    helper : ¬ (x ∷ xs ≈ y ∷ ys)
    helper (_ ∷-cong xs≈ys) = ¬xs≈ys xs≈ys
  ... | _         | no ¬x≊y = no helper
    where
    helper : ¬ (x ∷ xs ≈ y ∷ ys)
    helper (x≊y ∷-cong _) = ¬x≊y x≊y

module HeterogeneousEquality {A : Set} where

  open import Relation.Binary.HeterogeneousEquality as HetEq
    using (_≅_)
  open Equality (PropEq.setoid A)

  to-≅ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
         xs ≈ ys → xs ≅ ys
  to-≅ []-cong                      = HetEq.refl
  to-≅ (PropEq.refl ∷-cong xs¹≈xs²) with length-equal xs¹≈xs²
  ... | PropEq.refl = HetEq.cong (_∷_ _) $ to-≅ xs¹≈xs²

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module test where

open import cry.gfp
open import cry.ec

{-
-- open import IO.Primitive
-- open import Foreign.Haskell

open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Char using (Char) renaming (primCharToNat to toNat)
open import Agda.Builtin.String using (String) renaming (primStringAppend to _++_; primStringToList to toList)
open import Agda.Builtin.Unit using (⊤)
-}

open import Data.Char using (Char; toNat)
open import Data.Nat as N using (ℕ; zero)
open import Data.Nat.Show using (show)
open import Data.List using (List; []; _∷_)
-- open import Data.Product using (_×_; _,_; proj₁)
open import Data.String using (String; _++_; toList)
open import Relation.Nullary using (yes; no)
open import IO using (IO; run; putStrLn)
open import Coinduction using (♯_)
open import Function using (_∘_; _$_)

-- open import Agda.Builtin.IO public using (IO)

_>>=_ : ∀ {a} {A B : Set a} → IO A → (A → IO B) → IO B
m >>= f = ♯ m IO.>>= λ a → ♯ f a

_>>_ : ∀ {a} {A B : Set a} → IO A → IO B → IO B
m >> n = ♯ m IO.>> ♯ n

open cry.ec using (module test-ec)
open test-ec

showElem : 𝔽 → String
showElem n = show n

read₁₀ : ℕ → List Char → ℕ × List Char
read₁₀ n [] = n , []
read₁₀ n (c ∷ cs) with toNat '0' N.≤? toNat c
... | no _ = n , cs
... | yes _ with toNat c N.≤? toNat '9'
... | no _ = n , cs
... | yes _ = read₁₀ (10 N.* n N.+ (toNat c N.∸ toNat '0')) cs

readsElem : List Char → 𝔽 × List Char
readsElem cs with read₁₀ 0 cs
... | n , cs′ = n , cs′ where

readElem : String → 𝔽
readElem = proj₁ ∘ readsElem ∘ toList

showPoint : Point → String
showPoint (x ∶ y ∶ z) = showElem x ++ ":" ++ showElem y ++ ":" ++ showElem z

readsPoint : List Char → Point × List Char
readsPoint s with readsElem s
... | x , s′ with readsElem s′
... | y , s″ with readsElem s″
... | z , s‴ = (x ∶ y ∶ z) , s‴ where

readPoint : String → Point
readPoint = proj₁ ∘ readsPoint ∘ toList

showPoint′ : Point → String
showPoint′ p = showPoint p ++ " = " ++ showPoint (aff p)

main′ : IO _
main′ = do
  let
    p = readPoint "4:2:1"
    2p = dbl p
    3p = add 2p p
    3p′ = add p 2p
    4p = dbl 2p
    4p′ = add p 3p
    4p″ = add p 3p′
    5p = add 4p p
    5p′ = add 2p 3p
    5p+0 = add 5p 𝕆
    6p = dbl 3p
    6p′ = add 5p p
    6p″ = add p 5p
  putStrLn ("p = " ++ showPoint′ p)
  putStrLn ("2p = " ++ showPoint′ 2p)
  putStrLn ("3p = " ++ showPoint′ 3p)
  putStrLn ("3p′ = " ++ showPoint′ 3p′)
  putStrLn ("4p = " ++ showPoint′ 4p)
  putStrLn ("4p′ = " ++ showPoint′ 4p′)
  putStrLn ("4p″ = " ++ showPoint′ 4p″)
  putStrLn ("5p = " ++ showPoint′ 5p)
  putStrLn ("5p′ = " ++ showPoint′ 5p′)
  putStrLn ("5p+0 = " ++ showPoint′ 5p+0)
  putStrLn ("6p = " ++ showPoint′ 6p)
  putStrLn ("6p′ = " ++ showPoint′ 6p′)
  putStrLn ("6p″ = " ++ showPoint′ 6p″)

main = run main′

max_stars_repo_name: semenov-vladyslav/cry-agda

max_issues_repo_name: semenov-vladyslav/cry-agda

max_forks_repo_name: semenov-vladyslav/cry-agda


text:
module GUIgeneric.GUIFeaturesPart2 where

open import GUIgeneric.Prelude renaming (addButton to addButton')

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.GUI.WxGraphicsLibLevel3 renaming (addButton to addButton')
open import GUIgeneric.GUIFeatures
open import GUIgeneric.GUIExample using (propOneBtn; propTwoBtn ; black ; oneColumnLayout)

open import Data.Product
open import Data.Fin

data ReturnTypeₛ  (S : Set) : Set where
    noChange      : ReturnTypeₛ S
    changedState  : (snew : S) →  ReturnTypeₛ S

-- handler GUI interface with separte state (i.e. state is a separte set instead of GUI)
-- We might later separte State into a gui state and property state i.e. have
--  GuiState : Set
--  AttrState : GuiState → Set
--  s2GUI : GuiState → GUI
--  s2prop : (g : GuiState)(prop : AttrState g) → properties (s2GUI g)

handlerGUIInterfₛ  : (S : Set) (s2GUI : (s : S) → Frame)
                     → Interfaceˢ
handlerGUIInterfₛ S s2GUI .Stateˢ                        = S
handlerGUIInterfₛ S s2GUI .Methodˢ  s                    = methodsG (s2GUI s)
handlerGUIInterfₛ S s2GUI .Resultˢ  s m                  = ReturnTypeₛ S
handlerGUIInterfₛ S s2GUI .nextˢ s m noChange            = s
handlerGUIInterfₛ S s2GUI .nextˢ s m (changedState snew) = snew

handlerGUIObjectₛ : (i : Size)(S : Set) (s2GUI : (s : S) → Frame)(s : S) → Set
handlerGUIObjectₛ i S s2GUI s = IOObjectˢ- GuiLev1Interface (handlerGUIInterfₛ S s2GUI) i s

mutual
  hGuiObjₛ2ord : (i : Size)(S : Set)
                 (s2GUI : (s : S) → Frame)
                 (s2prop : (s : S) → properties (s2GUI s))
                 (obj :  (s : S) → handlerGUIObjectₛ i S s2GUI s)
                 (s : S)
                 → HandlerObject i (s2GUI s)
  method (hGuiObjₛ2ord i S s2GUI s2prop obj s) {j} m =
        hGuiObjₛ2ordaux ∞  j  S s2GUI s s2prop obj m (method (obj s) m )

  hGuiObjₛ2ordaux' : (j : Size)(j' : Size)(S : Set)
                  (s2GUI : (s : S) → Frame)(s : S)
                  (s2prop : (s : S) → properties (s2GUI s))
                  (obj :  (s : S) → handlerGUIObjectₛ j' S s2GUI s)
                  (m   : methodsG (s2GUI s))
                  (prog : IO' GuiLev1Interface j
                            (ReturnTypeₛ S))
                  → IO' GuiLev1Interface j
                         ( Σ[ r ∈ returnType (s2GUI s) ]
                            (IOObjectˢ GuiLev1Interface handlerInterface j'
                             (nextˢ handlerInterface (s2GUI s) m r)))
  hGuiObjₛ2ordaux' j j' S s2GUI s s2prop obj m (do' c f) = do' c (λ r → hGuiObjₛ2ordaux j j' S s2GUI s s2prop obj m  (f r) )
  hGuiObjₛ2ordaux' j j' S s2GUI s s2prop obj m (return' noChange ) = return' (noChange , hGuiObjₛ2ord j' S s2GUI s2prop obj s {-obj'-})
  hGuiObjₛ2ordaux' j j' S s2GUI s s2prop obj m (return' (changedState snew)) = return' (changedGUI (s2GUI snew) (s2prop snew) , hGuiObjₛ2ord j' S s2GUI s2prop obj snew {- obj'-})

  hGuiObjₛ2ordaux : (j : Size)(j' : Size)(S : Set)
                  (s2GUI : (s : S) → Frame)(s : S)
                  (s2prop : (s : S) → properties (s2GUI s))
                  (obj :  (s : S) → handlerGUIObjectₛ j' S s2GUI s)
                  (m   : methodsG (s2GUI s))
                  (prog : IO GuiLev1Interface j
                            (ReturnTypeₛ S))
                  → IO GuiLev1Interface j
                         ( Σ[ r ∈  returnType (s2GUI s) ]
                            (IOObjectˢ GuiLev1Interface handlerInterface j'
                             (nextˢ handlerInterface (s2GUI s) m r)))
  force (hGuiObjₛ2ordaux j j' S s2GUI s s2prop obj m pr) {j''} = hGuiObjₛ2ordaux' j'' j' S s2GUI s s2prop obj m (force pr)

{-   *** STATE MACHINES  **** -}

sMachineHdl : (S : Set)(s : S) (f  : Frame) → Set
sMachineHdl S s f =  (m : methodsG f)
              → IO GuiLev1Interface ∞ (ReturnTypeₛ S)

record SMachineState (S : Set)(s : S) : Set where
  field
    fSM     : Frame
    propSM  : properties fSM
    handlSM : sMachineHdl S s fSM

SMachine : Set → Set
SMachine S = (s : S) → SMachineState S s

open SMachineState public

SMachine2HandlerGuiObjectₛ : (S : Set)
                             (sm : SMachine S)
                             (s : S)
                             → handlerGUIObjectₛ ∞ S (λ s → sm s .fSM) s
method (SMachine2HandlerGuiObjectₛ S sm s) = sm s .handlSM

stateMachine2Obj : (S : Set)
                   (sm : SMachine S)
                   (s : S)
                   → HandlerObject ∞ (sm s .fSM)
stateMachine2Obj S sm = hGuiObjₛ2ord ∞ S
                        (λ s → sm s .fSM)
                        (λ s → sm s .propSM)
                        (λ s → SMachine2HandlerGuiObjectₛ S sm s)

stateMachine2GUI : (S : Set) (sm : SMachine S) (s : S) → GUI
stateMachine2GUI S sm s .defFrame = sm s .fSM
stateMachine2GUI S sm s .property = sm s .propSM
stateMachine2GUI S sm s .obj = stateMachine2Obj S sm s

compileSMachine :  {S : Set} (sm : SMachine S) (s : S)
                   → NativeIO Unit
compileSMachine {S} sm s =
         compileGUI (stateMachine2GUI S sm s)

{-  **************** FEATURE MACHINE **** -}

-- an example of a feature machine wihout additional states:

record FeatureVMVers1 : Set₁ where
  field
    Features  : Set
    State     : Set
    GUIF      : (f : Features) → SMachine State

record FMachine (BaseSt : Set) : Set₁ where
  field
     Features : Set
     AddStateF : Set
     GUIF      : (f : Features) → SMachine (BaseSt ⊎ AddStateF)
  State : Set
  State =  BaseSt ⊎ AddStateF

open FMachine public

featureVMFull2GUI : (BaseSt : Set)
                        (vm : FMachine BaseSt)
                        (f : vm .Features)
                        (s : State vm)
                        → GUI
featureVMFull2GUI BaseSt vm f s =
         stateMachine2GUI
              (BaseSt ⊎ vm .AddStateF)
              (vm .GUIF f)  s

featureVMFull2IOˢprog : {BaseSt : Set}
                        (vm : FMachine BaseSt)
                        (f : vm .Features)
                        (s : State vm) → IOˢ GuiLev3Interface ∞ (λ _ → Unit) []
featureVMFull2IOˢprog {BaseSt} vm f s = guiFull2IOˢprog (featureVMFull2GUI BaseSt vm f s)

compileFeatureVM : {BaseSt : Set}
                   (vm : FMachine BaseSt)
                   (f : vm .Features)
                   (s : State vm)
                    → NativeIO Unit
compileFeatureVM {BaseSt} vm f s = compileGUI (featureVMFull2GUI BaseSt vm f s)

{- methodsREduce creates from a method for the frame (addButon s g)
    a method for g -}

mutual
  methodsReduce : (g : Frame)(str : String)(m : MethodsStruct)
                  (u : methodsStruct2Method (addButton str g notOptimzed) m)
                  → methodsStruct2Method g m
  methodsReduce g str (fficom) (ffibtn , gcomp) = gcomp
  methodsReduce g str (⊥^) ()
  methodsReduce g str (m ⊎^unoptimized m₁) (inj₁ x) = inj₁ (methodsReduce g str m x)
  methodsReduce g str (m ⊎^unoptimized m₁) (inj₂ y) = inj₂ (methodsReduce g str m₁ y)
  methodsReduce g str (m ⊎^ m₁) x = methodsReduceaux g str m m₁
                                      (methodsUnivIsEmpty m)
                                      (methodsUnivIsEmpty m₁) x

  methodsReduceaux : (g : Frame)(str : String)(m : MethodsStruct)
                     (m₁ : MethodsStruct)
                     (s  : SemiDec (λ g' → methodsStruct2Method g'  m))
                     (s₁  : SemiDec (λ g' → methodsStruct2Method g' m₁))
                     (u : methodsStruct2Methodaux
                          (addButton str g notOptimzed) m m₁ s s₁)
                     → methodsStruct2Methodaux g  m m₁ s s₁
  methodsReduceaux g str m m₁ s (isEmpty s₁) u = methodsReduce g str m u
  methodsReduceaux g str m m₁ (isEmpty x) posNonEmpty u = methodsReduce g str m₁ u
  methodsReduceaux g str m m₁ posNonEmpty posNonEmpty (inj₁ x) = inj₁ (methodsReduce g str m x)
  methodsReduceaux g str m m₁ posNonEmpty posNonEmpty (inj₂ y) = inj₂ (methodsReduce g str m₁ y)

subMethodToFullMethod : (btnStr : String)
                        (fr     : Frame)
                        (m      : methodsStruct2Method (addButton btnStr fr notOptimzed)
                                   (methodStruct fr ))
                        → methodsG fr
subMethodToFullMethod btnStr fr m = methodsReduce fr btnStr (methodStruct fr ) m

simpleAttr1Btn : (btnStr : String) → properties (addButton btnStr create-frame notOptimzed)
simpleAttr1Btn btnStr = black , oneColumnLayout

simpleSMState : {S : Set}
                (btnStr : String)
                {start : S}
                (end : S)
                → SMachineState S start
simpleSMState btnStr end .fSM = addButton btnStr create-frame notOptimzed
simpleSMState btnStr end .propSM = simpleAttr1Btn btnStr
simpleSMState btnStr end .handlSM m .force  = return' (changedState end)

baseF : FMachine StateV
baseF .Features = ⊤
baseF .AddStateF = ⊥
baseF .GUIF f (inj₁ s0) = simpleSMState "1Euro" (inj₁ s1)
baseF .GUIF f (inj₁ s1) = simpleSMState "Get Change" (inj₁ s2)
baseF .GUIF f (inj₁ s2) = simpleSMState "Soda" (inj₁ s0)
baseF .GUIF f (inj₂ ())

addBtn2StateMachine : {S : Set}{s : S}(sm : SMachineState S s)
                      (btnStr : String)(end : S)
                      → SMachineState S s
addBtn2StateMachine sm btnStr end .fSM = addButton btnStr (sm .fSM) notOptimzed
addBtn2StateMachine sm btnStr end .propSM = black , sm .propSM
addBtn2StateMachine sm btnStr end .handlSM (inj₁ x) .force = return' (changedState end)
addBtn2StateMachine sm btnStr end .handlSM (inj₂ m) =
      sm .handlSM (subMethodToFullMethod btnStr (sm .fSM) m)

simpleCancel : FMachine StateV → FMachine StateV
simpleCancel vm .Features = vm .Features × FeatureCancel
simpleCancel vm .AddStateF  = vm .AddStateF
simpleCancel vm .GUIF (f , yesCancel) (inj₁ s1) =
          addBtn2StateMachine  (vm .GUIF f (inj₁ s1)) "Cancel"  (inj₁ s0)

simpleCancel vm .GUIF (f , _) s = vm .GUIF f s

simpleCancelBase : FMachine StateV
simpleCancelBase = simpleCancel baseF

main1 : NativeIO Unit
main1 = compileFeatureVM baseF _ (inj₁ s0) --

main : NativeIO Unit
main = compileFeatureVM simpleCancelBase (_ , yesCancel) (inj₁ s0) --

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

record Eta : Set where
  constructor _,_
  field fst : Nat
        snd : Nat

open Eta

data ⊥ : Set where

hard-fail : (a : Eta) (x : Nat) → (fst a , x) ≡ a → ⊥
hard-fail a x ()  -- Should be error (refl is valid)

loop : ⊥
loop = hard-fail (0 , 0) 0 refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Builtin.Bool
open import Data.Maybe.Base using (just; nothing)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Integer.Base
open import Data.Integer.Properties using (+-*-commutativeRing)

open import Tactic.RingSolver.Core.AlmostCommutativeRing using (fromCommutativeRing)
open import Tactic.RingSolver.NonReflective (fromCommutativeRing +-*-commutativeRing λ { +0 -> just refl; _ -> nothing}) public

max_stars_repo_name: z-murray/AnalysisAgda

max_issues_repo_name: z-murray/AnalysisAgda

max_forks_repo_name: z-murray/AnalysisAgda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Fibration where

open import Level hiding (lift)
open import Data.Product

open import Categories.Category
open import Categories.Functor hiding (_∘_; _≡_)
open import Categories.Morphism.Cartesian
import Categories.Morphisms as Morphisms

record CartesianLifting {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} {E : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁}
                        (p : Functor E B) {a e} (f : B [ a , Functor.F₀ p e ]) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁) where
  private module E = Category E
  private module B = Category B
  open B using (_∘_; _≡_)

  open Functor p renaming (F₀ to p₀; F₁ to p₁)
  open Morphisms B

  field
    e′ : E.Obj

    φ : E [ e′ , e ]
    proof : ∃ \ (h : a ≅ p₀ e′) → f ∘ _≅_.g h ≡ p₁ φ
    φ-cartesian : Cartesian p φ

record Fibration {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} (E : Category o₀ ℓ₀ e₀) (B : Category o₁ ℓ₁ e₁) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁) where
  private module E = Category E
  private module B = Category B
  open B using (_∘_; _≡_)

  field
    p : Functor E B

  open Functor p renaming (F₀ to p₀; F₁ to p₁)

  open Morphisms B

  field
    lift : ∀ {a} e → (f : B [ a  , p₀ e ]) → CartesianLifting p f

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a preorder
------------------------------------------------------------------------

-- Example uses:
--
--    u∼y : u ∼ y
--    u∼y = begin
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  ∼⟨ w∼y ⟩
--      y  ≈⟨ z≈y ⟩
--      z  ∎
--
--    u≈w : u ≈ w
--    u≈w = begin-equality
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  ≡˘⟨ x≡w ⟩
--      x  ∎

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

open import Relation.Binary

module Relation.Binary.Reasoning.Preorder
  {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

open Preorder P

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Relation.Binary.Reasoning.Base.Double isPreorder public

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

infixr 2 _≈⟨⟩_

_≈⟨⟩_ = _≡⟨⟩_
{-# WARNING_ON_USAGE _≈⟨⟩_
"Warning: _≈⟨⟩_ was deprecated in v1.0.
Please use _≡⟨⟩_ instead."
#-}


text:
{-# OPTIONS --rewriting -v rewriting:80 #-}

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

postulate
  A : Set
  f : A → A
  h : .A → A → A
  rew : ∀ {x} → h x x ≡ x

{-# REWRITE rew #-}

test2 : (x y : A) → h x y ≡ y
test2 x y = refl

postulate
  r : .A → A
  s : .A → A
  rewr : ∀ x → r x ≡ s x
{-# REWRITE rewr #-}


text:
module PrettyPrinter where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Int using (pos)
open import Agda.Builtin.Unit using (⊤)

open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
open import FFI.Data.Aeson using (Value; eitherDecode)
open import FFI.Data.Either using (Left; Right)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Text.Encoding using (encodeUtf8)
open import FFI.System.Exit using (exitWith; ExitFailure)

open import Luau.Syntax using (Block)
open import Luau.Syntax.FromJSON using (blockFromJSON)
open import Luau.Syntax.ToString using (blockToString)

runBlock : ∀ {a} → Block a → IO ⊤
runBlock block = putStrLn (blockToString block)

runJSON : Value → IO ⊤
runJSON value with blockFromJSON(value)
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Right block) = runBlock block

runString : String → IO ⊤
runString txt with eitherDecode (encodeUtf8 txt)
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Right value) = runJSON value

main : IO ⊤
main = getContents >>= runString


text:
{-# OPTIONS --without-K #-}
module hott.core.equality where

open import hott.core.universe

-- | The equality type. In hott we think of the equality type as paths
-- between two points in the space A. To simplify the types we first
-- fix the common parameters.

module common {a : Level}{A : Type a} where

  data _≡_ (x : A) : (y : A) → Type a where
    refl : x ≡ x

  -- Induction principle for ≡ type.
  induction≡ : {ℓ : Level}
             → (D : {x y : A} (p : x ≡ y) → Type ℓ)
             → (d : {x : A} → D {x} {x} refl)
             → {x y : A} → (p : x ≡ y) → D p
  induction≡ D d refl = d

  -- In hott view point, this function takes the inverse of the path
  -- from x to y. As a relation you are proving that ≡ is symmetric.
  _⁻¹ : ∀{x y}
      → x ≡ y → y ≡ x
  refl ⁻¹ = refl

  -- The path composition. This means transitivity of the ≡ relation.
  _∙_ : ∀ {x y z}
      → x ≡ y → y ≡ z → x ≡ z
  refl ∙ refl = refl

  infixr 1 _≡_

  -- Precedence of multiplication
  infixl 70 _∙_

  -- Precedence of exponentiation.
  infixl 90 _⁻¹
  -- Equational reasoning
  -- To prove x_0 = x_n by a sequence of proofs
  -- x_0 = x_1
  -- x_1 = x_2
  -- ... you can use the following syntax
  --
  -- begin x_0 ≅ x_1 by p1
  --           ≅ x_2 by p2
  --       ....
  --           ≅ x_n by pn
  -- ∎
  --

  -- In equational proofs, it is more readable to use by definition
  -- than by refl
  definition : ∀{x} → x ≡ x
  definition = refl

  begin_ : (x : A)
         → x ≡ x
  begin_ x = refl

  _≡_by_ : ∀ {x y : A}
         → x ≡ y
         → (z : A)
         → y ≡ z
         → x ≡ z
  p ≡ z by q = p ∙ q

  _∎ : ∀{x y : A}
     → (x ≡ y)
     → (x ≡ y)
  proof ∎ = proof

  infixl 2 begin_
  infixl 1 _≡_by_
  infixl 0 _∎

  -- We now capture path transportation in the following submodule.
  module Transport {ℓ : Level} where
    -- Path transportation.
    transport : ∀ {x y : A}
              → x ≡ y
              → {P : A → Type ℓ}
              → P x → P y
    transport refl = λ z → z

    -- Another symbol for transport. Use it when you do not want to
    -- specify P.
    _⋆ : {P : A → Type ℓ}
     → {x y : A}
     → x ≡ y
     → P x → P y
    p ⋆ = transport p

  open Transport public

open common public

{-# BUILTIN EQUALITY _≡_     #-}
{-# BUILTIN REFL     refl    #-}

-- The functional congruence, i.e. likes gives likes on application of
-- a function. In the HoTT perspective this says that functions are
-- functors.
ap : ∀ {a b : Level} {A : Type a}{B : Type b} {x y : A}
     → (f : A → B)
     → x ≡ y → (f x) ≡ (f y)
ap f refl = refl

-- The dependent version of ap. This requires transport for its
-- definition.
apd : ∀{a b : Level }{A : Type a}{B : A → Type b}
    → (f : (a : A) → B a)
    → {x y : A}
    → (p : x ≡ y)
    → (p ⋆) (f x) ≡ f y
apd f refl = refl

-- Better syntax fro ap in equational reasoning.
applying_on_ : ∀{ℓ₀ ℓ₁}{A : Type ℓ₀}{B : Type ℓ₁}
             → (f : A → B)
             → {x y : A}
             → (p : x ≡ y)
             → f x ≡ f y
applying_on_ f a = ap f a

-- Better syntax for dependent version of applying on both sides.
transporting_over_ : ∀{ℓ₀ ℓ₁}{A : Type ℓ₀}{B : A → Type ℓ₁}
                   → (f : (a : A) → B(a)){x y : A}
                   → (p : x ≡ y)
                   → (p ⋆) (f x) ≡ f y
transporting f over p = apd f p

infixr 2 applying_on_
infixr 2 transporting_over_

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Empty where

open import Cubical.Data.Empty.Base public

open import Cubical.Data.Empty.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

data D (A : Set) : Set → Set₁ where
  c₁ : {B : Set} → D A B
  c₂ : D A A

record P {A B : Set} (p : D A B) : Set₁ where
  constructor c
  field
    d : D A B

Q : {A B₁ B₂ C : Set} {x : D A (B₁ → C)} {y : D A B₂} →
    P x → P y → B₁ ≡ B₂ → Nat
Q (c c₁) _      refl = 0
Q _      (c c₁) refl = 1
Q _      _      _    = 2

module _ {A B C : Set} where

  checkQ₀ : {x : D A (B → C)} {y : D A B} (px : P x) (py : P y) →
              Q {x = x} {y = y} (c c₁) py refl ≡ 0
  checkQ₀ _ _ = refl

  checkQ₁ : {x : D (A → B) (A → B)} {y : D (A → B) A} (px : P x) (py : P y) →
              Q {x = x} {y = y} (c c₂) (c c₁) refl ≡ 1
  checkQ₁ _ _ = refl

  checkQ₂ : {x : D (A → B) (A → B)} {y : D (A → B) (A → B)} (px : P x) (py : P y) (eq : A ≡ (A → B)) →
              Q {x = x} {y = y} (c c₂) (c c₂) eq ≡ 2
  checkQ₂ _ _ _ = refl

R : {A B₁ B₂ C : Set} {x : D A (B₁ → C)} {y : D A B₂} →
    P x → P y → B₁ ≡ B₂ → Nat
R (c c₂) _      refl = 0
R _      (c c₂) refl = 1
R _      _      _    = 2

module _ {A B C : Set} where

  checkR₀ : ∀ {B C} {x : D (B → C) (B → C)} {y : D (B → C) B} (px : P x) (py : P y) →
             R {x = x} {y = y} (c c₂) py refl ≡ 0
  checkR₀ _ _ = refl

  checkR₁ : ∀ {A B} {x : D A (A → B)} {y : D A A} (px : P x) (py : P y) →
             R {x = x} {y = y} (c c₁) (c c₂) refl ≡ 1
  checkR₁ _ _ = refl

  checkR₂ : ∀ {A B C} {x : D A (B → C)} {y : D A B} (px : P x) (py : P y) →
             R {x = x} {y = y} (c c₁) (c c₁) refl ≡ 2
  checkR₂ _ _ = refl


text:
module List.Order.Simple.Properties  {A : Set}
                     (_≤_ : A → A → Set)
                     (trans≤ : {x y z : A} → x ≤ y → y ≤ z → x ≤ z) where

open import Data.List
open import List.Order.Simple _≤_
open import List.Sorted _≤_

lemma-≤-*≤ : {x y : A}{xs : List A} → xs *≤ y → y ≤ x → xs *≤ x
lemma-≤-*≤ lenx y≤x  = lenx
lemma-≤-*≤ (lecx z≤y zs≤y) y≤x = lecx (trans≤ z≤y y≤x) (lemma-≤-*≤ zs≤y y≤x)

lemma-++-*≤ : {x y : A}{xs ys : List A} → y ≤ x → xs *≤ y → ys *≤ x → (xs ++ (y ∷ ys)) *≤ x
lemma-++-*≤ y≤x lenx ys≤x = lecx y≤x ys≤x
lemma-++-*≤ y≤x (lecx z≤y zs≤y) ys≤x = lecx (trans≤ z≤y y≤x) (lemma-++-*≤ y≤x zs≤y ys≤x)

lemma-≤-≤* : {x y : A}{xs : List A} → x ≤ y → y ≤* xs → x ≤* xs
lemma-≤-≤* x≤y genx = genx
lemma-≤-≤* x≤y (gecx y≤z y≤zs) = gecx (trans≤ x≤y y≤z) (lemma-≤-≤* x≤y y≤zs)

lemma-≤*-++ : {x y : A}{xs ys : List A} → x ≤ y → x ≤* xs → y ≤* ys → x ≤* (xs ++ (y ∷ ys))
lemma-≤*-++ x≤y genx y≤ys = gecx x≤y (lemma-≤-≤* x≤y y≤ys)
lemma-≤*-++ x≤y (gecx x≤z x≤zs) y≤ys = gecx x≤z (lemma-≤*-++ x≤y x≤zs y≤ys)

lemma-sorted++ : {x : A}{xs ys : List A} → xs *≤ x → x ≤* ys → Sorted xs → Sorted ys → Sorted (xs ++ (x ∷ ys))
lemma-sorted++ {x = x} lenx genx _ _ = singls x
lemma-sorted++ lenx (gecx u≤y _) _ sys = conss u≤y sys
lemma-sorted++ (lecx x≤u xs≤*u) u*≤ys (singls x) sys = conss x≤u (lemma-sorted++ xs≤*u u*≤ys nils sys)
lemma-sorted++ (lecx x≤u xs≤*u) u*≤ys (conss x≤z sxs) sys = conss x≤z (lemma-sorted++ xs≤*u u*≤ys sxs sys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2020-03-21, issue #4456

{-# OPTIONS --safe #-}

postulate A : Set


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

open import Categories.Category

module Categories.Category.Instance.Simplex where

open import Level
open import Data.Product
open import Data.Fin
open import Data.Nat using (ℕ)
open import Function renaming (id to idF; _∘_ to _∙_)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

Δ : Category 0ℓ 0ℓ 0ℓ
Δ = record
  { Obj       = ℕ
  ; _⇒_       = λ m n → Σ (Fin m → Fin n) (λ f → _≤_ =[ f ]⇒ _≤_)
  ; _≈_       = λ { (f , mf) (g , mg) → ∀ x → f x ≡ g x }
  ; id        = idF , idF
  ; _∘_       = λ { (f , mf) (g , mg) → f ∙ g , mf ∙ mg }
  ; assoc     = λ _ → refl
  ; sym-assoc = λ _ → refl
  ; identityˡ = λ _ → refl
  ; identityʳ = λ _ → refl
  ; identity² = λ _ → refl
  ; equiv     = record
    { refl  = λ _ → refl
    ; sym   = λ eq x → sym (eq x)
    ; trans = λ eq₁ eq₂ x → trans (eq₁ x) (eq₂ x)
    }
  ; ∘-resp-≈  = λ {_ _ _ f g h i} eq₁ eq₂ x → trans (cong (λ t → proj₁ f t) (eq₂ x)) (eq₁ (proj₁ i x))
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
postulate
  admit : ∀ {i} {X : Set i} → X
  X Y Z : Set

data Id (z : Z) : Z → Set where
  refl : Id z z

record Square : Set₁ where
  field
    U : Set
    u : U
open Square

record RX : Set where
  field x : X
open RX

record R : Set where
  -- This definition isn't used; without it,
  -- the internal error disappears.
  r : Square
  r .U = admit
  r .u = admit

  module M (z₀ z₁ : Z) where
    f : Id z₀ z₁ → RX
    f refl = {!λ where .x → ?!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Nat

record Pointed (A : Set) : Set where
 field point : A

it : ∀ {A : Set} {{x : A}} → A
it {{x}} = x

instance _ = record { point = 3 - 4 }

_ : Pointed Nat
_ = {!!}