text:
module BTA6 where

----------------------------------------------
-- Preliminaries: Imports and List-utilities
----------------------------------------------

open import Data.Nat hiding (_<_)
open import Data.Bool
open import Function using (_∘_)
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Category.Functor

-- Pointer into a list. It is similar to list membership as defined in
-- Data.List.AnyMembership, rather than going through propositional
-- equality, it asserts the existence of the referenced element
-- directly.
module ListReference where
  infix 4 _∈_
  data _∈_ {A : Set} : A → List A → Set where
    hd : ∀ {x xs} → x ∈ (x ∷ xs)
    tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)
open ListReference

mapIdx : {A B : Set} → (f : A → B) →
         {x : A} {xs : List A} → x ∈ xs → f x ∈ map f xs
mapIdx f hd = hd
mapIdx f (tl x₁) = tl (mapIdx f x₁)

-- Extension of lists at the front and, as a generalization, extension
-- of lists somewhere in the middle.
module ListExtension where
  open import Relation.Binary.PropositionalEquality

  -- Extension of a list by consing elements at the front.
  data _↝_ {A : Set} : List A → List A → Set where
    ↝-refl   : ∀ {Γ}      → Γ ↝ Γ
    ↝-extend : ∀ {Γ Γ' τ} → Γ ↝ Γ' → Γ ↝ (τ ∷ Γ')

  -- Combining two transitive extensions.
  ↝-trans : ∀ {A : Set}{Γ Γ' Γ'' : List A} → Γ ↝ Γ' → Γ' ↝ Γ'' → Γ ↝ Γ''
  ↝-trans Γ↝Γ' ↝-refl = Γ↝Γ'
  ↝-trans Γ↝Γ' (↝-extend Γ'↝Γ'') = ↝-extend (↝-trans Γ↝Γ' Γ'↝Γ'')

  -- Of course, ↝-refl is the identity for combining two extensions.
  lem-↝-refl-id : ∀ {A : Set} {Γ Γ' : List A} →
                    (Γ↝Γ' : Γ ↝ Γ') →
                    Γ↝Γ' ≡ (↝-trans ↝-refl Γ↝Γ')
  lem-↝-refl-id ↝-refl = refl
  lem-↝-refl-id (↝-extend Γ↝Γ') =
    cong ↝-extend (lem-↝-refl-id Γ↝Γ')
  -- TODO: why does this work?
  -- lem-↝-refl-id (↝-extend Γ↝Γ') = lem-↝-refl-id (↝-extend Γ↝Γ')

  -- Extending a list in the middle:
  data _↝_↝_ {A : Set} : List A → List A → List A → Set where
    -- First prepend the extension list to the common suffix
    ↝↝-base   : ∀ {Γ Γ''} → Γ ↝ Γ'' → Γ ↝ [] ↝ Γ''
    -- ... and then add the common prefix
    ↝↝-extend : ∀ {Γ Γ' Γ'' τ} →
                 Γ ↝ Γ' ↝ Γ'' → (τ ∷ Γ) ↝ (τ ∷ Γ') ↝ (τ ∷ Γ'')
open ListExtension

---------------------------------------
-- Start of the development:
---------------------------------------

-- Intro/Objective:
-------------------
-- The following development defines a (verified) specializer/partial
-- evaluator for a simply typed lambda calculus embedded in Agda using
-- deBruijn indices.

-- The residual language.
-------------------------

-- The residual language is a standard simply typed λ-calculus.  The
-- types are integers and functions.
data Type : Set where
  Int : Type
  Fun : Type → Type → Type
Ctx = List Type

-- The type Exp describes the typed residual expressions. Variables
-- are represented by deBruijn indices that form references into the
-- typing context. The constructors and typing constraints are
-- standard.

-- TODO: citations for ``as usual'' and ``standard''
data Exp (Γ : Ctx) : Type → Set where
  EVar : ∀ {τ} → τ ∈ Γ → Exp Γ τ
  EInt : ℕ → Exp Γ Int
  EAdd : Exp Γ Int → Exp Γ Int -> Exp Γ Int
  ELam : ∀ {τ τ'} → Exp (τ ∷ Γ) τ' → Exp Γ (Fun τ τ')
  EApp : ∀ {τ τ'} → Exp Γ (Fun τ τ')  → Exp Γ τ → Exp Γ τ'

-- The standard functional semantics of the residual expressions.
-- TODO: citations for ``as usual'' and ``standard''
module Exp-Eval where
  -- interpretation of Exp types
  EImp : Type → Set
  EImp Int = ℕ
  EImp (Fun τ₁ τ₂) = EImp τ₁ → EImp τ₂

  -- Environments containing values for free variables. An environment
  -- is indexed by a typing context that provides the types for the
  -- contained values.
  data Env : Ctx → Set where
    [] : Env []
    _∷_ : ∀ {τ Γ} → EImp τ → Env Γ → Env (τ ∷ Γ)

  -- Lookup a value in the environment, given a reference into the
  -- associated typing context.
  lookupE : ∀ { τ Γ } → τ ∈ Γ → Env Γ → EImp τ
  lookupE hd (x ∷ env) = x
  lookupE (tl v) (x ∷ env) = lookupE v env

  -- Evaluation of residual terms, given a suitably typed environment.
  ev : ∀ {τ Γ} → Exp Γ τ → Env Γ → EImp τ
  ev (EVar x) env = lookupE x env
  ev (EInt x) env = x
  ev (EAdd e f) env = ev e env + ev f env
  ev (ELam e) env = λ x → ev e (x ∷ env)
  ev (EApp e f) env = ev e env (ev f env)

-- The binding-time-annotated language.
---------------------------------------

-- The type of a term determines the term's binding time. The type
-- constructors with an A-prefix denote statically bound integers and
-- functions. Terms with dynamic binding time have a `D' type. The `D'
-- type constructor simply wraps up a residual type.
data AType : Set where
    AInt  : AType
    AFun  : AType → AType → AType
    D     : Type → AType
ACtx = List AType

-- The mapping from annotated types to residual types is straightforward.
typeof : AType → Type
typeof AInt = Int
typeof (AFun α₁ α₂) = Fun (typeof α₁) (typeof α₂)
typeof (D x) = x

-- ATypes are stratified such that that dynamically bound
-- functions can only have dynamically bound parameters.

-- TODO: why exactly is that necessary?

-- The following well-formedness relation as an alternative representation
-- for this constraint:
module AType-WF where
  open import Relation.Binary.PropositionalEquality
  -- Static and dynamic binding times
  data BT : Set where
    stat : BT
    dyn : BT

  -- Ordering on binding times: dynamic binding time subsumes static
  -- binding time.
  data _≤-bt_ : BT → BT → Set where
    bt≤bt : ∀ bt → bt ≤-bt bt
    stat≤bt : ∀ bt → stat ≤-bt bt

  module WF (ATy : Set) (typeof : ATy → Type) (btof : ATy → BT) where
    data wf : ATy → Set where
      wf-int : ∀ α → typeof α ≡ Int → wf α
      wf-fun : ∀ α α₁ α₂ →
               typeof α ≡ Fun (typeof α₁) (typeof α₂) →
               btof α ≤-bt btof α₁ →
               btof α ≤-bt btof α₂ →
               wf α₁ → wf α₂ →
               wf α

  -- It is easy to check that the stratification respects the
  -- well-formedness, given the intended mapping from ATypes to
  -- binding times expained above:
  btof : AType → BT
  btof AInt = stat
  btof (AFun _ _) = stat
  btof (D x) = dyn

  open WF AType typeof btof using (wf-fun; wf-int) renaming (wf to wf-AType)
  lem-wf-AType : ∀ α → wf-AType α
  lem-wf-AType AInt = WF.wf-int AInt refl
  lem-wf-AType (AFun α α₁) = WF.wf-fun (AFun α α₁) α α₁ refl (stat≤bt (btof α))
                             (stat≤bt (btof α₁))
                             (lem-wf-AType α)
                             (lem-wf-AType α₁)
  lem-wf-AType (D Int) = WF.wf-int (D Int) refl
  lem-wf-AType (D (Fun x x₁)) = WF.wf-fun (D (Fun x x₁))
                                          (D x) (D x₁)
                                          refl (bt≤bt dyn) (bt≤bt dyn)
                                          (lem-wf-AType (D x))
                                          (lem-wf-AType (D x₁))

-- The typed annotated terms: The binding times of variables is
-- determined by the corresponding type-binding in the context. In the
-- other cases, the A- and D-prefixes on term constructors inidicate
-- the corresponding binding times for the resulting terms.
data AExp (Δ : ACtx) : AType → Set where
  Var : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : ℕ → AExp Δ AInt
  AAdd : AExp Δ AInt → AExp Δ AInt → AExp Δ AInt
  ALam : ∀ {α₁ α₂}   → AExp (α₁ ∷ Δ) α₂ → AExp Δ (AFun α₁ α₂)
  AApp : ∀ {α₁ α₂}   → AExp Δ (AFun α₂ α₁) → AExp Δ α₂ → AExp Δ α₁
  DInt : ℕ → AExp Δ (D Int)
  DAdd : AExp Δ (D Int) → AExp Δ (D Int) → AExp Δ (D Int)
  DLam : ∀ {σ₁ σ₂} → AExp ((D σ₁) ∷ Δ) (D σ₂) → AExp Δ (D (Fun σ₁ σ₂))
  DApp : ∀ {α₁ α₂} → AExp Δ (D (Fun α₂ α₁)) → AExp Δ (D α₂) → AExp Δ (D α₁)
  Lift : AExp Δ AInt → AExp Δ (D Int)

-- The terms of AExp assign a binding time to each subterm. For
-- program specialization, we interpret terms with dynamic binding
-- time as the programs subject to specialization, and their subterms
-- with static binding time as statically known inputs. A partial
-- evaluation function (or specializer) then compiles the program into
-- a residual term for that is specialized for the static inputs. The
-- main complication when defining partial evaluation as a total,
-- primitively recursive function will be the treatment of the De
-- Bruijn variables of non-closed residual expressions.

-- Before diving into the precise definition, it is instructive to
-- investigate the expected result of partial evaluation on some
-- examples.

module ApplicativeMaybe where
  open import Data.Maybe public
  open import Category.Functor public
  import Level
  open RawFunctor {Level.zero} functor public

  infixl 4 _⊛_
  _⊛_ : {A B : Set} → Maybe (A → B) → Maybe A → Maybe B
  just f ⊛ just x = just (f x)
  _ ⊛ _           = nothing

  liftA2 : {A B C : Set} → (A → B → C) → Maybe A → Maybe B → Maybe C
  liftA2 f mx my = just f ⊛ mx ⊛ my

module AExp-Examples where

  open import Data.Product hiding (map)
  open ApplicativeMaybe
  open import Data.Empty
  open Relation.Binary.PropositionalEquality

  -- (We pre-define some De Bruijn indices to improve
  -- readability of the examples:)
  x : ∀ {α Δ} → AExp (α ∷ Δ) α
  x = Var hd
  x' : ∀ {α Δ} → Exp (α ∷ Δ) α
  x' = EVar hd
  y : ∀ {α₁ α Δ} → AExp (α₁ ∷ α ∷ Δ) α
  y = Var (tl hd)
  z : ∀ {α₁ α₂ α Δ} → AExp (α₁ ∷ α₂ ∷ α ∷ Δ) α
  z = Var (tl (tl hd))

  -- A rather trivial case is the specialization of base-type
  -- calulations. Here, we simply want to emit the result of a static
  -- addition as a constant:

  -- Lift (5S +S 5S) --specializes to --> 5E
  ex0 : AExp [] (D Int)
  ex0 = (Lift (AAdd (AInt 5) (AInt 5)))

  ex0' : AExp [] (D Int)
  ex0' = DAdd (DInt 6) (Lift (AAdd (AInt 5) (AInt 5)))

  ex0-spec : Exp [] Int
  ex0-spec = (EInt 10)

  ex0'-spec : Exp [] Int
  ex0'-spec = (EAdd (EInt 6) (EInt 10))

  -- The partial evaluation for this case is of course
  -- straightforward. We use Agda's ℕ as an implementation type for
  -- static integers and residual expressions Exp for dynamic ones.
  Imp0 : AType → Set
  Imp0 AInt = ℕ
  Imp0 (D σ) = Exp [] σ
  Imp0 _ = ⊥

  pe-ex0 : ∀ { α } → AExp [] α → Maybe (Imp0 α)
  pe-ex0 (AInt x) = just (x)
  pe-ex0 (DInt x) = just (EInt x)
  pe-ex0 (AAdd e f) = liftA2 _+_  (pe-ex0 e) (pe-ex0 f)
  pe-ex0 (DAdd e f) = liftA2 EAdd (pe-ex0 e) (pe-ex0 f)
  pe-ex0 (Lift e) = EInt <$> (pe-ex0 e)
  pe-ex0 _ = nothing

  ex0-test : pe-ex0 ex0 ≡ just ex0-spec
  ex0-test = refl

  ex0'-test : pe-ex0 ex0' ≡ just ex0'-spec
  ex0'-test = refl

  -- Specializing open terms is also straightforward. This situation
  -- typically arises when specializing the body of a lambda
  -- abstraction.
  -- (Dλ x → x +D Lift (5S + 5S)) ---specializes to--> Eλ x → EInt 10
  ex1 : AExp [] (D (Fun Int Int))
  ex1 = (DLam (DAdd x (Lift (AAdd (AInt 5) (AInt 5)))))

  ex1-spec : Exp [] (Fun Int Int)
  ex1-spec = ELam (EAdd x' (EInt 10))

  ex1' : AExp (D Int ∷ []) (D Int)
  ex1' = (Lift (AAdd (AInt 5) (AInt 5)))

  ex1'-spec : Exp (Int ∷ []) Int
  ex1'-spec = (EAdd x' (EInt 10))

  -- The implementation type now also has to hold open residual terms,
  -- which arise as the result of partially evaluating an open term
  -- with with dynamic binding time. The calculation of the
  -- implementation type thus requires a typing context as a
  -- parameter.
  Imp1 : Ctx → AType → Set
  Imp1 _ AInt = ℕ
  Imp1 Γ (D τ) = Exp Γ τ
  Imp1 _ _ = ⊥

  erase = typeof

  -- Unsurprisingly, Partial evaluation of open terms emits
  -- implementations that are typed under the erased context.
  pe-ex1 : ∀ {α Δ} → AExp Δ α → Maybe (Imp1 (map erase Δ) α)
  pe-ex1 (AInt x) = just (x)
  pe-ex1 (DInt x) = just (EInt x)
  pe-ex1 (AAdd e f) = liftA2 _+_  (pe-ex1 e) (pe-ex1 f)
  pe-ex1 (DAdd e f) = liftA2 EAdd (pe-ex1 e) (pe-ex1 f)
  pe-ex1 (Lift e) = EInt <$> (pe-ex1 e)
  pe-ex1 (DLam {τ} e) = ELam  <$> pe-ex1 e
  -- Technical note: In the case for variables we can simply exploit
  -- the fact that variables are functorial in the actual type of
  -- their contexts' elements
  pe-ex1 (Var {D _} x) = just (EVar (mapIdx typeof x))
  pe-ex1 _ = nothing

  ex1-test : pe-ex1 ex1 ≡ just ex1-spec
  ex1-test = refl

  data Static : AType → Set where
    SInt : Static AInt
    SFun : ∀ { α₁ α₂ } → Static α₂ → Static (AFun α₁ α₂)

  is-static : (α : AType) → Dec (Static α)
  is-static α = {!!}

  Imp2 : Ctx → AType → Set
  Imp2 _ AInt = ℕ
  Imp2 Γ (D τ) = Exp Γ τ
  Imp2 Γ (AFun α₁ α₂) =   Imp2 Γ α₁ → Imp2 Γ α₂

-- The interpretation of annotated types.
Imp : Ctx → AType → Set
Imp Γ (AInt) = ℕ
Imp Γ (AFun α₁ α₂) = ∀ {Γ'} → Γ ↝ Γ' → (Imp Γ' α₁ → Imp Γ' α₂)
Imp Γ (D σ) = Exp Γ σ

elevate-var : ∀ {Γ Γ'} {τ : Type} → Γ ↝ Γ' → τ ∈ Γ → τ ∈ Γ'
elevate-var ↝-refl x = x
elevate-var (↝-extend Γ↝Γ') x = tl (elevate-var Γ↝Γ' x)

elevate-var2 : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → τ ∈ Γ → τ ∈ Γ''
elevate-var2 (↝↝-base x) x₁ = elevate-var x x₁
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') hd = hd
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') (tl x) = tl (elevate-var2 Γ↝Γ'↝Γ'' x)

elevate : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → Exp Γ τ → Exp Γ'' τ
elevate Γ↝Γ'↝Γ'' (EVar x) = EVar (elevate-var2 Γ↝Γ'↝Γ'' x)
elevate Γ↝Γ'↝Γ'' (EInt x) = EInt x
elevate Γ↝Γ'↝Γ'' (EAdd e e₁) = EAdd (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)
elevate Γ↝Γ'↝Γ'' (ELam e) = ELam (elevate (↝↝-extend Γ↝Γ'↝Γ'') e)
elevate Γ↝Γ'↝Γ'' (EApp e e₁) = EApp (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)

lift : ∀ {Γ Γ'} α → Γ ↝ Γ' → Imp Γ α → Imp Γ' α
lift AInt p v = v
lift (AFun x x₁) Γ↝Γ' v = λ Γ'↝Γ'' → v (↝-trans Γ↝Γ' Γ'↝Γ'')
lift (D x₁) Γ↝Γ' v = elevate (↝↝-base Γ↝Γ') v

module SimpleAEnv where
  -- A little weaker, but much simpler
  data AEnv (Γ : Ctx) : ACtx → Set where
    [] : AEnv Γ []
    cons : ∀ {Δ} (α : AType) → Imp Γ α → AEnv Γ Δ → AEnv Γ (α ∷ Δ)

  lookup : ∀ {α Δ Γ} → AEnv Γ Δ → α ∈ Δ → Imp Γ α
  lookup (cons α v env) hd =  v
  lookup (cons α₁ v env) (tl x) = lookup env x

  liftEnv : ∀ {Γ Γ' Δ} → Γ ↝ Γ' → AEnv Γ Δ → AEnv Γ' Δ
  liftEnv Γ↝Γ' [] = []
  liftEnv Γ↝Γ' (cons α x env) = cons α (lift α Γ↝Γ' x) (liftEnv Γ↝Γ' env)

  consD : ∀ {Γ Δ} σ → AEnv Γ Δ → AEnv (σ ∷ Γ) (D σ ∷ Δ)
  consD σ env = (cons (D σ) (EVar hd) (liftEnv (↝-extend {τ = σ} ↝-refl) env))

  pe : ∀ {α Δ Γ} → AExp Δ α → AEnv Γ Δ → Imp Γ α
  pe (Var x) env = lookup env x
  pe (AInt x) env = x
  pe (AAdd e₁ e₂) env = pe e₁ env + pe e₂ env
  pe (ALam {α} e) env = λ Γ↝Γ' → λ y → pe e (cons α y (liftEnv Γ↝Γ' env))
  pe (AApp e₁ e₂) env = ((pe e₁ env) ↝-refl) (pe e₂ env)
  pe (DInt x) env = EInt x
  pe (DAdd e e₁) env = EAdd (pe e env) (pe e₁ env)
  pe (DLam {σ} e) env = ELam (pe e (consD σ env))
  pe (DApp e e₁) env = EApp (pe e env) (pe e₁ env)
  pe (Lift e) env = EInt (pe e env)

module CheckExamples where
  open import Relation.Binary.PropositionalEquality hiding ([_])
  open SimpleAEnv
  open AExp-Examples

  check-ex1 : pe ex1 [] ≡ ex1-spec
  check-ex1 = refl

  check-ex0 : pe ex0 [] ≡ ex0-spec
  check-ex0 = refl

  check-ex0' : pe ex0' [] ≡ ex0'-spec
  check-ex0' = refl
module Examples where
  open SimpleAEnv
  open import Relation.Binary.PropositionalEquality

  x : ∀ {α Δ} → AExp (α ∷ Δ) α
  x = Var hd
  y : ∀ {α₁ α Δ} → AExp (α₁ ∷ α ∷ Δ) α
  y = Var (tl hd)
  z : ∀ {α₁ α₂ α Δ} → AExp (α₁ ∷ α₂ ∷ α ∷ Δ) α
  z = Var (tl (tl hd))

-- Dλ y → let f = λ x → x D+ y in Dλ z → f z
  term1 : AExp [] (D (Fun Int (Fun Int Int)))
  term1 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DAdd x y))))

-- Dλ y → let f = λ x → (Dλ w → x D+ y) in Dλ z → f z
-- Dλ y → (λ f → Dλ z → f z) (λ x → (Dλ w → x D+ y))
  term2 : AExp [] (D (Fun Int (Fun Int Int)))
  term2 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DLam {σ₁ = Int} (DAdd y z)))))

  -- closed pe. In contrast to BTA5, it is now not clear what Γ is
  -- given an expression. So perhaps AEnv has it's merrits after all?
  pe[] : ∀ {α} → AExp [] α → Imp [] α
  pe[] e = pe e []

  ex-pe-term1 : pe[] term1 ≡ ELam (ELam (EVar hd))
  ex-pe-term1 = refl

  ex-pe-term2 : pe[] term2 ≡ ELam (ELam (EVar hd))
  ex-pe-term2 = refl

module Correctness where
  open SimpleAEnv
  open Exp-Eval

  -- TODO: rename occurences of stripα to typeof
  stripα = typeof

  stripΔ : ACtx → Ctx
  stripΔ = map stripα

  strip-lookup : ∀ { α Δ} → α ∈ Δ → stripα α ∈ stripΔ Δ
  strip-lookup hd = hd
  strip-lookup (tl x) = tl (strip-lookup x)

  strip : ∀ {α Δ} → AExp Δ α → Exp (stripΔ Δ) (stripα α)
  strip (Var x) = EVar (strip-lookup x)
  strip (AInt x) = EInt x
  strip (AAdd e f) = EAdd (strip e) (strip f)
  strip (ALam e) = ELam (strip e)
  strip (AApp e f) = EApp (strip e) (strip f)
  strip (DInt x) = EInt x
  strip (DAdd e f) = EAdd (strip e) (strip f)
  strip (DLam e) = ELam (strip e)
  strip (DApp e f) = EApp (strip e) (strip f)
  strip (Lift e) = strip e

  liftE : ∀ {τ Γ Γ'} → Γ ↝ Γ' → Exp Γ τ → Exp Γ' τ
  liftE Γ↝Γ' e = elevate (↝↝-base Γ↝Γ') e

  stripLift : ∀ {α Δ Γ} → stripΔ Δ ↝ Γ → AExp Δ α  → Exp Γ (stripα α)
  stripLift Δ↝Γ = liftE Δ↝Γ ∘ strip

  -- We want to show that pe preserves the semantics of the
  -- program. Roughly, Exp-Eval.ev-ing a stripped program is
  -- equivalent to first pe-ing a program and then Exp-Eval.ev-ing the
  -- result. But as the pe-result of a static function ``can do more''
  -- than the (ev ∘ strip)ped function we need somthing more refined.

  module Equiv where
    open import Relation.Binary.PropositionalEquality

    -- Extending a value environment according to an extension of a
    -- type environment
    data _⊢_↝_ {Γ} : ∀ {Γ'} → Γ ↝ Γ' → Env Γ → Env Γ' → Set where
      refl : ∀ env → ↝-refl ⊢ env ↝ env
      extend : ∀ {τ Γ' env env'} →  {Γ↝Γ' : Γ ↝ Γ'} →
                 (v : EImp τ) → (Γ↝Γ' ⊢  env ↝ env')  →
                 ↝-extend Γ↝Γ' ⊢ env ↝ (v ∷ env')

    env↝trans : ∀ {Γ Γ' Γ''} {Γ↝Γ' : Γ ↝ Γ'} {Γ'↝Γ'' : Γ' ↝ Γ''}
                  {env env' env''} →
                  Γ↝Γ' ⊢ env ↝ env' →
                  Γ'↝Γ'' ⊢ env' ↝ env'' →
                  let Γ↝Γ'' = ↝-trans Γ↝Γ' Γ'↝Γ'' in
                  Γ↝Γ'' ⊢ env ↝ env''
    -- env↝trans {Γ} {.Γ''} {Γ''} {Γ↝Γ'} {.↝-refl} {env} {.env''} {env''} env↝env' (refl .env'') = env↝env'
    -- env↝trans env↝env' (extend v env'↝env'') = extend v (env↝trans env↝env' env'↝env'')

    -- TODO: why does this work???
    env↝trans {.Γ'} {Γ'} {Γ''} {.↝-refl} {Γ'↝Γ''} {.env'} {env'} (refl .env') env'↝env''
      rewrite sym (lem-↝-refl-id  Γ'↝Γ'') = env'↝env''
    env↝trans (extend v env↝env') env'↝env'' = env↝trans (extend v env↝env') env'↝env''

    -- Equivalent Imp Γ α and EImp τ values (where τ = stripα α). As
    -- (v : Imp Γ α) is not necessarily closed, equivalence is defined for
    -- the closure (Env Γ, ImpΓ α)
    Equiv : ∀ {α Γ} → Env Γ → Imp Γ α → EImp (stripα α) → Set
    Equiv {AInt} env av v = av ≡ v
    Equiv {AFun α₁ α₂} {Γ} env af f = -- extensional equality, given -- an extended context
        ∀ {Γ' env' Γ↝Γ'} → (Γ↝Γ' ⊢ env ↝ env') →
        {ax : Imp Γ' α₁} → {x : EImp (stripα α₁)} →
        Equiv env' ax x → Equiv env' (af Γ↝Γ' ax) (f x)
    Equiv {D x} {Γ} env av v = ev av env ≡ v -- actually we mean extensional equality

    -- Equivalence of AEnv and Env environments. They need to provide
    -- Equivalent bindings for a context Δ/stripΔ Δ. Again, the
    -- equivalence is defined for a closure (Env Γ', AEnv Γ' Δ).
    data Equiv-Env {Γ' : _} (env' : Env Γ') :
      ∀ {Δ} → let Γ = stripΔ Δ in
      AEnv Γ' Δ → Env Γ → Set where
      [] : Equiv-Env env' [] []
      cons : ∀ {α Δ} → let τ = stripα α
                           Γ = stripΔ Δ in
              {env : Env Γ} → {aenv : AEnv Γ' Δ} →
              Equiv-Env env' aenv env →
              (va : Imp (Γ') α) → (v : EImp τ) →
              Equiv env' va v →
              Equiv-Env env' (cons α va (aenv)) (v ∷ env)

  -- Now for the proof...
  module Proof where
    open Equiv
    open import Relation.Binary.PropositionalEquality

    -- Extensional equality as an axiom to prove the Equivalence of
    -- function values.  We could (should?) define it locally for
    -- Equiv.
    postulate ext : ∀ {τ₁ τ₂} {f g : EImp τ₁ → EImp τ₂} →
                    (∀ x → f x ≡ g x) → f ≡ g

    -- Ternary helper relation for environment extensions, analogous to _↝_↝_ for contexts
    data _⊢_↝_↝_⊣ : ∀ { Γ Γ' Γ''} → Γ ↝ Γ' ↝ Γ'' → Env Γ → Env Γ' → Env Γ'' → Set where
      refl : ∀ {Γ Γ''} {Γ↝Γ'' : Γ ↝ Γ''} { env env'' } →
             Γ↝Γ'' ⊢ env ↝ env'' →
             ↝↝-base Γ↝Γ'' ⊢ env ↝ [] ↝ env'' ⊣
      extend : ∀ {Γ Γ' Γ'' τ} {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''} { env env' env'' } →
               Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
               (v : EImp τ) → ↝↝-extend Γ↝Γ'↝Γ'' ⊢ (v ∷ env) ↝ (v ∷ env') ↝ (v ∷ env'') ⊣

    -- the following lemmas are strong versions of the shifting
    -- functions, proving that consistent variable renaming preserves
    -- equivalence (and not just typing).
    lookup-elevate-≡ : ∀ {τ Γ Γ'} {Γ↝Γ' : Γ ↝ Γ'}
                       {env : Env Γ} {env' : Env Γ'} →
                       Γ↝Γ' ⊢ env ↝ env' →
                       (x : τ ∈ Γ) → lookupE x env ≡ lookupE (elevate-var Γ↝Γ' x) env'
    lookup-elevate-≡ {τ} {.Γ'} {Γ'} {.↝-refl} {.env'} {env'} (refl .env') x = refl
    lookup-elevate-≡ (extend v env↝env') x = lookup-elevate-≡ env↝env' x

    lookup-elevate2-≡ : ∀ {τ Γ Γ' Γ''} {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''}
                       {env : Env Γ} {env' : Env Γ'} {env'' : Env Γ''} →
                       Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
                       (x : τ ∈ Γ) → lookupE x env ≡ lookupE (elevate-var2 Γ↝Γ'↝Γ'' x) env''
    lookup-elevate2-≡ (refl Γ↝Γ') x = lookup-elevate-≡ Γ↝Γ' x
    lookup-elevate2-≡ (extend env↝env'↝env'' v) hd = refl
    lookup-elevate2-≡ (extend env↝env'↝env'' _) (tl x)
      rewrite lookup-elevate2-≡ env↝env'↝env'' x = refl

    lem-elevate-≡ : ∀ {τ Γ Γ' Γ''}
                      {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''}
                      {env : Env Γ} {env' : Env Γ'} {env'' : Env Γ''} →
                      Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
                      (e : Exp Γ τ) →
                      ev e env ≡ ev (elevate Γ↝Γ'↝Γ'' e) env''
    lem-elevate-≡ env↝env' (EVar x) = lookup-elevate2-≡ env↝env' x
    lem-elevate-≡ env↝env' (EInt x) = refl
    lem-elevate-≡ env↝env' (EAdd e f) with lem-elevate-≡ env↝env' e | lem-elevate-≡ env↝env' f
    ... | IA1 | IA2 = cong₂ _+_ IA1 IA2
    lem-elevate-≡ {Γ↝Γ'↝Γ'' = Γ↝Γ'↝Γ''}
                  {env = env}
                  {env'' = env''}
                  env↝env' (ELam e) = ext lem-elevate-≡-body
      where lem-elevate-≡-body : ∀ x → ev e (x ∷ env) ≡ ev (elevate (↝↝-extend Γ↝Γ'↝Γ'') e) (x ∷ env'')
            lem-elevate-≡-body x = lem-elevate-≡ (extend env↝env' x) e
    lem-elevate-≡ env↝env' (EApp e f) with lem-elevate-≡ env↝env' e | lem-elevate-≡ env↝env' f
    ... | IA1 | IA2 = cong₂ (λ f₁ x → f₁ x) IA1 IA2

    lem-lift-refl-id : ∀ {α Γ} → let τ = stripα α in
                       (env : Env Γ) →
                       (v : EImp τ) (va : Imp Γ α) →
                       Equiv env va v →
                       Equiv env (lift α ↝-refl va) v
    lem-lift-refl-id {AInt} env v va eq = eq
    lem-lift-refl-id {AFun α α₁} {Γ} env v va eq = body
      where body : ∀ {Γ'} {env' : Env Γ'} {Γ↝Γ' : Γ ↝ Γ'} →
                   Γ↝Γ' ⊢ env ↝ env' →
                   {av' : Imp Γ' α} {v' : EImp (stripα α)} →
                   Equiv env' av' v' → Equiv env' (va (↝-trans ↝-refl Γ↝Γ') av') (v v')
            body {Γ↝Γ' = Γ↝Γ'} env↝env' eq' rewrite sym (lem-↝-refl-id Γ↝Γ') = eq env↝env' eq'
    lem-lift-refl-id {D x} env v e eq rewrite sym eq = sym (lem-elevate-≡ (refl (refl env)) e)

    -- lifting an Imp does not affect equivalence
    lem-lift-equiv : ∀ {α Γ Γ'} → let τ = stripα α in
                     {Γ↝Γ' : Γ ↝ Γ'} →
                     (va : Imp Γ α) (v : EImp τ) →
                     {env : Env Γ} {env' : Env Γ'} →
                     Γ↝Γ' ⊢ env ↝ env' →
                     Equiv env va v →
                     Equiv env' (lift α Γ↝Γ' va) v
    lem-lift-equiv va v {.env'} {env'} (refl .env') eq = lem-lift-refl-id env' v va eq
    lem-lift-equiv {AInt} va v (extend v₁ env↝env') eq = eq
    lem-lift-equiv {AFun α α₁} va v (extend v₁ env↝env') eq =
      λ v₁env₁↝env' eq₁ → eq (env↝trans (extend v₁ env↝env') v₁env₁↝env') eq₁
    lem-lift-equiv {D x} va v (extend v₁ env↝env') eq
      rewrite sym eq = sym (lem-elevate-≡ (refl (extend v₁ env↝env')) va)

    lem-equiv-lookup : ∀ {α Δ Γ'} → let Γ = stripΔ Δ in
                       { aenv : AEnv Γ' Δ } {env : Env Γ} →
                       (env' : Env Γ') →
                       Equiv-Env env' aenv env →
                       ∀ x → Equiv {α} env' (lookup aenv x) (lookupE (strip-lookup x) env)
    lem-equiv-lookup env' [] ()
    lem-equiv-lookup env' (cons  enveq va v eq) hd = eq
    lem-equiv-lookup env' (cons  enveq va v eq) (tl x) = lem-equiv-lookup env' enveq x

    lem-equiv-env-lift-extend :
      ∀ {σ Γ' Δ} (env' : Env Γ') → let Γ = stripΔ Δ in
        {env : Env Γ} {aenv : AEnv Γ' Δ} →
        Equiv-Env env' aenv env → (x : EImp σ) →
        Equiv-Env (x ∷ env') (liftEnv (↝-extend ↝-refl) aenv) env
    lem-equiv-env-lift-extend _ [] x = []
    lem-equiv-env-lift-extend env' (cons {α} eqenv va v x) x₁ =
      cons (lem-equiv-env-lift-extend env' eqenv x₁)
           (lift α (↝-extend ↝-refl) va) v (lem-lift-equiv va v (extend x₁ (refl env')) x)

    lem-equiv-env-lift-lift :
      ∀ {Γ' Γ'' Δ} → let Γ = stripΔ Δ in
        {Γ↝Γ' : Γ' ↝ Γ''}
        {env' : Env Γ'} {env'' : Env Γ''}
        (env'↝env'' : Γ↝Γ' ⊢ env' ↝ env'') →
        {env : Env Γ} {aenv : AEnv Γ' Δ} →
        Equiv-Env env' aenv env →
        Equiv-Env env'' (liftEnv Γ↝Γ' aenv) env
    lem-equiv-env-lift-lift env'↝env'' [] = []
    lem-equiv-env-lift-lift {Γ↝Γ' = Γ↝Γ'} env'↝env'' (cons {α} eqenv va v x)
      with lem-equiv-env-lift-lift env'↝env'' eqenv
    ... | IA = cons IA (lift α Γ↝Γ' va) v (lem-lift-equiv va v env'↝env'' x)

    -- When we partially evaluate somthing under an environment , it
    -- will give equivalent results to a ``complete'' evaluation under
    -- an equivalent environment
    pe-correct : ∀ { α Δ Γ' } → (e : AExp Δ α) →
                 let Γ = stripΔ Δ in
                 {aenv : AEnv Γ' Δ} → {env : Env Γ} →
                 (env' : Env Γ') →
                 Equiv-Env env' aenv env →
                 Equiv env' (pe e aenv) (ev (strip e) env)
    pe-correct (Var x) env' eqenv = lem-equiv-lookup env' eqenv x
    pe-correct (AInt x) env' eqenv = refl
    pe-correct (AAdd e f) env' eqenv
      rewrite pe-correct e env' eqenv | pe-correct f env' eqenv = refl
    pe-correct (ALam e) env' eqenv =
      λ {_} {env''} env'↝env'' {av'} {v'} eq →
        let eqenv' = (lem-equiv-env-lift-lift env'↝env'' eqenv)
            eqenv'' = (cons eqenv' av' v' eq)
        in pe-correct e env'' eqenv''
    pe-correct (AApp e f) env' eqenv
      with pe-correct e env' eqenv | pe-correct f env' eqenv
    ... | IAe | IAf = IAe (refl env') IAf
    pe-correct (DInt x) env' eqenv = refl
    pe-correct (DAdd e f) env' eqenv
      rewrite pe-correct e env' eqenv | pe-correct f env' eqenv = refl
    pe-correct (DLam e) env' eqenv =
      ext (λ x → let eqenv' = (lem-equiv-env-lift-extend env' eqenv x)
                     eqenv'' = (cons eqenv' (EVar hd) x refl)
                 in pe-correct e (x ∷ env') eqenv'')
    pe-correct (DApp e f) {env = env} env' eqenv
      with pe-correct f env' eqenv | pe-correct e env' eqenv
    ... | IA' | IA = cong₂ (λ f x → f x) IA IA'
    pe-correct (Lift e) env' eqenv
      with pe-correct e env' eqenv
    ... | IA = IA

-- module PreciseAEnv where
--   open Exp-Eval
--   open import Relation.Binary.PropositionalEquality

--   data AEnv : Ctx → ACtx → Set where
--     [] : AEnv [] []
--     cons : ∀ { Γ Γ' Δ } (α : AType) → Γ ↝ Γ' → Imp Γ' α → AEnv Γ Δ → AEnv Γ' (α ∷ Δ)

--   consD : ∀ {Γ Δ} σ → AEnv Γ Δ → AEnv (σ ∷ Γ) (D σ ∷ Δ)
--   consD σ env = (cons (D σ) (↝-extend {τ = σ} ↝-refl) (EVar hd) (env))

--   lookup : ∀ {α Δ Γ} → AEnv Γ Δ → α ∈ Δ → Imp Γ α
--   lookup (cons α _ v env) hd =  v
--   lookup (cons α₁ Γ↝Γ' v env) (tl x) = lookup (cons α₁ Γ↝Γ' v env) (tl x)

--   pe : ∀ {α Δ Γ} → AExp Δ α → AEnv Γ Δ → Imp Γ α
--   pe (Var x) env = lookup env x
--   pe (AInt x) env = x
--   pe (AAdd e₁ e₂) env = pe e₁ env + pe e₂ env
--   pe (ALam {α} e) env = λ Γ↝Γ' → λ y → pe e (cons α Γ↝Γ' y env)
--   pe (AApp e₁ e₂) env = ((pe e₁ env) ↝-refl) (pe e₂ env)
--   pe (DInt x) env = EInt x
--   pe (DAdd e e₁) env = EAdd (pe e env) (pe e₁ env)
--   pe (DLam {σ} e) env = ELam (pe e (consD σ env))
--   pe (DApp e e₁) env = EApp (pe e env) (pe e₁ env)

--   -- What is a suitable environment to interpret an AExp without pe?
--   -- 1-1 mapping from AExp into Exp
--   stripα : AType → Type
--   stripα AInt = Int
--   stripα (AFun α₁ α₂) = Fun (stripα α₁) (stripα α₂)
--   stripα (D x) = x

--   stripΔ : ACtx → Ctx
--   stripΔ = map stripα

--   stripEnv : ∀ {Δ} →
--              let Γ = stripΔ Δ
--              in AEnv Γ Δ → Env Γ
--   stripEnv [] = []
--   stripEnv (cons AInt Γ↝Γ' v env) = v ∷ (stripEnv {!!})
--   stripEnv (cons (AFun α α₁) Γ↝Γ' v env) = {!!}
--   stripEnv (cons (D x) Γ↝Γ' v env) = {!!}

--   -- Extending a value environment according to an extension of a type environment
--   data _⊢_↝_ {Γ} : ∀ {Γ'} → Γ ↝ Γ' → Env Γ → Env Γ' → Set where
--     refl : ∀ env → ↝-refl ⊢ env ↝ env
--     extend : ∀ {τ Γ' env env'} →  {Γ↝Γ' : Γ ↝ Γ'} →
--                (v : EImp τ) → (Γ↝Γ' ⊢  env ↝ env')  →
--                ↝-extend Γ↝Γ' ⊢ env ↝ (v ∷ env')

--   -- It turns out that we have to shift Exp also
--   liftE : ∀ {τ Γ Γ'} → Γ ↝ Γ' → Exp Γ τ → Exp Γ' τ
--   liftE Γ↝Γ' e = elevate (↝↝-base Γ↝Γ') e

--   Equiv : ∀ {α Γ} → Env Γ → Imp Γ α → EImp (stripα α) → Set
--   Equiv {AInt} env av v = av ≡ v
--   Equiv {AFun α₁ α₂} {Γ} env av v = -- an pe-d static function is
--                                     -- equivalent to an EImp value
--                                     -- if given an suitably extended
--                                     -- environment, evaluating the
--                                     -- body yields something
--                                       -- equivalent to the EImp-value
--     ∀ {Γ' env' Γ↝Γ'} → (Γ↝Γ' ⊢ env ↝ env') →
--       {av' : Imp Γ' α₁} → {v' : EImp (stripα α₁)} →
--       Equiv env' av' v' → Equiv env' (av Γ↝Γ' av') (v v')
--   Equiv {D x} {Γ} env av v = ev av env ≡ v

--   data Equiv-Env : ∀ {Δ} → let Γ = stripΔ Δ in
--                    AEnv Γ Δ → Env Γ → Set where
--     [] : Equiv-Env [] []
--     -- cons : ∀ {α Δ} → let Γ = stripΔ Δ in

--     --         (va : Imp Γ α) → (v : EImp (stripα α)) →
--     --         (env : Env Γ) → Equiv env v va →
--     --         (aenv : AEnv Γ Δ) →
--     --         Equiv-Env aenv env →
--     --         Equiv-Env {α ∷ Δ} (cons α (lift α (↝-extend ↝-refl) va)
--     --                                   (liftEnv (↝-extend ↝-refl) aenv))
--     --                           (v ∷ env)

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
module Prelude where

id : {A : Set} -> A -> A
id x = x

_·_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
f · g = \ x -> f (g x)

flip : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
flip f x y = f y x

Rel : Set -> Set1
Rel X = X -> X -> Set

data False : Set where
record True : Set where

tt : True
tt = _

! : {A : Set} -> A -> True
! = _

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : {A : Set}(P : A -> Set){x y : A} -> x == y -> P y -> P x
subst P refl p = p

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

sym : {A : Set}{x y : A} -> x == y -> y == x
sym refl = refl

trans : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
trans refl yz = yz

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

infixr 10 _,_

record Σ (A : Set)(B : A -> Set) : Set where
  field
    fst : A
    snd : B fst

_,,_ : {A : Set}{B : A -> Set}(x : A) -> B x -> Σ A B
x ,, y = record { fst = x; snd = y }

private module Σp {A : Set}{B : A -> Set} = Σ {A}{B}
open Σp public

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

data Bool : Set where
  false : Bool
  true  : Bool

IsTrue : Bool -> Set
IsTrue false = False
IsTrue true  = True

IsFalse : Bool -> Set
IsFalse true  = False
IsFalse false = True

data Inspect (b : Bool) : Set where
  itsTrue  : IsTrue b -> Inspect b
  itsFalse : IsFalse b -> Inspect b

inspect : (b : Bool) -> Inspect b
inspect true  = itsTrue  _
inspect false = itsFalse _

data LeqBool : Rel Bool where
  ref : {b : Bool} -> LeqBool b b
  up  : LeqBool false true

One : Rel True
One _ _ = True

_[×]_ : {A B : Set} -> Rel A -> Rel B -> Rel (A × B)
(R [×] S) (a₁ , b₁) (a₂ , b₂) = R a₁ a₂ × S b₁ b₂

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
postulate
  @0 A : Set

_ : (@0 B : Set) .(C : Set) → Set
_ = λ B C → ?

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
import Common.Level
open import Common.Equality

record Sigma (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Sigma

-- projected bound var
fail : (A : Set) (B : A -> Set) ->
  let X : A -> Sigma A B
      X = _
  in  (z : Sigma A B) -> X (fst z) ≡ z
fail A B z = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Another definition of indexed containers
------------------------------------------------------------------------

-- Partly based on "Indexed containers" by Altenkirch, Ghani, Hancock,
-- McBride and Morris, and partly based on "Non-wellfounded trees in
-- Homotopy Type Theory" by Ahrens, Capriotti and Spadotti.

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

open import Equality

module Container.Indexed.Variant
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

import Bijection eq as B
open import Container.Indexed eq as C
  using (_⇾_; id⇾; _∘⇾_; Shape; Position; index)
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level.Closure eq
open import Tactic.Sigma-cong eq
open import Univalence-axiom eq

private
  variable
    a ℓ p p₁ p₂ p′ q : Level
    A I O            : Type a
    P Q R            : A → Type p
    ext f i k o s    : A

------------------------------------------------------------------------
-- Containers

-- Doubly indexed containers.

record Container₂
         (I : Type i) (O : Type o) s p :
         Type (i ⊔ o ⊔ lsuc (s ⊔ p)) where
  constructor _◁_
  field
    Shape    : O → Type s
    Position : ∀ {o} → Shape o → I → Type p

open Container₂ public

-- Singly indexed containers.

Container : Type i → ∀ s p → Type (i ⊔ lsuc (s ⊔ p))
Container I = Container₂ I I

private
  variable
    C : Container₂ I O s p

-- Container₂ can be expressed as a Σ-type.

Container≃Σ :
  Container₂ I O s p ≃
  (∃ λ (S : O → Type s) → ∀ {o} → S o → I → Type p)
Container≃Σ = Eq.↔→≃ (λ (S ◁ P) → S , P) (uncurry _◁_) refl refl

------------------------------------------------------------------------
-- Polynomial functors

-- The polynomial functor associated to a container.

⟦_⟧ :
  {I : Type i} {O : Type o} →
  Container₂ I O s p → (I → Type ℓ) → O → Type (ℓ ⊔ i ⊔ s ⊔ p)
⟦ S ◁ P ⟧ Q o = ∃ λ (s : S o) → P s ⇾ Q

-- A map function.

map : (C : Container₂ I O s p) → P ⇾ Q → ⟦ C ⟧ P ⇾ ⟦ C ⟧ Q
map C f _ (s , g) = s , f ∘⇾ g

-- Functor laws.

map-id : map C (id⇾ {P = P}) ≡ id⇾
map-id = refl _

map-∘ :
  (f : Q ⇾ R) (g : P ⇾ Q) →
  map C (f ∘⇾ g) ≡ map C f ∘⇾ map C g
map-∘ _ _ = refl _

-- A preservation lemma.

⟦⟧-cong :
  {I : Type i} {P₁ : I → Type p₁} {P₂ : I → Type p₂} →
  Extensionality? k (i ⊔ p) (p ⊔ p₁ ⊔ p₂) →
  (C : Container₂ I O s p) →
  (∀ i → P₁ i ↝[ k ] P₂ i) →
  (∀ o → ⟦ C ⟧ P₁ o ↝[ k ] ⟦ C ⟧ P₂ o)
⟦⟧-cong {i = i} {k = k} {p = p} {P₁ = Q₁} {P₂ = Q₂}
        ext (S ◁ P) Q₁↝Q₂ o =
  (∃ λ (s : S o) → P s ⇾ Q₁)  ↝⟨ (∃-cong λ _ →
                                  ∀-cong (lower-extensionality? k p lzero ext) λ _ →
                                  ∀-cong (lower-extensionality? k i p ext) λ _ →
                                  Q₁↝Q₂ _) ⟩□
  (∃ λ (s : S o) → P s ⇾ Q₂)  □

-- The forward direction of ⟦⟧-cong is an instance of map (at least
-- when k is equivalence).

_ : _≃_.to (⟦⟧-cong ext C f o) ≡ map C (_≃_.to ∘ f) o
_ = refl _

-- The shapes of a container are pointwise equivalent to the
-- polynomial functor of the container applied to the constant
-- function yielding the unit type.
--
-- (This lemma was suggested to me by an anonymous reviewer of a
-- paper.)

Shape≃⟦⟧⊤ :
  (C : Container₂ I O s p) →
  Shape C o ≃ ⟦ C ⟧ (λ _ → ⊤) o
Shape≃⟦⟧⊤ {o = o} (S ◁ P) =
  S o                                ↔⟨ inverse $ drop-⊤-right (λ _ → →-right-zero F.∘ inverse currying) ⟩□
  (∃ λ (s : S o) → ∀ i → P s i → ⊤)  □

------------------------------------------------------------------------
-- Coalgebras

-- The type of coalgebras for a (singly indexed) container.

Coalgebra : {I : Type i} → Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Coalgebra {i = i} {s = s} {p = p} {I = I} C =
  ∃ λ (P : I → Type (i ⊔ s ⊔ p)) → P ⇾ ⟦ C ⟧ P

-- Coalgebra morphisms.

infix 4 _⇨_

_⇨_ :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Coalgebra C → Type (i ⊔ s ⊔ p)
(P , f) ⇨ (Q , g) = ∃ λ (h : P ⇾ Q) → g ∘⇾ h ≡ map _ h ∘⇾ f

private
  variable
    X Y Z : Coalgebra C

-- An identity morphism.

id⇨ : X ⇨ X
id⇨ = id⇾ , refl _

-- Composition for _⇨_.

infix 9 [_]_∘⇨_

[_]_∘⇨_ : ∀ Z → Y ⇨ Z → X ⇨ Y → X ⇨ Z
[_]_∘⇨_ {Y = _ , g} {X = _ , f} (_ , h) (f₁ , eq₁) (f₂ , eq₂) =
    f₁ ∘⇾ f₂
  , (h ∘⇾ (f₁ ∘⇾ f₂)              ≡⟨⟩
     (h ∘⇾ f₁) ∘⇾ f₂              ≡⟨ cong (_∘⇾ f₂) eq₁ ⟩
     (map _ f₁ ∘⇾ g) ∘⇾ f₂        ≡⟨⟩
     map _ f₁ ∘⇾ (g ∘⇾ f₂)        ≡⟨ cong (map _ f₁ ∘⇾_) eq₂ ⟩
     map _ f₁ ∘⇾ (map _ f₂ ∘⇾ f)  ≡⟨⟩
     map _ (f₁ ∘⇾ f₂) ∘⇾ f        ∎)

-- The property of being a final coalgebra.

Final :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Type (lsuc (i ⊔ s ⊔ p))
Final X = ∀ Y → Contractible (Y ⇨ X)

-- A perhaps more traditional definition of what it means to be final.

Final′ :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Type (lsuc (i ⊔ s ⊔ p))
Final′ X =
  ∀ Y → ∃ λ (m : Y ⇨ X) → (m′ : Y ⇨ X) → proj₁ m ≡ proj₁ m′

-- Final X implies Final′ X.

Final→Final′ : (X : Coalgebra C) → Final X → Final′ X
Final→Final′ _ =
  ∀-cong _ λ _ → ∃-cong λ _ → ∀-cong _ λ _ → cong proj₁

-- Final is pointwise propositional (assumption extensionality).

Final-propositional :
  {I : Type i} {C : Container I s p} →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  (X : Coalgebra C) →
  Is-proposition (Final X)
Final-propositional ext _ =
  Π-closure ext 1 λ _ →
  Contractible-propositional (lower-extensionality _ lzero ext)

-- Final coalgebras.

Final-coalgebra :
  {I : Type i} →
  Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Final-coalgebra C = ∃ λ (X : Coalgebra C) → Final X

-- Final coalgebras, defined using Final′.

Final-coalgebra′ :
  {I : Type i} →
  Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Final-coalgebra′ C = ∃ λ (X : Coalgebra C) → Final′ X

-- Final-coalgebra C implies Final-coalgebra′ C.

Final-coalgebra→Final-coalgebra′ :
  Final-coalgebra C → Final-coalgebra′ C
Final-coalgebra→Final-coalgebra′ =
  ∃-cong Final→Final′

-- Carriers of final coalgebras (defined using Final′) for a given
-- container are pointwise equivalent.

carriers-of-final-coalgebras-equivalent′ :
  (((P₁ , _) , _) ((P₂ , _) , _) : Final-coalgebra′ C) →
  ∀ i → P₁ i ≃ P₂ i
carriers-of-final-coalgebras-equivalent′ (X₁ , final₁) (X₂ , final₂) i =
  Eq.↔→≃ (proj₁ to i) (proj₁ from i) to∘from from∘to
  where
  to : X₁ ⇨ X₂
  to = proj₁ (final₂ X₁)

  from : X₂ ⇨ X₁
  from = proj₁ (final₁ X₂)

  to∘from : ∀ x → proj₁ ([ X₂ ] to ∘⇨ from) i x ≡ x
  to∘from x =
    proj₁ ([ X₂ ] to ∘⇨ from) i x  ≡⟨ cong (λ f → f i x) $ sym $ proj₂ (final₂ X₂) $ [ X₂ ] to ∘⇨ from ⟩
    proj₁ (proj₁ (final₂ X₂)) i x  ≡⟨ cong (λ f → f i x) $ proj₂ (final₂ X₂) id⇨ ⟩
    proj₁ (id⇨ {X = X₂}) i x       ≡⟨⟩
    x                              ∎

  from∘to : ∀ x → proj₁ ([ X₁ ] from ∘⇨ to) i x ≡ x
  from∘to x =
    proj₁ ([ X₁ ] from ∘⇨ to) i x  ≡⟨ cong (λ f → f i x) $ sym $ proj₂ (final₁ X₁) $ [ X₁ ] from ∘⇨ to ⟩
    proj₁ (proj₁ (final₁ X₁)) i x  ≡⟨ cong (λ f → f i x) $ proj₂ (final₁ X₁) id⇨ ⟩
    proj₁ (id⇨ {X = X₁}) i x       ≡⟨⟩
    x                              ∎

-- The previous lemma relates the "out" functions of the two final
-- coalgebras in a certain way.

out-related′ :
  {C : Container I s p}
  (F₁@((_ , out₁) , _) F₂@((_ , out₂) , _) : Final-coalgebra′ C) →
  map C (_≃_.to ∘ carriers-of-final-coalgebras-equivalent′ F₁ F₂) ∘⇾
    out₁
    ≡
  out₂ ∘⇾ (_≃_.to ∘ carriers-of-final-coalgebras-equivalent′ F₁ F₂)
out-related′ (X₁ , _) (_ , final₂) =
  sym $ proj₂ (proj₁ (final₂ X₁))

-- Carriers of final coalgebras for a given container are pointwise
-- equivalent.

carriers-of-final-coalgebras-equivalent :
  (((P₁ , _) , _) ((P₂ , _) , _) : Final-coalgebra C) →
  ∀ i → P₁ i ≃ P₂ i
carriers-of-final-coalgebras-equivalent =
  carriers-of-final-coalgebras-equivalent′ on
    Final-coalgebra→Final-coalgebra′

-- The previous lemma relates the "out" functions of the two final
-- coalgebras in a certain way.

out-related :
  {C : Container I s p}
  (F₁@((_ , out₁) , _) F₂@((_ , out₂) , _) : Final-coalgebra C) →
  map C (_≃_.to ∘ carriers-of-final-coalgebras-equivalent F₁ F₂) ∘⇾ out₁
    ≡
  out₂ ∘⇾ (_≃_.to ∘ carriers-of-final-coalgebras-equivalent F₁ F₂)
out-related = out-related′ on Final-coalgebra→Final-coalgebra′

-- If X and Y are final coalgebras (with finality defined using
-- Final′), then—assuming extensionality—finality of X (defined using
-- Final) is equivalent to finality of Y.

Final′→Final≃Final :
  {I : Type i} {C : Container I s p}
  ((X , _) (Y , _) : Final-coalgebra′ C) →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  Final X ↝[ lsuc (i ⊔ s ⊔ p) ∣ i ⊔ s ⊔ p ] Final Y
Final′→Final≃Final {i = i} {s = s} {p = p} {C = C}
  ((X₁ , out₁) , final₁) ((X₂ , out₂) , final₂) ext {k = k} ext′ =
  ∀-cong ext′ λ Y@(_ , f) →
  H-level-cong
    (lower-extensionality? k _ lzero ext′)
    0
    (Σ-cong (lemma₂ Y) λ g →

       out₁ ∘⇾ g ≡ map C g ∘⇾ f                 ↝⟨ inverse $ Eq.≃-≡ (lemma₃ Y) ⟩

       _≃_.to (lemma₃ Y) (out₁ ∘⇾ g) ≡
       _≃_.to (lemma₃ Y) (map C g ∘⇾ f)         ↔⟨⟩

       map C (_≃_.to ∘ lemma₁) ∘⇾ out₁ ∘⇾ g ≡
       map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f  ↝⟨ ≡⇒↝ _ $ cong (λ h → h ∘⇾ g ≡ map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f) $
                                                   out-related′ ((X₁ , out₁) , final₁) ((X₂ , out₂) , final₂) ⟩
       out₂ ∘⇾ (_≃_.to ∘ lemma₁) ∘⇾ g ≡
       map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f  ↔⟨⟩

       out₂ ∘⇾ _≃_.to (lemma₂ Y) g ≡
       map C (_≃_.to (lemma₂ Y) g) ∘⇾ f         □)
  where
  ext₁ = lower-extensionality (s ⊔ p) lzero ext
  ext₂ = lower-extensionality (i ⊔ s) lzero ext

  lemma₁ : ∀ i → X₁ i ≃ X₂ i
  lemma₁ =
    carriers-of-final-coalgebras-equivalent′
      ((X₁ , out₁) , final₁)
      ((X₂ , out₂) , final₂)

  lemma₂ : ((Y , _) : Coalgebra C) → (Y ⇾ X₁) ≃ (Y ⇾ X₂)
  lemma₂ _ =
    ∀-cong ext₁ λ _ →
    ∀-cong ext  λ _ →
    lemma₁ _

  lemma₃ : ((Y , _) : Coalgebra C) → (Y ⇾ ⟦ C ⟧ X₁) ≃ (Y ⇾ ⟦ C ⟧ X₂)
  lemma₃ _ =
    ∀-cong ext₁ λ _ →
    ∀-cong ext  λ _ →
    ⟦⟧-cong ext₂ C lemma₁ _

-- If there is a final C-coalgebra, and we have Final′ X for some
-- C-coalgebra X, then we also have Final X (assuming extensionality).

Final′→Final :
  {I : Type i} {C : Container I s p} →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  Final-coalgebra C →
  ((X , _) : Final-coalgebra′ C) →
  Final X
Final′→Final ext F₁@(_ , final₁) F₂ =
  Final′→Final≃Final
    (Final-coalgebra→Final-coalgebra′ F₁) F₂
    ext _ final₁

-- Final-coalgebra is pointwise propositional, assuming extensionality
-- and univalence.
--
-- This is a variant of Lemma 5 from "Non-wellfounded trees in
-- Homotopy Type Theory".

Final-coalgebra-propositional :
  {I : Type i} {C : Container I s p} →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (lsuc (i ⊔ s ⊔ p)) →
  Univalence (i ⊔ s ⊔ p) →
  Is-proposition (Final-coalgebra C)
Final-coalgebra-propositional {I = I} {C = C@(S ◁ P)}
  ext univ F₁@((P₁ , out₁) , _) F₂@(X₂@(P₂ , out₂) , _) =
  block λ b →
  Σ-≡,≡→≡ (Σ-≡,≡→≡ (lemma₁ b) (lemma₂ b))
    (Final-propositional (lower-extensionality lzero _ ext) X₂ _ _)
  where
  ext₁′ = lower-extensionality _ lzero ext
  ext₁  = Eq.good-ext ext₁′

  lemma₀ : Block "lemma₀" → ∀ i → P₁ i ≃ P₂ i
  lemma₀ ⊠ = carriers-of-final-coalgebras-equivalent F₁ F₂

  lemma₀-lemma :
    ∀ b x →
    map C (_≃_.to ∘ lemma₀ b) i (out₁ i (_≃_.from (lemma₀ b i) x)) ≡
    out₂ i x
  lemma₀-lemma {i = i} ⊠ x =
    map C (_≃_.to ∘ lemma₀ ⊠) i (out₁ i (_≃_.from (lemma₀ ⊠ i) x))  ≡⟨ cong (λ f → f _ (_≃_.from (lemma₀ ⊠ i) x)) $
                                                                       out-related F₁ F₂ ⟩
    out₂ i (_≃_.to (lemma₀ ⊠ i) (_≃_.from (lemma₀ ⊠ i) x))          ≡⟨ cong (out₂ _) $
                                                                       _≃_.right-inverse-of (lemma₀ ⊠ i) _ ⟩∎
    out₂ i x                                                        ∎

  lemma₁ : Block "lemma₀" → P₁ ≡ P₂
  lemma₁ b =
    apply-ext ext₁ λ i →
    ≃⇒≡ univ (lemma₀ b i)

  lemma₁-lemma₁ = λ b i →
    sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (subst-const _)   ≡⟨ cong sym Σ-≡,≡→≡-subst-const-refl ⟩
    sym $ cong₂ _,_ (sym (lemma₁ b)) (refl _)        ≡⟨ sym cong₂-sym ⟩
    cong₂ _,_ (sym (sym (lemma₁ b))) (sym (refl _))  ≡⟨ cong₂ (cong₂ _) (sym-sym _) sym-refl ⟩
    cong₂ _,_ (lemma₁ b) (refl i)                    ≡⟨ cong₂-reflʳ _ ⟩∎
    cong (_, i) (lemma₁ b)                           ∎

  lemma₁-lemma₂ = λ b i x →
    subst (_$ i) (sym (lemma₁ b)) x                                    ≡⟨⟩
    subst (_$ i) (sym (apply-ext ext₁ λ i → ≃⇒≡ univ (lemma₀ b i))) x  ≡⟨ cong (flip (subst (_$ i)) _) $ sym $
                                                                          Eq.good-ext-sym ext₁′ _ ⟩
    subst (_$ i) (apply-ext ext₁ λ i → sym (≃⇒≡ univ (lemma₀ b i))) x  ≡⟨ Eq.subst-good-ext ext₁′ _ _ ⟩
    subst id (sym (≃⇒≡ univ (lemma₀ b i))) x                           ≡⟨ subst-id-in-terms-of-inverse∘≡⇒↝ equivalence ⟩
    _≃_.from (≡⇒≃ (≃⇒≡ univ (lemma₀ b i))) x                           ≡⟨ cong (λ eq → _≃_.from eq _) $
                                                                          _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎
    _≃_.from (lemma₀ b i) x                                            ∎

  lemma₁-lemma₃ : ∀ b (f : P s ⇾ P₁) i p → _ ≡ _
  lemma₁-lemma₃ b f i p =
    subst (_$ i) (lemma₁ b) (f i p)                                    ≡⟨⟩
    subst (_$ i) (apply-ext ext₁ λ i → ≃⇒≡ univ (lemma₀ b i)) (f i p)  ≡⟨ Eq.subst-good-ext ext₁′ _ _ ⟩
    subst id (≃⇒≡ univ (lemma₀ b i)) (f i p)                           ≡⟨ subst-id-in-terms-of-≡⇒↝ equivalence ⟩
    ≡⇒→ (≃⇒≡ univ (lemma₀ b i)) (f i p)                                ≡⟨ cong (λ eq → _≃_.to eq _) $
                                                                          _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎
    _≃_.to (lemma₀ b i) (f i p)                                        ∎

  lemma₂ = λ b →
    apply-ext (lower-extensionality _ _ ext) λ i →
    apply-ext (lower-extensionality _ _ ext) λ x →

    subst (λ P → P ⇾ ⟦ C ⟧ P) (lemma₁ b) out₁ i x                   ≡⟨⟩

    subst (λ P → ∀ i → P i → ⟦ C ⟧ P i) (lemma₁ b) out₁ i x         ≡⟨ cong (_$ x) subst-∀ ⟩

    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (refl _))
      (out₁ (subst (λ _ → I) (sym (lemma₁ b)) i)) x                 ≡⟨ elim¹
                                                                         (λ {i′} eq →
                                                                            subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
                                                                              (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (refl _))
                                                                              (out₁ (subst (λ _ → I) (sym (lemma₁ b)) i)) x ≡
                                                                            subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
                                                                              (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) eq)
                                                                              (out₁ i′) x)
                                                                         (refl _)
                                                                         _ ⟩
    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (subst-const _))
      (out₁ i) x                                                    ≡⟨ cong (λ eq → subst (uncurry λ P i → P i → ⟦ C ⟧ P i) eq _ _) $
                                                                       lemma₁-lemma₁ b i ⟩
    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (cong (_, _) (lemma₁ b))
      (out₁ i) x                                                    ≡⟨ cong (_$ x) $ sym $ subst-∘ _ _ _ ⟩

    subst (λ P → P i → ⟦ C ⟧ P i) (lemma₁ b) (out₁ i) x             ≡⟨ subst-→ ⟩

    subst (λ P → ⟦ C ⟧ P i) (lemma₁ b)
      (out₁ i (subst (_$ i) (sym (lemma₁ b)) x))                    ≡⟨ cong (subst (λ P → ⟦ C ⟧ P i) _) $ cong (out₁ _) $
                                                                       lemma₁-lemma₂ b i x ⟩
    subst (λ P → ⟦ C ⟧ P i) (lemma₁ b)
      (out₁ i (_≃_.from (lemma₀ b i) x))                            ≡⟨⟩

    subst (λ Q → ∃ λ (s : S i) → P s ⇾ Q) (lemma₁ b)
      (out₁ i (_≃_.from (lemma₀ b i) x))                            ≡⟨ push-subst-pair-× _ _ ⟩

    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , subst (λ Q → P s ⇾ Q) (lemma₁ b) f)                        ≡⟨ (let s , _ = out₁ i (_≃_.from (lemma₀ b i) x) in
                                                                        cong (s ,_) $
                                                                        apply-ext (lower-extensionality _ _ ext) λ _ → sym $
                                                                        push-subst-application _ _) ⟩
    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , λ i → subst (λ Q → P s i → Q i) (lemma₁ b) (f i))          ≡⟨ (let s , _ = out₁ i (_≃_.from (lemma₀ b i) x) in
                                                                        cong (s ,_) $
                                                                        apply-ext (lower-extensionality _ _ ext) λ _ →
                                                                        apply-ext (lower-extensionality _ _ ext) λ _ → sym $
                                                                        push-subst-application _ _) ⟩
    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , λ i p → subst (_$ i) (lemma₁ b) (f i p))                   ≡⟨ (let _ , f = out₁ i (_≃_.from (lemma₀ b i) x) in
                                                                        cong (_ ,_) $
                                                                        apply-ext (lower-extensionality _ _ ext) λ i →
                                                                        apply-ext (lower-extensionality _ _ ext) $
                                                                        lemma₁-lemma₃ b f i) ⟩
    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , λ i p → _≃_.to (lemma₀ b i) (f i p))                       ≡⟨⟩

    map C (_≃_.to ∘ lemma₀ b) i (out₁ i (_≃_.from (lemma₀ b i) x))  ≡⟨ lemma₀-lemma b x ⟩∎

    out₂ i x                                                        ∎

------------------------------------------------------------------------
-- Conversion lemmas

-- A conversion lemma for Container. Note that the last index is not
-- unrestricted.

Container⇔Container :
  ∀ {I : Type i} {O : Type o} p →
  Container₂ I O s (i ⊔ p) ⇔ C.Container₂ I O s (i ⊔ p)
Container⇔Container {i = iℓ} {s = s} {I = I} {O = O} p =
  Container₂ I O s (iℓ ⊔ p)                 ↔⟨ Container≃Σ ⟩

  (∃ λ (S : O → Type s) →
   ∀ {o} → S o → I → Type (iℓ ⊔ p))         ↔⟨ (∃-cong λ _ →
                                                B.implicit-Π↔Π) ⟩
  (∃ λ (S : O → Type s) →
   ∀ o (s : S o) → I → Type (iℓ ⊔ p))       ↝⟨ (∃-cong λ _ → ∀-cong _ λ _ → ∀-cong _ λ _ →
                                                Pow⇔Fam p) ⟩
  (∃ λ (S : O → Type s) →
   ∀ o (s : S o) →
   ∃ λ (P : Type (iℓ ⊔ p)) → P → I)         ↝⟨ (∃-cong λ _ →
                                                from-bijection ΠΣ-comm F.∘
                                                ∀-cong _ λ _ → from-bijection ΠΣ-comm) ⟩
  (∃ λ (S : O → Type s) →
   ∃ λ (P : ∀ o → S o → Type (iℓ ⊔ p)) →
   ∀ o (s : S o) → P o s → I)               ↝⟨ (∃-cong λ _ → inverse $
                                                Σ-cong-refl {k₂ = logical-equivalence} B.implicit-Π↔Π λ _ →
                                                (∀-cong _ λ _ →
                                                 from-bijection B.implicit-Π↔Π) F.∘
                                                from-bijection B.implicit-Π↔Π) ⟩
  (∃ λ (S : O → Type s) →
   ∃ λ (P : ∀ {o} → S o → Type (iℓ ⊔ p)) →
   ∀ {o} {s : S o} → P s → I)               ↔⟨ inverse C.Container≃Σ ⟩□

  C.Container₂ I O s (iℓ ⊔ p)               □

-- Another conversion lemma for Container.

Container≃Container :
  ∀ {I : Type i} {O : Type o} p →
  Extensionality (i ⊔ o ⊔ s) (lsuc i ⊔ s ⊔ lsuc p) →
  Univalence (i ⊔ p) →
  Container₂ I O s (i ⊔ p) ≃ C.Container₂ I O s (i ⊔ p)
Container≃Container {i = i} {o = o} {s = s} {I = I} {O = O} p ext univ =
  Container₂ I O s (i ⊔ p)                 ↝⟨ Container≃Σ ⟩

  (∃ λ (S : O → Type s) →
   ∀ {o} → S o → I → Type (i ⊔ p))         ↔⟨ (∃-cong λ _ →
                                               B.implicit-Π↔Π) ⟩
  (∃ λ (S : O → Type s) →
   ∀ o (s : S o) → I → Type (i ⊔ p))       ↔⟨ (∃-cong λ _ →
                                               ∀-cong (lower-extensionality l r ext) λ _ →
                                               ∀-cong (lower-extensionality l r ext) λ _ →
                                               Pow↔Fam p (lower-extensionality l r ext) univ) ⟩
  (∃ λ (S : O → Type s) →
   ∀ o (s : S o) →
   ∃ λ (P : Type (i ⊔ p)) → P → I)         ↔⟨ (∃-cong λ _ →
                                               ΠΣ-comm F.∘
                                               ∀-cong (lower-extensionality l r ext) λ _ → ΠΣ-comm) ⟩
  (∃ λ (S : O → Type s) →
   ∃ λ (P : ∀ o → S o → Type (i ⊔ p)) →
   ∀ o (s : S o) → P o s → I)              ↝⟨ (∃-cong λ _ → inverse $
                                               Σ-cong-refl {k₂ = logical-equivalence} B.implicit-Π↔Π λ _ →
                                               (∀-cong _ λ _ →
                                                from-bijection B.implicit-Π↔Π) F.∘
                                               from-bijection B.implicit-Π↔Π) ⟩
  (∃ λ (S : O → Type s) →
   ∃ λ (P : ∀ {o} → S o → Type (i ⊔ p)) →
   ∀ {o} {s : S o} → P s → I)              ↝⟨ inverse C.Container≃Σ ⟩□

  C.Container₂ I O s (i ⊔ p)               □
  where
  l = i ⊔ o ⊔ s
  r = lsuc i ⊔ s ⊔ lsuc p

-- The two conversion lemmas for Container are related.

_ :
  {I : Type i} {univ : Univalence (i ⊔ p)} →
  _≃_.logical-equivalence
    (Container≃Container {I = I} {O = O} p ext univ) ≡
  Container⇔Container p
_ = refl _

-- A conversion lemma for ⟦_⟧.

⟦⟧≃⟦⟧ :
  ∀ p →
  {I : Type i} (C : Container₂ I O s (i ⊔ p)) {P : I → Type ℓ} →
  ∀ o →
  C.⟦ _⇔_.to (Container⇔Container p) C ⟧ P o ≃ ⟦ C ⟧ P o
⟦⟧≃⟦⟧ _ {I = I} C {P = P} o =
  (∃ λ (s : Shape C o) → ((i , _) : Σ I (Position C s)) → P i)  ↔⟨ (∃-cong λ _ → currying) ⟩□
  (∃ λ (s : Shape C o) → (i : I) → Position C s i → P i)        □

-- Another conversion lemma for ⟦_⟧.

⟦⟧≃⟦⟧′ :
  ∀ p →
  {I : Type i} (C : C.Container₂ I O s (i ⊔ p)) {P : I → Type ℓ} →
  ∀ o →
  ⟦ _⇔_.from (Container⇔Container p) C ⟧ P o ↝[ i ⊔ p ∣ i ⊔ p ⊔ ℓ ]
  C.⟦ C ⟧ P o
⟦⟧≃⟦⟧′ {i = i} {ℓ = ℓ} p {I = I} C {P = P} _ {k = k} ext =
  ∃-cong λ s →

  ((i : I) → (∃ λ (p : C .Position s) → C .index p ≡ i) → P i)     ↝⟨ (∀-cong (lower-extensionality? k l r ext) λ _ →
                                                                       from-bijection currying) ⟩

  ((i : I) (p : C .Position s) → C .index p ≡ i → P i)             ↔⟨ Π-comm ⟩

  ((p : C .Position s) (i : I) → C .index p ≡ i → P i)             ↝⟨ (∀-cong (lower-extensionality? k l r ext) λ _ →
                                                                       ∀-cong (lower-extensionality? k l r ext) λ _ →
                                                                       ∀-cong (lower-extensionality? k l r ext) λ eq →
                                                                       ≡⇒↝ _ $ cong P (sym eq)) ⟩

  ((p : C .Position s) (i : I) → C .index p ≡ i → P (C .index p))  ↝⟨ (∀-cong (lower-extensionality? k l r ext) λ _ →
                                                                       from-bijection $ inverse currying) ⟩
  ((p : C .Position s) → (∃ λ (i : I) → C .index p ≡ i) →
   P (C .index p))                                                 ↝⟨ (∀-cong (lower-extensionality? k l r ext) λ _ →
                                                                       drop-⊤-left-Π (lower-extensionality? k l r ext) $
                                                                       _⇔_.to contractible⇔↔⊤ $
                                                                       other-singleton-contractible _) ⟩□
  ((p : C .Position s) → P (C .index p))                           □
  where
  l = i ⊔ p
  r = i ⊔ p ⊔ ℓ

-- The map functions commute with ⟦⟧≃⟦⟧ (in a certain sense).

_ :
  map C f ∘⇾ (_≃_.to ∘ ⟦⟧≃⟦⟧ p C) ≡
  (_≃_.to ∘ ⟦⟧≃⟦⟧ p C) ∘⇾ C.map (_⇔_.to (Container⇔Container p) C) f
_ = refl _

-- The map functions commute with ⟦⟧≃⟦⟧′ (in a certain sense, assuming
-- extensionality).

map≡map′ :
  {I : Type i} {O : Type o} {P : I → Type p} {Q : I → Type q} →
  ∀ p′ →
  Extensionality (i ⊔ o ⊔ p ⊔ s ⊔ p′) (i ⊔ p ⊔ q ⊔ s ⊔ p′) →
  (C : C.Container₂ I O s (i ⊔ p′)) {f : P ⇾ Q} →
  C.map C f ∘⇾ (λ o → ⟦⟧≃⟦⟧′ p′ C o _) ≡
  (λ o → ⟦⟧≃⟦⟧′ p′ C o _) ∘⇾ map (_⇔_.from (Container⇔Container p′) C) f
map≡map′ {i = i} {o = o} {p = p} {q = q} {s = s} {P = P} {Q = Q}
  p′ ext C {f = f} =
  apply-ext (lower-extensionality l r ext) λ _ →
  apply-ext (lower-extensionality l r ext) λ (_ , g) →
  cong (_ ,_) $
  apply-ext (lower-extensionality l r ext) λ p →
  let i = C .index p in

  f i (≡⇒↝ _ (cong P (sym (refl _))) (g i (p , refl _)))  ≡⟨ cong (λ eq → f i (≡⇒↝ _ eq (g i (p , refl _)))) $
                                                             trans (cong (cong P) sym-refl) $
                                                             cong-refl _ ⟩
  f i (≡⇒↝ _ (refl _) (g i (p , refl _)))                 ≡⟨ cong (f i) $ cong (_$ g i (p , refl _))
                                                             ≡⇒↝-refl ⟩
  f i (g i (p , refl _))                                  ≡⟨ cong (_$ f i (g i (p , refl _))) $ sym
                                                             ≡⇒↝-refl ⟩
  ≡⇒↝ _ (refl _) (f i (g i (p , refl _)))                 ≡⟨ cong (λ eq → ≡⇒↝ _ eq (f i (g i (p , refl _)))) $ sym $
                                                             trans (cong (cong Q) sym-refl) $
                                                             cong-refl _ ⟩∎
  ≡⇒↝ _ (cong Q (sym (refl _))) (f i (g i (p , refl _)))  ∎
  where
  l = i ⊔ o ⊔ p ⊔ s ⊔ p′
  r = i ⊔ p ⊔ q ⊔ s ⊔ p′

-- A conversion lemma for Coalgebra.

Coalgebra≃Coalgebra :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Coalgebra C ↝[ i ⊔ s ⊔ p ∣ i ⊔ s ⊔ p ]
  C.Coalgebra (_⇔_.to (Container⇔Container p) C)
Coalgebra≃Coalgebra {s = s} p C {k = k} ext =
  (∃ λ P → P ⇾ ⟦ C ⟧ P)                                   ↝⟨ (∃-cong λ _ →
                                                              ∀-cong (lower-extensionality? k (s ⊔ p) lzero ext) λ _ →
                                                              ∀-cong ext λ _ →
                                                              from-equivalence $ inverse $ ⟦⟧≃⟦⟧ p C _) ⟩□
  (∃ λ P → P ⇾ C.⟦ _⇔_.to (Container⇔Container p) C ⟧ P)  □

-- A conversion lemma for _⇨_.

⇨≃⇨ :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  (X Y : Coalgebra C) →
  (X ⇨ Y) ≃
  (Coalgebra≃Coalgebra p C _ X C.⇨ Coalgebra≃Coalgebra p C _ Y)
⇨≃⇨ {s = s} p C ext (P , f) (Q , g) =
  (∃ λ (h : P ⇾ Q) → g ∘⇾ h ≡ map _ h ∘⇾ f)     ↝⟨ (∃-cong λ h → inverse $ Eq.≃-≡ $
                                                    ∀-cong (lower-extensionality (s ⊔ p) lzero ext) λ _ →
                                                    ∀-cong ext λ _ →
                                                    inverse $ ⟦⟧≃⟦⟧ p C _) ⟩□
  (∃ λ (h : P ⇾ Q) →
     ((Σ-map id uncurry ∘_) ∘ g) ∘⇾ h ≡
     C.map _ h ∘⇾ ((Σ-map id uncurry ∘_) ∘ f))  □

-- A conversion lemma for Final.

Final≃Final :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  (ext : Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p))
  (X : Coalgebra C) →
  Final X ≃ C.Final (_≃_.to (Coalgebra≃Coalgebra p C ext) X)
Final≃Final p C ext′ ext X =
  (∀ Y → Contractible (Y ⇨ X))                              ↝⟨ (Π-cong ext′ (Coalgebra≃Coalgebra p C {k = equivalence} ext) λ Y →
                                                                H-level-cong ext 0 $
                                                                ⇨≃⇨ p C ext Y X) ⟩□
  (∀ Y → Contractible (Y C.⇨ Coalgebra≃Coalgebra p C _ X))  □

-- A conversion lemma for Final′.

Final′≃Final′ :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  (ext : Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p))
  (X : Coalgebra C) →
  Final′ X ≃ C.Final′ (_≃_.to (Coalgebra≃Coalgebra p C ext) X)
Final′≃Final′ p C ext′ ext X =
  (∀ Y → ∃ λ (m : Y   ⇨ X ) → (m′ : Y   ⇨ X ) → proj₁ m ≡ proj₁ m′)  ↝⟨ (Π-cong ext′ (Coalgebra≃Coalgebra p C {k = equivalence} ext) λ Y →
                                                                         Σ-cong (⇨≃⇨ p C ext Y X) λ _ →
                                                                         Π-cong ext (⇨≃⇨ p C ext Y X) λ _ →
                                                                         F.id) ⟩□
  (∀ Y → ∃ λ (m : Y C.⇨ X′) → (m′ : Y C.⇨ X′) → proj₁ m ≡ proj₁ m′)  □
  where
  X′ = _≃_.to (Coalgebra≃Coalgebra p C ext) X

-- A conversion lemma for Final-coalgebra.

Final-coalgebra≃Final-coalgebra :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  Final-coalgebra C ≃
  C.Final-coalgebra (_⇔_.to (Container⇔Container p) C)
Final-coalgebra≃Final-coalgebra p C ext =
  (∃ λ (X :   Coalgebra C ) →   Final X)  ↝⟨ Σ-cong {k₁ = equivalence}
                                               (Coalgebra≃Coalgebra p C ext′)
                                               (Final≃Final p C ext ext′) ⟩□
  (∃ λ (X : C.Coalgebra C′) → C.Final X)  □
  where
  C′   = _⇔_.to (Container⇔Container p) C
  ext′ = lower-extensionality _ lzero ext

-- A conversion lemma for Final-coalgebra′.

Final-coalgebra′≃Final-coalgebra′ :
  ∀ p {I : Type i} (C : Container I s (i ⊔ p)) →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  Final-coalgebra′ C ≃
  C.Final-coalgebra′ (_⇔_.to (Container⇔Container p) C)
Final-coalgebra′≃Final-coalgebra′ p C ext =
  (∃ λ (X :   Coalgebra C ) →   Final′ X)  ↝⟨ Σ-cong {k₁ = equivalence}
                                                (Coalgebra≃Coalgebra p C ext′)
                                                (Final′≃Final′ p C ext ext′) ⟩□
  (∃ λ (X : C.Coalgebra C′) → C.Final′ X)  □
  where
  C′   = _⇔_.to (Container⇔Container p) C
  ext′ = lower-extensionality _ lzero ext

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
import Lvl

-- TODO: Just testing how it goes with creating an axiomatic system
module Geometry.Test (Point : Set(Lvl.𝟎)) where

open import Functional
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
-- open import Structure.Setoid.Uniqueness{Lvl.𝟎}{Lvl.𝟎}{Lvl.𝟎} hiding (Theorems)
open import Structure.Relator.Equivalence{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Relator.Ordering{Lvl.𝟎}{Lvl.𝟎}
-- open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎} hiding (Theorems)

-- A line of infinite length
record Line : Set(Lvl.𝟎) where
  constructor line
  field
    a : Point
    b : Point

-- A line segment of finite length
record LineSegment : Set(Lvl.𝟎) where
  constructor lineSegment
  field
    a : Point
    b : Point

-- A circle
record Circle : Set(Lvl.𝟎) where
  constructor circle
  field
    middle : Point
    outer : Point

record Theory : Set(Lvl.𝐒(Lvl.𝟎)) where
  -- Symbols
  field
    PointOnLine : Point → Line → Set(Lvl.𝟎) -- The point lies on the line
    PointOnLineSegment : Point → LineSegment → Set(Lvl.𝟎) -- The point lies on the line segment
    PointOnCircle : Point → Circle → Set(Lvl.𝟎) -- The point lies on the circle
    _≾_ : LineSegment → LineSegment → Set(Lvl.𝟎) -- Comparison of line length

  _≿_ : LineSegment → LineSegment → Set(Lvl.𝟎) -- Comparison of line length
  _≿_ l₁ l₂ = l₂ ≾ l₁

  _≋_ : LineSegment → LineSegment → Set(Lvl.𝟎) -- Equality of line length
  _≋_ l₁ l₂ = (l₁ ≾ l₂) ∧ (l₁ ≿ l₂)

  -- Axioms
  field
    [≾]-weak-total-order : Weak.TotalOrder(_≾_)(_≋_) -- (_≾_) is a weak total order

    point-on-line-existence : ∀{l : Line} → ∃(p ↦ PointOnLine(p)(l)) -- There is a point on a line
    point1-on-line : ∀{l : Line} → PointOnLine(Line.a(l))(l)
    point2-on-line : ∀{l : Line} → PointOnLine(Line.b(l))(l)

    point-on-lineSegment-existence : ∀{l : LineSegment} → ∃(p ↦ PointOnLineSegment(p)(l)) -- There is a point on a line
    endpoint1-on-lineSegment : ∀{l : LineSegment} → PointOnLineSegment(Line.a(l))(l)
    endpoint2-on-lineSegment : ∀{l : LineSegment} → PointOnLineSegment(Line.b(l))(l)

    point-on-circle-existence : ∀{c : Circle} → ∃(p ↦ PointOnCircle(p)(c)) -- There is a point on a circle
    outer-on-circle : ∀{c : Circle} → PointOnCircle(Circle.outer(c))(c)
    single-point-circle : ∀{p : Point}{x : Point} → PointOnCircle(x) (circle(p)(p)) → (x ≡ p) -- There is only a simgle point on a circle of zero radius

    line-equality : ∀{l : Line}{a : Point}{b : Point} → PointOnLine(a)(l) → PointOnLine(b)(l) → (l ≡ line(a)(b)) -- A line is non-directional
    circle-equality : ∀{c : Circle}{o : Point} → PointOnCircle(o)(c) → (c ≡ circle(Circle.middle(c))(o))
    lineSegment-equality : ∀{a : Point}{b : Point} → (lineSegment(a)(b) ≡ lineSegment(b)(a)) -- A line segment is non-directional

    -- line-intersection : ∀{l₁ : Line}{l₂ : Line} → ∃!(p ↦ PointOnLine(p)(l₁) ∧ PointOnLine(p)(l₂))
    circle-intersection : ∀{a : Point}{b : Point} → ∃(i ↦ PointOnCircle(i)(circle(a)(b)) ∧ PointOnCircle(i)(circle(b)(a))) ∧ ∃(i ↦ PointOnCircle(i)(circle(a)(b)) ∧ PointOnCircle(i)(circle(b)(a)))

module Theorems ⦃ _ : Theory ⦄ where
  open Theory ⦃ ... ⦄

  -- middlepoint : Line → Point
  -- middlepoint(line(a)(b)) =

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Oscar.Data.Permutation where

--open import Data.Permutation public
import Data.Permutation as P
open import Data.Permutation renaming (delete to deleteP; _∘_ to _∘P_; enum to allInj)

open import Oscar.Data.Vec renaming (delete to deleteV; map to mapV)

open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Fin renaming (inject to injectF)

open ≡-Reasoning

open import Data.Permutation.Properties

open import Oscar.Data.Vec.Properties
open import Function

open import Data.Sum
open import Agda.Builtin.Nat

<>-inv : ∀ {n} (ps : Permutation n) i → i ≡ < ps > (< ps ⁻¹ > i)
<>-inv ps i =
  trans
    (sym (id-is-id i))
    (subst (< P.id > _ ≡_)
           (inj-correct (ps ⁻¹) ps i)
           (cong (flip <_> _)
                 (sym (inv-left ps))))

_⋟_÷_ : ∀ {a m n} {A : Set a} → Vec A n → Vec A m → Inj m n → Set a
x ⋟ px ÷ p = ∀ i → lookup i px ≡ lookup (< p > i) x

lookup-ext : ∀ {a n} {A : Set a} {pv₁ pv₂ : Vec A n} → (∀ i → lookup i pv₁ ≡ lookup i pv₂) → pv₁ ≡ pv₂
lookup-ext {pv₁ = []} {[]} x = refl
lookup-ext {pv₁ = x₁ ∷ pv₁} {x₂ ∷ pv₂} x with lookup-ext {pv₁ = pv₁} {pv₂} (x ∘ suc) | x zero
… | refl | refl = refl

injected-inj : ∀ {a n m} {A : Set a} {v : Vec A m} {pv₁ pv₂ : Vec A n} {p : Inj n m} → v ⋟ pv₁ ÷ p → v ⋟ pv₂ ÷ p → pv₁ ≡ pv₂
injected-inj {pv₁ = pv₁} {pv₂} v⋟pv₁÷p v⋟pv₂÷p = lookup-ext foo where
  foo : (i : Fin _) → lookup i pv₁ ≡ lookup i pv₂
  foo i = trans (v⋟pv₁÷p i) (sym (v⋟pv₂÷p i))

permuted-inj : ∀ {a n} {A : Set a} {v : Vec A n} {pv₁ pv₂ : Vec A n} {p : Permutation n} → v ⋟ pv₁ ÷ p → v ⋟ pv₂ ÷ p → pv₁ ≡ pv₂
permuted-inj {pv₁ = pv₁} {pv₂} v⋟pv₁÷p v⋟pv₂÷p = lookup-ext foo where
  foo : (i : Fin _) → lookup i pv₁ ≡ lookup i pv₂
  foo i = trans (v⋟pv₁÷p i) (sym (v⋟pv₂÷p i))

permutedLookup : ∀ {a n} {A : Set a} → Permutation n → Vec A n → Fin n → A
permutedLookup p v = flip lookup v ∘ < p >

inject : ∀ {a n m} {A : Set a} → (p : Inj n m) → (v : Vec A m) → Vec A n
inject p v = tabulate (flip lookup v ∘ < p >)

permute : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) → Vec A n
permute p v = tabulate (flip lookup v ∘ < p >)

inject-correct : ∀ {a n m} {A : Set a} → (p : Inj n m) → (v : Vec A m) →
                  v ⋟ inject p v ÷ p
inject-correct p v = lookup∘tabulate (flip lookup v ∘ < p >)

permute-correct : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) →
                  v ⋟ permute p v ÷ p
permute-correct p v = lookup∘tabulate (flip lookup v ∘ < p >)

Permute : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) →
          ∃ (v ⋟_÷ p)
Permute p v = permute p v , permute-correct p v

_⋟_÷? : ∀ {a m n} {A : Set a} → Vec A n → Vec A m → Set a
_⋟_÷? x px = ∃ (x ⋟ px ÷_)

∈-allInj : ∀ {n m} (i : Inj n m) → i ∈ allInj n m
∈-allInj {zero} [] = here
∈-allInj {suc n} (i ∷ is) = ∈-map₂ _∷_ (∈-allFin i) (∈-allInj is)

tabulate₂ : ∀ {n m a} {A : Set a} → (Inj n m → A) → Vec A (size n m)
tabulate₂ f = mapV f (allInj _ _)

∈-tabulate₂ : ∀ {n m a} {A : Set a} (f : Inj n m → A) i → f i ∈ tabulate₂ f
∈-tabulate₂ f i = ∈-map f (∈-allInj i)

ENUM₂ : ∀ {a n} {A : Set a} → (v : Vec A n) → Vec (∃ (v ⋟_÷?)) (size n n)
ENUM₂ v = tabulate₂ (λ p → permute p v , p , permute-correct p v)

enumᵢ : ∀ {a n m} {A : Set a} → Vec A m → Vec (Vec A n) (size n m)
enumᵢ v = tabulate₂ (flip inject v)

enum₂ : ∀ {a n} {A : Set a} → Vec A n → Vec (Vec A n) (size n n)
enum₂ v = tabulate₂ (flip permute v)

enumᵢ-sound : ∀ {a} {A : Set a} {n m} (x : Vec A m) (px : Vec A n) → px ∈ enumᵢ x → x ⋟ px ÷?
enumᵢ-sound x _ px∈enum₂x with map-∈ px∈enum₂x
enumᵢ-sound x _ _ | p , refl = p , inject-correct p x

enum₂-sound : ∀ {a} {A : Set a} {n} (x px : Vec A n) → px ∈ enum₂ x → x ⋟ px ÷?
enum₂-sound x _ px∈enum₂x with map-∈ px∈enum₂x
enum₂-sound x _ _ | p , refl = p , permute-correct p x

remove-÷-zero : ∀ {n a} {A : Set a} {x : A} {xs : Vec A n} {px : A}
                  {pxs : Vec A n} {ps : Inj n n} →
                (x ∷ xs) ⋟ px ∷ pxs ÷ (zero ∷ ps) →
                xs ⋟ pxs ÷ ps
remove-÷-zero f i = f (suc i)

enumᵢ-complete : ∀ {a} {A : Set a} {n m} (x : Vec A m) (px : Vec A n) → x ⋟ px ÷? → px ∈ enumᵢ x
enumᵢ-complete x px (p , x⋟px÷p) = proof where
  p∈allInj : p ∈ allInj _ _
  p∈allInj = ∈-allInj p
  permutepx∈enum₂x : inject p x ∈ enumᵢ x
  permutepx∈enum₂x = ∈-map (flip inject x) p∈allInj
  x⋟permutepx÷p : x ⋟ inject p x ÷ p
  x⋟permutepx÷p = inject-correct p x
  proof : px ∈ enumᵢ x
  proof = subst (_∈ _) (injected-inj {p = p} x⋟permutepx÷p x⋟px÷p) permutepx∈enum₂x

enum₂-complete : ∀ {a} {A : Set a} {n} (x px : Vec A n) → x ⋟ px ÷? → px ∈ enum₂ x
enum₂-complete x px (p , x⋟px÷p) = proof where
  p∈allInj : p ∈ allInj _ _
  p∈allInj = ∈-allInj p
  permutepx∈enum₂x : permute p x ∈ enum₂ x
  permutepx∈enum₂x = ∈-map (flip permute x) p∈allInj
  x⋟permutepx÷p : x ⋟ permute p x ÷ p
  x⋟permutepx÷p = permute-correct p x
  proof : px ∈ enum₂ x
  proof = subst (_∈ _) (permuted-inj {p = p} x⋟permutepx÷p x⋟px÷p) permutepx∈enum₂x

Enum₂ : ∀ {a n} {A : Set a} → (x : Vec A n) → Σ[ pxs ∈ Vec (Vec A n) (size n n) ] (∀ px → (px ∈ pxs → x ⋟ px ÷?) × (x ⋟ px ÷? → px ∈ pxs))
Enum₂ x = enum₂ x , (λ px → enum₂-sound x px , enum₂-complete x px)

_∃⊎∀_ : ∀ {a} {A : Set a} {l r} (L : A → Set l) (R : A → Set r) {p} (P : A → Set p) → Set _
(L ∃⊎∀ R) P = (∃ λ x → P x × L x) ⊎ (∀ x → P x → R x)

open import Agda.Primitive

stepDecide∃⊎∀ : ∀ {a} {A : Set a} {l r} {L : A → Set l} {R : A → Set r} → (∀ y → L y ⊎ R y) → ∀ {p} (P : A → Set p) →
                ∀ {d} (done : Vec A d) {nd} (not-done : Vec A nd) →
                (∀ y → y ∈ done ⊎ y ∈ not-done → P y) →
                (∀ y → P y → y ∈ done ⊎ y ∈ not-done) →
                (∀ y → y ∈ done → R y) →
                (L ∃⊎∀ R) P
stepDecide∃⊎∀ dec P done {zero} not-done dnd-sound dnd-complete done-R = inj₂ (λ y Py → done-R y (dnd-done y Py)) where
  dnd-done : ∀ y → P y → y ∈ done
  dnd-done y Py with dnd-complete y Py
  dnd-done y Py | inj₁ y∈done = y∈done
  dnd-done y Py | inj₂ ()
stepDecide∃⊎∀ dec P done {suc nd} (step ∷ not-dones) dnd-sound dnd-complete done-R with dec step
… | inj₁ l = inj₁ (step , (dnd-sound step (inj₂ here)) , l)
… | inj₂ r = stepDecide∃⊎∀ dec P (step ∷ done) not-dones stepdnd-sound stepdnd-complete (stepdone-R r) where
  stepdnd-sound : ∀ y → y ∈ step ∷ done ⊎ y ∈ not-dones → P y
  stepdnd-sound _ (inj₁ here) = dnd-sound step (inj₂ here)
  stepdnd-sound y (inj₁ (there y∈done)) = dnd-sound y (inj₁ y∈done)
  stepdnd-sound y (inj₂ y∈not-dones) = dnd-sound y (inj₂ (there y∈not-dones))

  stepdnd-complete : ∀ y → P y → y ∈ step ∷ done ⊎ y ∈ not-dones
  stepdnd-complete y Py with dnd-complete y Py
  stepdnd-complete y Py | inj₁ y∈done = inj₁ (there y∈done)
  stepdnd-complete y Py | inj₂ here = inj₁ here
  stepdnd-complete y Py | inj₂ (there y∈not-dones) = inj₂ y∈not-dones

  stepdone-R : _ → ∀ y → y ∈ step ∷ done → _
  stepdone-R Rstep _ here = Rstep
  stepdone-R Rstep y (there y∈done) = done-R y y∈done

decide∃⊎∀ : ∀ {a} {A : Set a} {l r} {L : A → Set l} {R : A → Set r} → (∀ y → L y ⊎ R y) → ∀ {p} (P : A → Set p) →
            ∀ {nd} (not-done : Vec A nd) →
            (∀ y → y ∈ not-done → P y) →
            (∀ y → P y → y ∈ not-done) →
            (L ∃⊎∀ R) P
decide∃⊎∀ dec P not-done nd-sound nd-complete = stepDecide∃⊎∀ dec P [] not-done []nd-sound []nd-complete (λ {_ ()}) where
  []nd-sound : ∀ y → y ∈ [] ⊎ y ∈ not-done → P y
  []nd-sound y (inj₁ ())
  []nd-sound y (inj₂ y∈not-done) = nd-sound y y∈not-done

  []nd-complete : ∀ y → P y → y ∈ [] ⊎ y ∈ not-done
  []nd-complete y Py = inj₂ (nd-complete y Py)

decidePermutations : ∀ {a n} {A : Set a} {l r} {L : Vec A n → Set l} {R : Vec A n → Set r} → ∀ x → (∀ y → L y ⊎ R y) →
                     (L ∃⊎∀ R) (x ⋟_÷?)
decidePermutations x f = decide∃⊎∀ f _ (enum₂ x) (enum₂-sound x) (enum₂-complete x)

decideInjections : ∀ {a n m} {A : Set a} {l r} {L : Vec A n → Set l} {R : Vec A n → Set r} → ∀ (x : Vec A m) → (∀ y → L y ⊎ R y) →
                     (L ∃⊎∀ R) (x ⋟_÷?)
decideInjections x f = decide∃⊎∀ f _ (enumᵢ x) (enumᵢ-sound x) (enumᵢ-complete x)

-- -- sym-⋟∣ : ∀ {a n} {A : Set a} → (y x : Vec A n) → (p : Permutation n) →
-- --          y ⋟ x ∣ p → x ⋟ y ∣ (p ⁻¹)
-- -- sym-⋟∣ y x ps y⋟x∣p i =
-- --   trans (cong (flip lookup x) {x = i} {y = < ps > (< ps ⁻¹ > i)} (<>-inv ps i)) (sym (y⋟x∣p (< ps ⁻¹ > i)))

-- -- open import Oscar.Data.Vec.Properties

-- -- Permute : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) →
-- --           ∃ λ w → w ⋟ v ∥ p
-- -- Permute [] v = v , λ ()
-- -- Permute p@(p' ∷ ps) v@(v' ∷ vs) =
-- --   let ws , [vs≡ws]ps = Permute ps (deleteV p' v)
-- --       w = lookup p' v ∷ ws
-- --       [v≡w]p : w ⋟ v ∥ p
-- --       [v≡w]p = {!!}
-- --       {-
-- --       [v≡w]p = λ
-- --         { zero → here
-- --         ; (suc f) → there (subst (ws [ f ]=_)
-- --                                  (lookup-delete-thin p' (< ps > f) v)
-- --                                  ([vs≡ws]ps f)) }
-- --       -}
-- --   in
-- --   w , [v≡w]p

-- -- -- permute : ∀ {a n} {A : Set a} → Permutation n → Vec A n → Vec A n
-- -- -- permute p v = proj₁ (Permute p v)

-- -- -- permute-correct : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) → v ⋟ permute p v ∥ p
-- -- -- permute-correct p v = proj₂ (Permute p v)

-- -- -- open import Function

-- -- -- --∈-map-proj₁ : mapV proj₁ (mapV (λ p → F p , G p) xs) ≡ mapV F xs
-- -- -- open import Data.Nat

-- -- -- ∈-enum : ∀ {n m} (i : Inj n m) → i ∈ enum n m
-- -- -- ∈-enum {zero} [] = here
-- -- -- ∈-enum {suc n} (i ∷ is) = ∈-map₂ _∷_ (∈-allFin i) (∈-enum is)

-- -- -- open import Data.Permutation.Properties

-- -- -- [thin]=→delete[]= : ∀ {a n} {A : Set a} {i j} {v : Vec A (suc n)} {x} → v [ thin i j ]= x → deleteV i v [ j ]= x
-- -- -- [thin]=→delete[]= {i = zero} {v = x ∷ v} (there x₂) = x₂
-- -- -- [thin]=→delete[]= {n = zero} {i = suc ()} x₁
-- -- -- [thin]=→delete[]= {n = suc n} {i = suc i} {zero} {x ∷ v} here = here
-- -- -- [thin]=→delete[]= {n = suc n} {i = suc i} {suc j} {x ∷ v} (there v[thinij]=?) = there ([thin]=→delete[]= {i = i} v[thinij]=?)

-- -- -- delete≡Permutation : ∀ {a n} {A : Set a} {v₀ : A} {v₊ : Vec A n} {w : Vec A (suc n)} {p : Permutation (suc n)} →
-- -- --                      (v₀ ∷ v₊) ⋟ w ∥ p →
-- -- --                      v₊ ⋟ deleteV (annihilator p) w ∥ delete (annihilator p) p
-- -- -- delete≡Permutation {v₀ = v₀} {v₊} {w} {p} [v₀∷v₊≡w]p f = [thin]=→delete[]= {i = annihilator p} {j = f} qux where
-- -- --   foo : thin (< p > (annihilator p)) (< delete (annihilator p) p > f) ≡ < p > (thin (annihilator p) f)
-- -- --   foo = inj-thin p (annihilator p) f

-- -- --   foo2 : suc (< delete (annihilator p) p > f) ≡ < p > (thin (annihilator p) f)
-- -- --   foo2 = subst (λ y → thin y (< delete (annihilator p) p > f) ≡ < p > (thin (annihilator p) f)) (ann-correct p) foo

-- -- --   bar : w [ thin (annihilator p) f ]= lookup (< p > (thin (annihilator p) f)) (v₀ ∷ v₊)
-- -- --   bar = [v₀∷v₊≡w]p (thin (annihilator p) f)

-- -- --   qux : w [ thin (annihilator p) f ]= lookup (< delete (annihilator p) p > f) v₊
-- -- --   qux = subst (λ y → w [ thin (annihilator p) f ]= lookup y (v₀ ∷ v₊)) (sym foo2) bar

-- -- -- permute-complete-step : ∀ {a n} {A : Set a} {v₀ : A} {w : Vec A (suc n)} {v₊ : Vec A n} (x : Fin (suc n)) →
-- -- --   w [ x ]= v₀ →
-- -- --   deleteV x w ∈ mapV (flip permute v₊) (enum n n) →
-- -- --   w ∈ mapV (flip permute (v₀ ∷ v₊)) (enum (suc n) (suc n))
-- -- -- permute-complete-step {n = zero} {w = x₃ ∷ []} {[]} zero here here = here
-- -- -- permute-complete-step {n = zero} {w = x₃ ∷ []} {[]} zero x₁ (there ())
-- -- -- permute-complete-step {n = zero} {w = x₃ ∷ []} {[]} (suc ()) x₁ x₂
-- -- -- permute-complete-step {n = suc n} {w = w ∷ ws} x w∷ws[x]=v₀ x₂ = {!!}

-- -- -- permute-lemma : ∀ {a n} {A : Set a} (v w : Vec A n) (p : Permutation n) →
-- -- --   v ⋟ w ∥ p →
-- -- --   w ≡ permute (p ⁻¹) v
-- -- -- permute-lemma v w p x = {!permute-correct p w!}

-- -- -- {-
-- -- -- permute-complete' : ∀ {a n} {A : Set a} (v w : Vec A n) (p : Permutation n) →
-- -- --   v ⋟ w ∥ p →
-- -- --   ∀ {m} {ps : Vec (Permutation n) m} → p ∈ ps →
-- -- --   w ≡ permute p v
-- -- --   w ∈ mapV (flip
-- -- -- -}

-- -- -- permute-complete : ∀ {a n} {A : Set a} (v w : Vec A n) →
-- -- --            v ∃≡Permutation w →
-- -- --            w ∈ mapV (flip permute v) (enum n n)
-- -- -- permute-complete [] [] (p , [v≡w]p) = here
-- -- -- permute-complete {n = suc n} v@(v₀ ∷ v₊) w (p , [v≡w]p) = permute-complete-step (annihilator p) w[ap]=v₀ pc' where
-- -- --   w[ap]=v₀ : w [ annihilator p ]= v₀
-- -- --   w[ap]=v₀ = {![v≡w]p (annihilator p)!}
-- -- --   pc' : deleteV (annihilator p) w ∈ mapV (flip permute v₊) (enum n n)
-- -- --   pc' = permute-complete v₊ (deleteV (annihilator p) w) (delete (annihilator p) p , delete≡Permutation {p = p} [v≡w]p)

-- -- -- EnumPermutations : ∀ {a n} {A : Set a} → (v : Vec A n) →
-- -- --                    Σ (Vec (∃ (v ∃≡Permutation_)) (size n n)) λ ws
-- -- --                    → ∀ w → (v ∃≡Permutation w → w ∈ mapV proj₁ ws)
-- -- -- EnumPermutations {n = n} v = mapV (λ p → permute p v , p , permute-correct p v) (enum n n) , (λ w v∃≡Pw → subst (w ∈_) (map-∘ proj₁ (λ p → permute p v , p , permute-correct p v) (enum n n)) (permute-complete v w v∃≡Pw))

-- -- -- enumPermutations : ∀ {a n} {A : Set a} → Vec A n → Vec (Vec A n) (size n n)
-- -- -- enumPermutations {n = n} xs = mapV (λ p → permute p xs) (enum n n)

-- -- -- tryPermutations : ∀ {a n} {A : Set a} {l r} {L : Vec A n → Set l} {R : Vec A n → Set r} → ∀ x → (f : ∀ y → L y ⊎ R y) → Vec (∃ λ y → x ∃≡Permutation y × L y ⊎ R y) (size n n)
-- -- -- tryPermutations x f = mapV (λ x₁ → x₁ , {!!}) (enumPermutations x)


text:
module Type.Quotient where

open import Logic
open import Relator.Equals
open import Type
open import Lvl

private variable ℓ₁ : Lvl.Level
private variable ℓ₂ : Lvl.Level

data _/_  (T : Type{ℓ₁}) (_≅_ : T → T → Stmt{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
  [_] : T → (T / (_≅_))
  [/]-equiv-to-eq : ∀{x y : T} → (x ≅ y) → ([ x ] ≡ [ y ])
  [/]-uip : ∀{X Y : (T / (_≅_))} → (proof₁ proof₂ : (X ≡ Y)) → (proof₁ ≡ proof₂)

  -- TODO: [/]-eq-to-equiv : (x y : A) → (x ≅ y) ← ([ x ] ≡ [ y ])


text:
module Issue292-27 where

postulate A : Set

data D : Set → Set where
  d₁ : D A
  d₂ : D (A → A)

data P : (B : Set) → B → D B → Set₁ where
  p₁ : (x : A)     → P A       x d₁
  p₂ : (f : A → A) → P (A → A) f d₂

Foo : (x : A) → P A x d₁ → Set₁
Foo x (p₁ .x) = Set

-- Cannot decide whether there should be a case for the constructor
-- p₂, since the unification gets stuck on unifying the inferred
-- indices
--   [A → A, f, d₂]
-- with the expected indices
--   [A, x, d₁]
-- when checking the definition of Foo


text:
{-# OPTIONS --cubical --safe #-}

module Algebra.Construct.Free.Semilattice.FromList where

open import Prelude
open import Algebra.Construct.Free.Semilattice.Definition
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Relation.Unary
open import Data.List
import Data.List.Membership as ℰ
open import Data.Fin using (Fin; fs; f0)
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties

fromList : List A → 𝒦 A
fromList = foldr _∷_ []

∈List⇒∈𝒦 : ∀ xs {x : A} → ∥ x ℰ.∈ xs ∥ → x ∈ fromList xs
∈List⇒∈𝒦 [] ∣x∈xs∣ = ⊥-elim (refute-trunc (λ ()) ∣x∈xs∣)
∈List⇒∈𝒦 (x ∷ xs) ∣x∈xs∣ = do
  (fs n , x∈xs) ← ∣x∈xs∣
    where (f0 , x∈xs) → ∣ inl x∈xs ∣
  ∣ inr (∈List⇒∈𝒦 xs ∣ n , x∈xs ∣) ∣

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- Integers
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies
-- (in particular, not Groupoid). See Integer for more definitions.
-- The definitions below are reexported from Integer.

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

open import Equality

module Integer.Basics
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

import Agda.Builtin.Int

open import Prelude renaming (_+_ to _⊕_)

open import Equality.Decidable-UIP eq
import Nat eq as Nat

-- Integers.

open Agda.Builtin.Int public
  using ()
  hiding (module Int)
  renaming (Int to ℤ; pos to +_; negsuc to -[1+_])

module ℤ where
  open Agda.Builtin.Int.Int public
    using ()
    renaming (pos to +_; negsuc to -[1+_])

private
  variable
    m n : ℕ

-- Turns natural numbers into the corresponding negative integers.

-[_] : ℕ → ℤ
-[ zero  ] = + 0
-[ suc n ] = -[1+ n ]

-- Negation.

infix 8 -_

-_ : ℤ → ℤ
- + n      = -[ n ]
- -[1+ n ] = + suc n

-- A helper function used to implement addition.

+_+-[1+_] : ℕ → ℕ → ℤ
+ m +-[1+ n ] =
  if m Nat.<= n then -[1+ n ∸ m ] else + (m ∸ suc n)

private

  -- An alternative implementation of +_+-[1+_].

  +_+-[1+_]′ : ℕ → ℕ → ℤ
  + zero  +-[1+ n     ]′ = -[1+ n ]
  + suc m +-[1+ zero  ]′ = + m
  + suc m +-[1+ suc n ]′ = + m +-[1+ n ]′

  -- The alternative implementation of +_+-[1+_] is not optimised (it
  -- does not use builtin functions), but it computes in the same way
  -- as +_+-[1+_].

  ++-[1+]≡++-[1+]′ : ∀ m n → + m +-[1+ n ] ≡ + m +-[1+ n ]′
  ++-[1+]≡++-[1+]′ zero    n       = refl _
  ++-[1+]≡++-[1+]′ (suc m) zero    = refl _
  ++-[1+]≡++-[1+]′ (suc m) (suc n) = ++-[1+]≡++-[1+]′ m n

-- Addition.

infixl 6 _+_

_+_ : ℤ → ℤ → ℤ
+ m      + + n      = + (m ⊕ n)
+ m      + -[1+ n ] = + m +-[1+ n ]
-[1+ m ] + + n      = + n +-[1+ m ]
-[1+ m ] + -[1+ n ] = -[1+ suc m ⊕ n ]

-- Subtraction.

infixl 6 _-_

_-_ : ℤ → ℤ → ℤ
i - j = i + - j

-- The +_ constructor is cancellative.

+-cancellative : + m ≡ + n → m ≡ n
+-cancellative = cong f
  where
  f : ℤ → ℕ
  f (+ n)    = n
  f -[1+ n ] = n

-- The -[1+_] constructor is cancellative.

-[1+]-cancellative : -[1+ m ] ≡ -[1+ n ] → m ≡ n
-[1+]-cancellative = cong f
  where
  f : ℤ → ℕ
  f (+ n)    = n
  f -[1+ n ] = n

-- Non-negative integers are not equal to negative integers.

+≢-[1+] : + m ≢ -[1+ n ]
+≢-[1+] +≡- = subst P +≡- tt
  where
  P : ℤ → Type
  P (+ n)    = ⊤
  P -[1+ n ] = ⊥

-- Non-positive integers are not equal to positive integers.

+[1+]≢- : + suc m ≢ -[ n ]
+[1+]≢- {n = zero}  = Nat.0≢+ ∘ sym ∘ +-cancellative
+[1+]≢- {n = suc _} = +≢-[1+]

-- Equality of integers is decidable.

infix 4 _≟_

_≟_ : Decidable-equality ℤ
+ m      ≟ + n      = ⊎-map (cong (+_)) (_∘ +-cancellative) (m Nat.≟ n)
+ m      ≟ -[1+ n ] = no +≢-[1+]
-[1+ m ] ≟ + n      = no (+≢-[1+] ∘ sym)
-[1+ m ] ≟ -[1+ n ] = ⊎-map (cong -[1+_]) (_∘ -[1+]-cancellative)
                        (m Nat.≟ n)

-- The integers form a set.

ℤ-set : Is-set ℤ
ℤ-set = decidable⇒set _≟_

-- Addition is commutative.

+-comm : ∀ i {j} → i + j ≡ j + i
+-comm (+ m)    {j = + _}      = cong (+_) $ Nat.+-comm m
+-comm (+ m)    {j = -[1+ _ ]} = refl _
+-comm -[1+ m ] {j = + _}      = refl _
+-comm -[1+ m ] {j = -[1+ _ ]} = cong (-[1+_] ∘ suc) $ Nat.+-comm m


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Categories.Limits.RightKan where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Limits.Limits

module _ {ℓC ℓC' ℓM ℓM' ℓA ℓA' : Level}
         {C : Category ℓC ℓC'}
         {M : Category ℓM ℓM'}
         {A : Category ℓA ℓA'}
         (limitA : Limits {ℓ-max ℓC' ℓM} {ℓ-max ℓC' ℓM'} A)
         (K : Functor M C)
         (T : Functor M A)
         where

 open Category
 open Functor
 open Cone
 open LimCone

 _↓Diag : ob C → Category (ℓ-max ℓC' ℓM) (ℓ-max ℓC' ℓM')
 ob (x ↓Diag) = Σ[ u ∈ ob M ] C [ x , K .F-ob u ]
 Hom[_,_] (x ↓Diag) (u , f) (v , g) = Σ[ h ∈ M [ u , v ] ] f ⋆⟨ C ⟩ K .F-hom h ≡ g
 id (x ↓Diag) {x = (u , f)} = id M , cong (seq' C f) (F-id K) ∙ ⋆IdR C f
 _⋆_ (x ↓Diag) {x = (u , f)} (h , hComm) (k , kComm) = (h ⋆⟨ M ⟩ k)
                                                     , cong (seq' C f) (F-seq K h k)
                                                     ∙ sym (⋆Assoc C _ _ _)
                                                     ∙ cong (λ l → seq' C l (F-hom K k)) hComm
                                                     ∙ kComm
 ⋆IdL (x ↓Diag) _ = Σ≡Prop (λ _ → isSetHom C _ _) (⋆IdL M _)
 ⋆IdR (x ↓Diag) _ = Σ≡Prop (λ _ → isSetHom C _ _) (⋆IdR M _)
 ⋆Assoc (x ↓Diag) _ _ _ = Σ≡Prop (λ _ → isSetHom C _ _) (⋆Assoc M _ _ _)
 isSetHom (x ↓Diag) = isSetΣSndProp (isSetHom M) λ _ → isSetHom C _ _

 private
  i : (x : ob C) → Functor (x ↓Diag) M
  F-ob (i x) = fst
  F-hom (i x) = fst
  F-id (i x) = refl
  F-seq (i x) _ _ = refl

  j : {x y : ob C} (f : C [ x , y ]) → Functor (y ↓Diag) (x ↓Diag)
  F-ob (j f) (u , g) = u , f ⋆⟨ C ⟩ g
  F-hom (j f) (h , hComm) = h , ⋆Assoc C _ _ _ ∙ cong (seq' C f) hComm
  F-id (j f) = Σ≡Prop (λ _ → isSetHom C _ _) refl
  F-seq (j f) _ _ = Σ≡Prop (λ _ → isSetHom C _ _) refl

  T* : (x : ob C) → Functor (x ↓Diag) A
  T* x = funcComp T (i x)

  RanOb : ob C → ob A
  RanOb x = limitA (x ↓Diag) (T* x) .lim

  RanCone : {x y : ob C} → C [ x , y ] → Cone (T* y) (RanOb x)
  coneOut (RanCone {x = x} f) v = limOut (limitA (x ↓Diag) (T* x)) (j f .F-ob v)
  coneOutCommutes (RanCone {x = x} f) h = limOutCommutes (limitA (x ↓Diag) (T* x)) (j f .F-hom h)

   -- technical lemmas for proving functoriality
  RanConeRefl : ∀ {x} v →
                limOut (limitA (x ↓Diag) (T* x)) v
              ≡ limOut (limitA (x ↓Diag) (T* x)) (j (id C) .F-ob v)
  RanConeRefl {x = x} (v , f) =
              cong (λ p → limOut (limitA (x ↓Diag) (T* x)) (v , p)) (sym (⋆IdL C f))

  RanConeTrans : ∀ {x y z} (f : C [ x , y ]) (g : C [ y , z ]) v →
                 limOut (limitA (x ↓Diag) (T* x)) (j f .F-ob (j g .F-ob v))
               ≡ limOut (limitA (x ↓Diag) (T* x)) (j (f ⋆⟨ C ⟩ g) .F-ob v)
  RanConeTrans {x = x} {y = y} {z = z} f g  (v , h) =
               cong (λ p → limOut (limitA (x ↓Diag) (T* x)) (v , p)) (sym (⋆Assoc C f g h))

 -- the right Kan-extension
 Ran : Functor C A
 F-ob Ran = RanOb
 F-hom Ran {y = y} f = limArrow (limitA (y ↓Diag) (T* y)) _ (RanCone f)
 F-id Ran {x = x} =
  limArrowUnique (limitA (x ↓Diag) (T* x)) _ _ _ (λ v → (⋆IdL A _) ∙ RanConeRefl v)
 F-seq Ran {x = x} {y = y} {z = z} f g =
  limArrowUnique (limitA (z ↓Diag) (T* z)) _ _ _ path
  where
  path : ∀ v →
         (F-hom Ran f) ⋆⟨ A ⟩ (F-hom Ran g) ⋆⟨ A ⟩ (limOut (limitA (z ↓Diag) (T* z)) v)
       ≡ coneOut (RanCone (f ⋆⟨ C ⟩ g)) v
  path v = (F-hom Ran f) ⋆⟨ A ⟩ (F-hom Ran g) ⋆⟨ A ⟩ (limOut (limitA (z ↓Diag) (T* z)) v)
         ≡⟨ ⋆Assoc A _ _ _ ⟩
           (F-hom Ran f) ⋆⟨ A ⟩ ((F-hom Ran g) ⋆⟨ A ⟩ (limOut (limitA (z ↓Diag) (T* z)) v))
         ≡⟨ cong (seq' A (F-hom Ran f)) (limArrowCommutes _ _ _ _) ⟩
           (F-hom Ran f) ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (j g .F-ob v)
         ≡⟨ limArrowCommutes _ _ _ _ ⟩
           limOut (limitA (x ↓Diag) (T* x)) (j f .F-ob (j g .F-ob v))
         ≡⟨ RanConeTrans f g v ⟩
           coneOut (RanCone (f ⋆⟨ C ⟩ g)) v ∎

 open NatTrans
 RanNatTrans : NatTrans (funcComp Ran K) T
 N-ob RanNatTrans u = coneOut (RanCone (id C)) (u , id C)
 N-hom RanNatTrans {x = u} {y = v} f =
     Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ coneOut (RanCone (id C)) (v , id C)
   ≡⟨ cong (λ g → Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ g) (sym (RanConeRefl (v , id C))) ⟩
     Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ limOut (limitA ((K .F-ob v) ↓Diag) (T* (K .F-ob v))) (v , id C)
   ≡⟨ limArrowCommutes _ _ _ _ ⟩
     coneOut (RanCone (K .F-hom f)) (v , id C)
   ≡⟨ cong (λ g → limOut (limitA ((K .F-ob u) ↓Diag) (T* (K .F-ob u))) (v , g))
                         (⋆IdR C (K .F-hom f) ∙ sym (⋆IdL C (K .F-hom f))) ⟩
     coneOut (RanCone (id C)) (v , K .F-hom f)
   ≡⟨ sym (coneOutCommutes (RanCone (id C)) (f , ⋆IdL C _)) ⟩
     coneOut (RanCone (id C)) (u , id C) ⋆⟨ A ⟩ T .F-hom f ∎

 -- TODO: show that this nat. trans. is a "universal arrow" and that is a nat. iso.
 -- if K is full and faithful...

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2012-09-13
module RelevanceSubtyping where

-- this naturally type-checks:
one : {A B : Set} → (.A → B) → A → B
one f x = f x

-- this type-checks because of subtyping
one' : {A B : Set} → (.A → B) → A → B
one' f = f

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
-- also importing warnings from A

import A


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.S1.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.HITs.S1.Base
open import Cubical.HITs.PropositionalTruncation as PropTrunc

isConnectedS¹ : (s : S¹) → ∥ base ≡ s ∥
isConnectedS¹ base = ∣ refl ∣
isConnectedS¹ (loop i) =
  squash ∣ (λ j → loop (i ∧ j)) ∣ ∣ (λ j → loop (i ∨ ~ j)) ∣ i

isGroupoidS¹ : isGroupoid S¹
isGroupoidS¹ s t =
  PropTrunc.rec isPropIsSet
    (λ p →
      subst (λ s → isSet (s ≡ t)) p
        (PropTrunc.rec isPropIsSet
          (λ q → subst (λ t → isSet (base ≡ t)) q isSetΩS¹)
          (isConnectedS¹ t)))
    (isConnectedS¹ s)

toPropElim : ∀ {ℓ} {B : S¹ → Type ℓ} → ((s : S¹) → isProp (B s)) → B base → (s : S¹) → B s
toPropElim {B = B} isprop b base = b
toPropElim {B = B} isprop b (loop i) = hcomp (λ k → λ {(i = i0) → b
                                                     ; (i = i1) → isprop base (subst B (loop) b) b k})
                                      (transp (λ j → B (loop (i ∧ j))) (~ i) b)


text:
{-# OPTIONS --safe #-}
open import Data.List as List hiding ([_])

module JVM.Compiler.Monad (T : Set) (⟨_⇒_⟩ : T → T → List T → Set) (nop : ∀ {τ} → ⟨ τ ⇒ τ ⟩ []) where

open import Level
open import Function using (_∘_)
open import Data.Product hiding (_<*>_)
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Monad
open import Relation.Ternary.Data.ReflexiveTransitive as Star
open import Relation.Ternary.Data.Bigplus as Bigplus

private
  variable
    τ₁ τ₂ τ : T

open import JVM.Model T; open Syntax
open import JVM.Syntax.Bytecode T ⟨_⇒_⟩

open import Relation.Ternary.Monad.Writer intf-rel
open WriterMonad (starMonoid {R = Code}) renaming
  ( Writer to Compiler
  ; execWriter to execCompiler)
  public

-- Output a single, unlabeled instruction
code : ∀[ ⟨ τ₁ ⇒ τ₂ ⟩ ⇒ Down⁻ (Compiler τ₁ τ₂ Emp) ]
code i = tell Star.[ instr (↓ i) ]

-- We can label the start of a compiler computation
attachTo : ∀ {P} → ∀[ Up (One τ₁) ⇒ Compiler τ₁ τ₂ P ─✴ Compiler τ₁ τ₂ P ]
attachTo l = censor (label-start nop ⦇ Bigplus.[ l ] ⦈)

attach : ∀[ Up (One τ₁) ⇒ Compiler τ₁ τ₁ Emp ]
attach l = attachTo l ⟨ ∙-idʳ ⟩ return refl

-- Creating binders is pure in the model by means of hiding
freshLabel : ∀ {ψ} → ε[ Compiler τ τ (Up (Own List.[ ψ ]) ✴ Down (Own List.[ ψ ])) ]
freshLabel = return balance


text:
open import MLib.Prelude.FromStdlib

module MLib.Prelude.TransitiveProver {a p} {A : Set a} (_⇒_ : A → A → Set p) (trans : Transitive _⇒_) where

import MLib.Prelude.DFS as DFS
open import MLib.Prelude.Path

open List using ([]; _∷_)

open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Decidable; IsStrictTotalOrder)

import Data.AVL as AVL

Database : Set (a ⊔ˡ p)
Database = List (∃₂ λ x y → x ⇒ y)

module Search {r} {_<_ : Rel A r} (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
  private
    module DFS′ = DFS _⇒_ isStrictTotalOrder
  open DFS′
  open DFS′ public using (Graph)
  open IsStrictTotalOrder isStrictTotalOrder using (_≟_)

  private
    module Tree = AVL isStrictTotalOrder
    open Tree using (Tree)

  mkGraph : Database → Graph
  mkGraph [] = Tree.empty
  mkGraph ((x , y , p) ∷ ps) = Tree.insertWith x ((y , p) ∷ []) List._++_ (mkGraph ps)

  private
    findPath : Graph → ∀ x y → Maybe (Path _⇒_ x y)
    findPath gr x y = findDest gr {y} (λ v → v ≟ y) x

  tryProve′ : Graph → ∀ x y → Maybe (x ⇒ y)
  tryProve′ gr x y = findPath gr x y >>=ₘ just ∘ transPath trans

  findTransTargets′ : Graph → ∀ x → List (∃ λ y → x ⇒ y)
  findTransTargets′ gr x = allTargetsFrom gr x >>=ₗ λ {(y , c) → return (y , transPath trans c)}

  tryProve : Database → ∀ x y → Maybe (x ⇒ y)
  tryProve = tryProve′ ∘ mkGraph

  findTransTargets : Database → ∀ x → List (∃ λ y → x ⇒ y)
  findTransTargets = findTransTargets′ ∘ mkGraph


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The unit type and the total relation on unit
------------------------------------------------------------------------

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

module Data.Unit.Base where

------------------------------------------------------------------------
-- A unit type defined as a record type

-- Note that the name of this type is "\top", not T.

open import Agda.Builtin.Unit public using (⊤; tt)

record _≤_ (x y : ⊤) : Set where