text:
module Formalization.ClassicalPropositionalLogic.NaturalDeduction where

open import Data.Either as Either using (Left ; Right)
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Functional
import      Lvl
import      Logic.Propositional as Meta
open import Logic
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)
open import Type

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

data _⊢_ {ℓ ℓₚ} {P : Type{ℓₚ}} : Formulas(P){ℓ} → Formula(P) → Stmt{Lvl.𝐒(ℓₚ Lvl.⊔ ℓ)} where
  direct : ∀{Γ} → (Γ ⊆ (Γ ⊢_))

  [⊤]-intro : ∀{Γ} → (Γ ⊢ ⊤)

  [⊥]-intro : ∀{Γ}{φ} → (Γ ⊢ φ) → (Γ ⊢ (¬ φ)) → (Γ ⊢ ⊥)
  [⊥]-elim  : ∀{Γ}{φ} → (Γ ⊢ ⊥) → (Γ ⊢ φ)

  [¬]-intro : ∀{Γ}{φ} → ((Γ ∪ singleton(φ)) ⊢ ⊥) → (Γ ⊢ (¬ φ))
  [¬]-elim  : ∀{Γ}{φ} → ((Γ ∪ singleton(¬ φ)) ⊢ ⊥) → (Γ ⊢ φ)

  [∧]-intro : ∀{Γ}{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ ψ) → (Γ ⊢ (φ ∧ ψ))
  [∧]-elimₗ : ∀{Γ}{φ ψ} → (Γ ⊢ (φ ∧ ψ)) → (Γ ⊢ φ)
  [∧]-elimᵣ : ∀{Γ}{φ ψ} → (Γ ⊢ (φ ∧ ψ)) → (Γ ⊢ ψ)

  [∨]-introₗ : ∀{Γ}{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ∨ ψ))
  [∨]-introᵣ : ∀{Γ}{φ ψ} → (Γ ⊢ ψ) → (Γ ⊢ (φ ∨ ψ))
  [∨]-elim   : ∀{Γ}{φ ψ χ} → ((Γ ∪ singleton(φ)) ⊢ χ) → ((Γ ∪ singleton(ψ)) ⊢ χ) → (Γ ⊢ (φ ∨ ψ)) → (Γ ⊢ χ)

  [⟶]-intro : ∀{Γ}{φ ψ} → ((Γ ∪ singleton(φ)) ⊢ ψ) → (Γ ⊢ (φ ⟶ ψ))
  [⟶]-elim  : ∀{Γ}{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ⟶ ψ)) → (Γ ⊢ ψ)

  [⟷]-intro : ∀{Γ}{φ ψ} → ((Γ ∪ singleton(ψ)) ⊢ φ) → ((Γ ∪ singleton(φ)) ⊢ ψ) → (Γ ⊢ (φ ⟷ ψ))
  [⟷]-elimₗ : ∀{Γ}{φ ψ} → (Γ ⊢ ψ) → (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ φ)
  [⟷]-elimᵣ : ∀{Γ}{φ ψ} → (Γ ⊢ φ) → (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ ψ)

module _ where
  private variable P : Type{ℓₚ}
  private variable Γ Γ₁ Γ₂ : Formulas(P){ℓ}
  private variable φ ψ : Formula(P)

  _⊬_ : Formulas(P){ℓ} → Formula(P) → Stmt
  _⊬_ = Meta.¬_ ∘₂ (_⊢_)

  weaken-union-singleton : (Γ₁ ⊆ Γ₂) → (((Γ₁ ∪ singleton(φ)) ⊢_) ⊆ ((Γ₂ ∪ singleton(φ)) ⊢_))

  weaken : (Γ₁ ⊆ Γ₂) → ((Γ₁ ⊢_) ⊆ (Γ₂ ⊢_))
  weaken Γ₁Γ₂ {φ}        (direct p)         = direct (Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.⊤}       [⊤]-intro          = [⊤]-intro
  weaken Γ₁Γ₂ {.⊥}       ([⊥]-intro  p q)   = [⊥]-intro  (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {φ}        ([⊥]-elim   p)     = [⊥]-elim   (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(¬ _)}   ([¬]-intro  p)     = [¬]-intro  (weaken-union-singleton Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}        ([¬]-elim   p)     = [¬]-elim   (weaken-union-singleton Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∧ _)} ([∧]-intro  p q)   = [∧]-intro  (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {φ}        ([∧]-elimₗ  p)     = [∧]-elimₗ  (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}        ([∧]-elimᵣ  p)     = [∧]-elimᵣ  (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∨ _)} ([∨]-introₗ p)     = [∨]-introₗ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {.(_ ∨ _)} ([∨]-introᵣ p)     = [∨]-introᵣ (weaken Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}        ([∨]-elim   p q r) = [∨]-elim   (weaken-union-singleton Γ₁Γ₂ p) (weaken-union-singleton Γ₁Γ₂ q) (weaken Γ₁Γ₂ r)
  weaken Γ₁Γ₂ {.(_ ⟶ _)} ([⟶]-intro  p)     = [⟶]-intro  (weaken-union-singleton Γ₁Γ₂ p)
  weaken Γ₁Γ₂ {φ}        ([⟶]-elim   p q)   = [⟶]-elim   (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {.(_ ⟷ _)} ([⟷]-intro  p q)   = [⟷]-intro  (weaken-union-singleton Γ₁Γ₂ p) (weaken-union-singleton Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {φ}        ([⟷]-elimₗ  p q)   = [⟷]-elimₗ  (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)
  weaken Γ₁Γ₂ {φ}        ([⟷]-elimᵣ  p q)   = [⟷]-elimᵣ  (weaken Γ₁Γ₂ p) (weaken Γ₁Γ₂ q)

  weaken-union-singleton Γ₁Γ₂ p = weaken (Either.mapLeft Γ₁Γ₂) p

  weaken-union : (Γ₁ ⊢_) ⊆ ((Γ₁ ∪ Γ₂) ⊢_)
  weaken-union = weaken Either.Left

  [⟵]-intro : ((Γ ∪ singleton(φ)) ⊢ ψ) → (Γ ⊢ (ψ ⟵ φ))
  [⟵]-intro = [⟶]-intro

  [⟵]-elim : (Γ ⊢ φ) → (Γ ⊢ (ψ ⟵ φ)) → (Γ ⊢ ψ)
  [⟵]-elim = [⟶]-elim

  [¬¬]-elim : (Γ ⊢ ¬(¬ φ)) → (Γ ⊢ φ)
  [¬¬]-elim nnφ =
    ([¬]-elim
      ([⊥]-intro
        (direct(Right [≡]-intro))
        (weaken-union nnφ)
      )
    )

  [¬¬]-intro : (Γ ⊢ φ) → (Γ ⊢ ¬(¬ φ))
  [¬¬]-intro Γφ =
    ([¬]-intro
      ([⊥]-intro
        (weaken-union Γφ)
        (direct (Right [≡]-intro))
      )
    )

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:
{-# OPTIONS --without-K #-}

open import Base

module Homotopy.Skeleton where

private
  module Graveyard {i} {A B : Set i} {f : A → B} where
    private
      data #skeleton₁ : Set i where
        #point : A → #skeleton₁

    skeleton₁ : Set i
    skeleton₁ = #skeleton₁

    point : A → skeleton₁
    point = #point

    postulate  -- HIT
      link : ∀ a₁ a₂ → f a₁ ≡ f a₂ → point a₁ ≡ point a₂

    skeleton₁-rec : ∀ {l} (P : skeleton₁ → Set l)
      (point* : ∀ a → P (point a))
      (link* : ∀ a₁ a₂ (p : f a₁ ≡ f a₂)
        → transport P (link a₁ a₂ p) (point* a₁) ≡ point* a₂)
      → (x : skeleton₁) → P x
    skeleton₁-rec P point* link* (#point a) = point* a

    postulate  -- HIT
      skeleton₁-β-link : ∀ {l} (P : skeleton₁ → Set l)
        (point* : ∀ a → P (point a))
        (link* : ∀ a₁ a₂ (p : f a₁ ≡ f a₂)
          → transport P (link a₁ a₂ p) (point* a₁) ≡ point* a₂)
        a₁ a₂ (p : f a₁ ≡ f a₂)
        → apd (skeleton₁-rec {l} P point* link*) (link a₁ a₂ p)
        ≡ link* a₁ a₂ p

    skeleton₁-rec-nondep : ∀ {l} (P : Set l) (point* : A → P)
      (link* : ∀ a₁ a₂ → f a₁ ≡ f a₂ → point* a₁ ≡ point* a₂)
      → (skeleton₁ → P)
    skeleton₁-rec-nondep P point* link* (#point a) = point* a

    postulate  -- HIT
      skeleton₁-β-link-nondep : ∀ {l} (P : Set l) (point* : A → P)
        (link* : ∀ a₁ a₂ → f a₁ ≡ f a₂ → point* a₁ ≡ point* a₂)
        a₁ a₂ (p : f a₁ ≡ f a₂)
        → ap (skeleton₁-rec-nondep P point* link*) (link a₁ a₂ p)
        ≡ link* a₁ a₂ p

open Graveyard public hiding (skeleton₁)

module _ {i} {A B : Set i} where
  skeleton₁ : (A → B) → Set i
  skeleton₁ f = Graveyard.skeleton₁ {i} {A} {B} {f}

  skeleton₁-lifted : ∀ {f} → skeleton₁ f → B
  skeleton₁-lifted {f} = skeleton₁-rec-nondep B f (λ _ _ p → p)

ext: agda

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical-compatible --rewriting --local-confluence-check #-}

open import Agda.Primitive using (Level; _⊔_; Setω; lzero; lsuc)

infix 4 _≡_

data _≡_ {ℓ : Level} {A : Set ℓ} (a : A) : A → Set ℓ where
  refl : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

run : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
run refl x = x

ap : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {a₁ a₂} → a₁ ≡ a₂ → f a₁ ≡ f a₂
ap f refl = refl

transport1 : ∀ {a b} {A : Set a} (B : A → Set b) {x y : A} (p : x ≡ y) → B x → B y
transport1 B p = run (ap B p)

ap-const : ∀ {a b} {A : Set a} {B : Set b} (f : B) {a₁ a₂ : A} (p : a₁ ≡ a₂) → ap (\ _ → f) p ≡ refl
ap-const f refl = refl
{-# REWRITE ap-const #-}

ap2 : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : ∀ a → B a → RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → fn a₁ b₁ ≡ fn a₂ b₂
ap2 fn refl refl = refl

transport2 : ∀ {a b rv} {A : Set a} {B : A → Set b} (RV : ∀ a → B a → Set rv) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → RV a₁ b₁  → RV a₂ b₂
transport2 RV pa pb = run (ap2 RV pa pb)

ap2-const : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → ap2 {a} {b} {rv} {A} {B} {RV} (λ _ _ → fn) pa pb ≡ refl
ap2-const fn refl refl = refl
{-# REWRITE ap2-const #-}

ap2-const' : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → ap2 {a} {b} {rv} {A} {B} {RV} (λ _ _ → fn) pa pb ≡ refl
ap2-const' {a} {b} {rv} {A} {B} {RV} fn pa pb = {!ap2 {a} {b} {_} {A} {_} {_} (λ _ _ → fn ≡ fn) pa _!}


text:
module conversion where

open import lib

open import cedille-types
open import ctxt
open import is-free
open import lift
open import rename
open import subst
open import syntax-util
open import general-util
open import to-string

{- Some notes:

   -- hnf{TERM} implements erasure as well as normalization.

   -- hnf{TYPE} does not descend into terms.

   -- definitions are assumed to be in hnf
-}

data unfolding : Set where
  no-unfolding : unfolding
  unfold : (unfold-all : 𝔹) {- if ff we unfold just the head -}
           → (unfold-lift : 𝔹) {- if tt we unfold lifting types -}
           → (dampen-after-head-beta : 𝔹) {- if tt we will not unfold definitions after a head beta reduction -}
           → (erase : 𝔹) -- if tt erase the term as we unfold
           → unfolding

unfolding-get-erased : unfolding → 𝔹
unfolding-get-erased no-unfolding = ff
unfolding-get-erased (unfold _ _ _ e) = e

unfolding-set-erased : unfolding → 𝔹 → unfolding
unfolding-set-erased no-unfolding e = no-unfolding
unfolding-set-erased (unfold b1 b2 b3 _) e = unfold b1 b2 b3 e

unfold-all : unfolding
unfold-all = unfold tt tt ff tt

unfold-head : unfolding
unfold-head = unfold ff tt ff tt

unfold-head-no-lift : unfolding
unfold-head-no-lift = unfold ff ff ff ff

unfold-head-one : unfolding
unfold-head-one = unfold ff tt tt tt

unfold-dampen : (after-head-beta : 𝔹) → unfolding → unfolding
unfold-dampen _ no-unfolding = no-unfolding
unfold-dampen _ (unfold tt b b' e) = unfold tt b b e -- we do not dampen unfolding when unfolding everywhere
unfold-dampen tt (unfold ff b tt e) = no-unfolding
unfold-dampen tt (unfold ff b ff e) = (unfold ff b ff e)
unfold-dampen ff _ = no-unfolding

unfolding-elab : unfolding → unfolding
unfolding-elab no-unfolding = no-unfolding
unfolding-elab (unfold b b' b'' _) = unfold b b' b'' ff

conv-t : Set → Set
conv-t T = ctxt → T → T → 𝔹

{-# TERMINATING #-}

-- main entry point
-- does not assume erased
conv-term : conv-t term
conv-type : conv-t type
conv-kind : conv-t kind

-- assume erased
conv-terme : conv-t term
conv-argse : conv-t (𝕃 term)
conv-typee : conv-t type
conv-kinde : conv-t kind

-- call hnf, then the conv-X-norm functions
conv-term' : conv-t term
conv-type' : conv-t type

hnf : {ed : exprd} → ctxt → (u : unfolding) → ⟦ ed ⟧ → (is-head : 𝔹) → ⟦ ed ⟧

-- assume head normalized inputs
conv-term-norm : conv-t term
conv-type-norm : conv-t type
conv-kind-norm : conv-t kind

hnf-optClass : ctxt → unfolding → optClass → optClass
-- hnf-tk : ctxt → unfolding → tk → tk

-- does not assume erased
conv-tk : conv-t tk
conv-liftingType : conv-t liftingType
conv-optClass : conv-t optClass
-- conv-optType : conv-t optType
conv-tty* : conv-t (𝕃 tty)

-- assume erased
conv-tke : conv-t tk
conv-liftingTypee : conv-t liftingType
conv-optClasse : conv-t optClass
-- -- conv-optTypee : conv-t optType
conv-ttye* : conv-t (𝕃 tty)

conv-term Γ t t' = conv-terme Γ (erase t) (erase t')

conv-terme Γ t t' with decompose-apps t | decompose-apps t'
conv-terme Γ t t' | Var _ x , args | Var _ x' , args' =
  if ctxt-eq-rep Γ x x' && conv-argse Γ args args' then tt else
  conv-term' Γ t t'
conv-terme Γ t t' | _ | _ = conv-term' Γ t t'

conv-argse Γ [] [] = tt
conv-argse Γ (a :: args) (a' :: args') = conv-terme Γ a a' && conv-argse Γ args args'
conv-argse Γ _ _ = ff

conv-type Γ t t' = conv-typee Γ (erase t) (erase t')

conv-typee Γ t t' with decompose-tpapps t | decompose-tpapps t'
conv-typee Γ t t' | TpVar _ x , args | TpVar _ x' , args' =
  if ctxt-eq-rep Γ x x' && conv-tty* Γ args args' then tt else
  conv-type' Γ t t'
conv-typee Γ t t' | _ | _ = conv-type' Γ t t'

conv-kind Γ k k' = conv-kinde Γ (erase k) (erase k')
conv-kinde Γ k k' = conv-kind-norm Γ (hnf Γ unfold-head k tt) (hnf Γ unfold-head k' tt)

conv-term' Γ t t' = conv-term-norm Γ (hnf Γ unfold-head t tt) (hnf Γ unfold-head t' tt)
conv-type' Γ t t' = conv-type-norm Γ (hnf Γ unfold-head t tt) (hnf Γ unfold-head t' tt)

-- is-head is only used in hnf{TYPE}
hnf{TERM} Γ no-unfolding e hd = erase-term e
hnf{TERM} Γ u (Parens _ t _) hd = hnf Γ u t hd
hnf{TERM} Γ u (App t1 Erased t2) hd = hnf Γ u t1 hd
hnf{TERM} Γ u (App t1 NotErased t2) hd with hnf Γ u t1 hd
hnf{TERM} Γ u (App _ NotErased t2) hd | Lam _ _ _ x _ t1 = hnf Γ (unfold-dampen tt u) (subst Γ t2 x t1) hd
hnf{TERM} Γ u (App _ NotErased t2) hd | t1 = App t1 NotErased (hnf Γ (unfold-dampen ff u) t2 hd)
hnf{TERM} Γ u (Lam _ Erased _ _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd with hnf (ctxt-var-decl x Γ) u t hd
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) with x =string x' && ~ (is-free-in skip-erased x t')
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) | tt = t' -- eta-contraction
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) | ff =
  Lam posinfo-gen NotErased posinfo-gen x NoClass (App t' NotErased (Var posinfo-gen x'))
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | t' = Lam posinfo-gen NotErased posinfo-gen x NoClass t'
hnf{TERM} Γ u (Let _ (DefTerm _ x _ t) t') hd = hnf Γ u (subst Γ t x t') hd
hnf{TERM} Γ u (Let _ (DefType _ x _ _) t') hd = hnf (ctxt-var-decl x Γ) u t' hd
hnf{TERM} Γ (unfold _ _ _ _) (Var _ x) hd with ctxt-lookup-term-var-def Γ x
hnf{TERM} Γ (unfold _ _ _ _) (Var _ x) hd | nothing = Var posinfo-gen x
hnf{TERM} Γ (unfold ff _ _ e) (Var _ x) hd | just t = erase-if e t -- definitions should be stored in hnf
hnf{TERM} Γ (unfold tt b b' e) (Var _ x) hd | just t = hnf Γ (unfold tt b b' e) t hd -- this might not be fully normalized, only head-normalized
hnf{TERM} Γ u (AppTp t tp) hd = hnf Γ u t hd
hnf{TERM} Γ u (Sigma _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (Epsilon _ _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (IotaPair _ t1 t2 _ _) hd = hnf Γ u t1 hd
hnf{TERM} Γ u (IotaProj t _ _) hd = hnf Γ u t hd
hnf{TERM} Γ u (Phi _ eq t₁ t₂ _) hd = hnf Γ u t₂ hd
hnf{TERM} Γ u (Rho _ _ _ t _ t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Chi _ T t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Delta _ T t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Theta _ u' t ls) hd = hnf Γ u (lterms-to-term u' t ls) hd
hnf{TERM} Γ u (Beta _ _ (SomeTerm t _)) hd = hnf Γ u t hd
hnf{TERM} Γ u (Beta _ _ NoTerm) hd = id-term
hnf{TERM} Γ u (Open _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u x hd = x

hnf{TYPE} Γ no-unfolding e _ = e
hnf{TYPE} Γ u (TpParens _ t _) hd = hnf Γ u t hd
hnf{TYPE} Γ u (NoSpans t _)  hd = hnf Γ u t hd
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) ff  = TpVar posinfo-gen x
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) tt with ctxt-lookup-type-var-def Γ x
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) tt | just tp = tp
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) tt | nothing = TpVar posinfo-gen x
hnf{TYPE} Γ u (TpAppt tp t) hd with hnf Γ u tp hd
hnf{TYPE} Γ u (TpAppt _ t) hd  | TpLambda _ _ x _ tp = hnf Γ u (subst Γ t x tp) hd
hnf{TYPE} Γ u (TpAppt _ t) hd | tp = TpAppt tp (erase-if (unfolding-get-erased u) t)
hnf{TYPE} Γ u (TpApp tp tp') hd with hnf Γ u tp hd
hnf{TYPE} Γ u (TpApp _ tp') hd | TpLambda _ _ x _ tp = hnf Γ u (subst Γ tp' x tp) hd
hnf{TYPE} Γ u (TpApp _ tp') hd | tp with hnf Γ u tp' hd
hnf{TYPE} Γ u (TpApp _ _) hd | tp | tp' = try-pull-lift-types tp tp'

  {- given (T1 T2), with T1 and T2 types, see if we can pull a lifting operation from the heads of T1 and T2 to
     surround the entire application.  If not, just return (T1 T2). -}
  where try-pull-lift-types : type → type → type
        try-pull-lift-types tp1 tp2 with decompose-tpapps tp1 | decompose-tpapps (hnf Γ u tp2 tt)
        try-pull-lift-types tp1 tp2 | Lft _ _ X t l , args1 | Lft _ _ X' t' l' , args2 =
          if conv-tty* Γ args1 args2 then
            try-pull-term-in Γ t l (length args1) [] []
          else
            TpApp tp1 tp2

          where try-pull-term-in : ctxt → term → liftingType → ℕ → 𝕃 var → 𝕃 liftingType → type
                try-pull-term-in Γ t (LiftParens _ l _) n vars ltps = try-pull-term-in Γ t l n vars ltps
                try-pull-term-in Γ t (LiftArrow _ l) 0 vars ltps =
                  recompose-tpapps
                    (Lft posinfo-gen posinfo-gen X
                      (Lam* vars (hnf Γ no-unfolding (App t NotErased (App* t' (map (λ v → NotErased , mvar v) vars))) tt))
                      (LiftArrow* ltps l) , args1)
                try-pull-term-in Γ (Lam _ _ _ x _ t) (LiftArrow l1 l2) (suc n) vars ltps =
                  try-pull-term-in (ctxt-var-decl x Γ) t l2 n (x :: vars) (l1 :: ltps)
                try-pull-term-in Γ t (LiftArrow l1 l2) (suc n) vars ltps =
                  let x = fresh-var "x" (ctxt-binds-var Γ) empty-renamectxt in
                    try-pull-term-in (ctxt-var-decl x Γ) (App t NotErased (mvar x)) l2 n (x :: vars) (l1 :: ltps)
                try-pull-term-in Γ t l n vars ltps = TpApp tp1 tp2

        try-pull-lift-types tp1 tp2 | _ | _ = TpApp tp1 tp2

hnf{TYPE} Γ u (Abs _ b _ x atk tp) _ with Abs posinfo-gen b posinfo-gen x atk (hnf (ctxt-var-decl x Γ) u tp ff)
hnf{TYPE} Γ u (Abs _ b _ x atk tp) _ | tp' with to-abs tp'
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x atk tt {- x is free in tp -} tp) = Abs posinfo-gen b posinfo-gen x atk tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x (Tkk k) ff tp) = Abs posinfo-gen b posinfo-gen x (Tkk k) tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x (Tkt tp') ff tp) = TpArrow tp' b tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | nothing = tp''
hnf{TYPE} Γ u (TpArrow tp1 arrowtype tp2) _ = TpArrow (hnf Γ u tp1 ff) arrowtype (hnf Γ u tp2 ff)
hnf{TYPE} Γ u (TpEq _ t1 t2 _) _
  = TpEq posinfo-gen (erase t1) (erase t2) posinfo-gen
hnf{TYPE} Γ u (TpLambda _ _ x atk tp) _ =
  TpLambda posinfo-gen posinfo-gen x (hnf Γ u atk ff) (hnf (ctxt-var-decl x Γ) u tp ff)
hnf{TYPE} Γ u @ (unfold b tt b'' b''') (Lft _ _ y t l) _ =
 let t = hnf (ctxt-var-decl y Γ) u t tt in
   do-lift Γ (Lft posinfo-gen posinfo-gen y t l) y l (λ t → hnf{TERM} Γ unfold-head t ff) t
-- We need hnf{TYPE} to preserve types' well-kindedness, so we must check if
-- the defined term is being checked against a type and use chi to make sure
-- that wherever it is substituted, the term will have the same directionality.
-- For example, "[e ◂ {a ≃ b} = ρ e' - β] - A (ρ e - a)", would otherwise
-- head-normalize to A (ρ (ρ e' - β) - a), which wouldn't check because it
-- synthesizes the type of "ρ e' - β" (which in turn fails to synthesize the type
-- of "β"). Similar issues could happen if the term is synthesized and it uses a ρ,
-- and then substitutes into a place where it would be checked against a type.
hnf{TYPE} Γ u (TpLet _ (DefTerm _ x ot t) T) hd =
  hnf Γ u (subst Γ (Chi posinfo-gen ot t) x T) hd
-- Note that if we ever remove the requirement that type-lambdas have a classifier,
-- we would need to introduce a type-level chi to do the same thing as above.
-- Currently, synthesizing or checking a type should not make a difference.
hnf{TYPE} Γ u (TpLet _ (DefType _ x k T) T') hd = hnf Γ u (subst Γ T x T') hd
hnf{TYPE} Γ u x _ = x

hnf{KIND} Γ no-unfolding e hd = e
hnf{KIND} Γ u (KndParens _ k _) hd = hnf Γ u k hd
hnf{KIND} Γ (unfold _ _ _ _) (KndVar _ x ys) _ with ctxt-lookup-kind-var-def Γ x
... | nothing = KndVar posinfo-gen x ys
... | just (ps , k) = fst $ subst-params-args Γ ps ys k {- do-subst ys ps k
  where do-subst : args → params → kind → kind
        do-subst (ArgsCons (TermArg _ t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k = do-subst ys ps (subst Γ t x k)
        do-subst (ArgsCons (TypeArg t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k = do-subst ys ps (subst Γ t x k)
        do-subst _ _ k = k -- should not happen -}

hnf{KIND} Γ u (KndPi _ _ x atk k) hd =
    if is-free-in check-erased x k then
      (KndPi posinfo-gen posinfo-gen x atk k)
    else
      tk-arrow-kind atk k
hnf{KIND} Γ u x hd = x

hnf{LIFTINGTYPE} Γ u x hd = x
hnf{TK} Γ u (Tkk k) _ = Tkk (hnf Γ u k tt)
hnf{TK} Γ u (Tkt tp) _ = Tkt (hnf Γ u tp ff)
hnf{QUALIF} Γ u x hd = x
hnf{ARG} Γ u x hd = x

hnf-optClass Γ u NoClass = NoClass
hnf-optClass Γ u (SomeClass atk) = SomeClass (hnf Γ u atk ff)

{- this function reduces a term to "head-applicative" normal form,
   which avoids unfolding definitions if they would lead to a top-level
   lambda-abstraction or top-level application headed by a variable for which we
   do not have a (global) definition. -}
{-# TERMINATING #-}
hanf : ctxt → (e : 𝔹) → term → term
hanf Γ e t with hnf Γ (unfolding-set-erased unfold-head-one e) t tt
hanf Γ e t | t' with decompose-apps t'
hanf Γ e t | t' | (Var _ x) , [] = t'
hanf Γ e t | t' | (Var _ x) , args with ctxt-lookup-term-var-def Γ x
hanf Γ e t | t' | (Var _ x) , args | nothing = t'
hanf Γ e t | t' | (Var _ x) , args | just _ = hanf Γ e t'
hanf Γ e t | t' | h , args {- h could be a Lambda if args is [] -} = t

-- unfold across the term-type barrier
hnf-term-type : ctxt → (e : 𝔹) → type → type
hnf-term-type Γ e (TpEq _ t1 t2 _) = TpEq posinfo-gen (hanf Γ e t1) (hanf Γ e t2) posinfo-gen
hnf-term-type Γ e (TpAppt tp t) = hnf Γ (unfolding-set-erased unfold-head e) (TpAppt tp (hanf Γ e t)) tt
hnf-term-type Γ e tp = hnf Γ unfold-head tp tt

conv-term-norm Γ (Var _ x) (Var _ x') = ctxt-eq-rep Γ x x'
-- hnf implements erasure for terms, so we can ignore some subterms for App and Lam cases below
conv-term-norm Γ (App t1 m t2) (App t1' m' t2') = conv-term-norm Γ t1 t1' && conv-term Γ t2 t2'
conv-term-norm Γ (Lam _ l _ x oc t) (Lam _ l' _ x' oc' t') = conv-term (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) t t'
conv-term-norm Γ (Hole _) _ = tt
conv-term-norm Γ _ (Hole _) = tt
-- conv-term-norm Γ (Beta _ _ NoTerm) (Beta _ _ NoTerm) = tt
-- conv-term-norm Γ (Beta _ _ (SomeTerm t _)) (Beta _ _ (SomeTerm t' _)) = conv-term Γ t t'
-- conv-term-norm Γ (Beta _ _ _) (Beta _ _ _) = ff
{- it can happen that a term is equal to a lambda abstraction in head-normal form,
   if that lambda-abstraction would eta-contract following some further beta-reductions.
   We implement this here by implicitly eta-expanding the variable and continuing
   the comparison.

   A simple example is

       λ v . t ((λ a . a) v) ≃ t
 -}
conv-term-norm Γ (Lam _ l _ x oc t) t' =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt in
  conv-term (ctxt-rename x x' Γ) t (App t' NotErased (Var posinfo-gen x'))
conv-term-norm Γ t' (Lam _ l _ x oc t) =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt in
  conv-term (ctxt-rename x x' Γ) (App t' NotErased (Var posinfo-gen x')) t
conv-term-norm Γ _ _ = ff

conv-type-norm Γ (TpVar _ x) (TpVar _ x') = ctxt-eq-rep Γ x x'
conv-type-norm Γ (TpApp t1 t2) (TpApp t1' t2') = conv-type-norm Γ t1 t1' && conv-type Γ t2 t2'
conv-type-norm Γ (TpAppt t1 t2) (TpAppt t1' t2') = conv-type-norm Γ t1 t1' && conv-term Γ t2 t2'
conv-type-norm Γ (Abs _ b _ x atk tp) (Abs _ b' _ x' atk' tp') =
  eq-maybeErased b b' && conv-tk Γ atk atk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpArrow tp1 a1 tp2) (TpArrow tp1' a2  tp2') = eq-maybeErased a1 a2 && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (TpArrow tp1 a tp2) (Abs _ b _ _ (Tkt tp1') tp2') = eq-maybeErased a b && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (Abs _ b _ _ (Tkt tp1) tp2) (TpArrow tp1' a tp2') = eq-maybeErased a b && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (Iota _ _ x m tp) (Iota _ _ x' m' tp') =
  conv-type Γ m m' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpEq _ t1 t2 _) (TpEq _ t1' t2' _) = conv-term Γ t1 t1' && conv-term Γ t2 t2'
conv-type-norm Γ (Lft _ _ x t l) (Lft _ _ x' t' l') =
  conv-liftingType Γ l l' && conv-term (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) t t'
conv-type-norm Γ (TpLambda _ _ x atk tp) (TpLambda _ _ x' atk' tp') =
  conv-tk Γ atk atk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ _ _ = ff

{- even though hnf turns Pi-kinds where the variable is not free in the body into arrow kinds,
   we still need to check off-cases, because normalizing the body of a kind could cause the
   bound variable to be erased (hence allowing it to match an arrow kind). -}
conv-kind-norm Γ (KndArrow k k₁) (KndArrow k' k'') = conv-kind Γ k k' && conv-kind Γ k₁ k''
conv-kind-norm Γ (KndArrow k k₁) (KndPi _ _ x (Tkk k') k'') = conv-kind Γ k k' && conv-kind Γ k₁ k''
conv-kind-norm Γ (KndArrow k k₁) _ = ff
conv-kind-norm Γ (KndPi _ _ x (Tkk k₁) k) (KndArrow k' k'') = conv-kind Γ k₁ k' && conv-kind Γ k k''
conv-kind-norm Γ (KndPi _ _ x atk k) (KndPi _ _ x' atk' k'') =
    conv-tk Γ atk atk' && conv-kind (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) k k''
conv-kind-norm Γ (KndPi _ _ x (Tkt t) k) (KndTpArrow t' k'') = conv-type Γ t t' && conv-kind Γ k k''
conv-kind-norm Γ (KndPi _ _ x (Tkt t) k) _ = ff
conv-kind-norm Γ (KndPi _ _ x (Tkk k') k) _ = ff
conv-kind-norm Γ (KndTpArrow t k) (KndTpArrow t' k') = conv-type Γ t t' && conv-kind Γ k k'
conv-kind-norm Γ (KndTpArrow t k) (KndPi _ _ x (Tkt t') k') = conv-type Γ t t' && conv-kind Γ k k'
conv-kind-norm Γ (KndTpArrow t k) _ = ff
conv-kind-norm Γ (Star x) (Star x') = tt
conv-kind-norm Γ (Star x) _ = ff
conv-kind-norm Γ _ _ = ff -- should not happen, since the kinds are in hnf

conv-tk Γ tk tk' = conv-tke Γ (erase-tk tk) (erase-tk tk')

conv-tke Γ (Tkk k) (Tkk k') = conv-kind Γ k k'
conv-tke Γ (Tkt t) (Tkt t') = conv-type Γ t t'
conv-tke Γ _ _ = ff

conv-liftingType Γ l l' = conv-liftingTypee Γ (erase l) (erase l')
conv-liftingTypee Γ l l' = conv-kind Γ (liftingType-to-kind l) (liftingType-to-kind l')

conv-optClass Γ NoClass NoClass = tt
conv-optClass Γ (SomeClass x) (SomeClass x') = conv-tk Γ (erase-tk x) (erase-tk x')
conv-optClass Γ _ _ = ff

conv-optClasse Γ NoClass NoClass = tt
conv-optClasse Γ (SomeClass x) (SomeClass x') = conv-tk Γ x x'
conv-optClasse Γ _ _ = ff

-- conv-optType Γ NoType NoType = tt
-- conv-optType Γ (SomeType x) (SomeType x') = conv-type Γ x x'
-- conv-optType Γ _ _ = ff

conv-tty* Γ [] [] = tt
conv-tty* Γ (tterm t :: args) (tterm t' :: args')
  = conv-term Γ (erase t) (erase t') && conv-tty* Γ args args'
conv-tty* Γ (ttype t :: args) (ttype t' :: args')
  = conv-type Γ (erase t) (erase t') && conv-tty* Γ args args'
conv-tty* Γ _ _ = ff

conv-ttye* Γ [] [] = tt
conv-ttye* Γ (tterm t :: args) (tterm t' :: args') = conv-term Γ t t' && conv-ttye* Γ args args'
conv-ttye* Γ (ttype t :: args) (ttype t' :: args') = conv-type Γ t t' && conv-ttye* Γ args args'
conv-ttye* Γ _ _ = ff

hnf-qualif-term : ctxt → term → term
hnf-qualif-term Γ t = hnf Γ unfold-head (qualif-term Γ t) tt

hnf-qualif-type : ctxt → type → type
hnf-qualif-type Γ t = hnf Γ unfold-head (qualif-type Γ t) tt

hnf-qualif-kind : ctxt → kind → kind
hnf-qualif-kind Γ t = hnf Γ unfold-head (qualif-kind Γ t) tt

ctxt-params-def : params → ctxt → ctxt
ctxt-params-def ps Γ@(mk-ctxt (fn , mn , _ , q) syms i symb-occs d) =
  mk-ctxt (fn , mn , ps' , q) syms i symb-occs d
  where ps' = qualif-params Γ ps

ctxt-kind-def : posinfo → var → params → kind → ctxt → ctxt
ctxt-kind-def pi v ps2 k Γ@(mk-ctxt (fn , mn , ps1 , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps1 , qualif-insert-params q (mn # v) v ps1)
  (trie-insert-append2 syms fn mn v , mn-fn)
  (trie-insert i (mn # v) (kind-def (append-params ps1 $ qualif-params Γ ps2) k' , fn , pi))
  symb-occs
  d
  where
  k' = hnf Γ unfold-head (qualif-kind Γ k) tt

-- assumption: classifier (i.e. kind) already qualified
ctxt-datatype-def : posinfo → var → params → kind → defDatatype → ctxt → ctxt
ctxt-datatype-def pi v pa k dd Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps , q')
  ((trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (datatype-def pa k , fn , pi))
  symb-occs
  (trie-insert d v' dd)
  where
  v' = mn # v
  q' = qualif-insert-params q v' v ps

-- assumption: classifier (i.e. kind) already qualified
ctxt-type-def : posinfo → defScope → opacity → var → type → kind → ctxt → ctxt
ctxt-type-def pi s op v t k Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps , q')
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (type-def (def-params s ps) op t' k , fn , pi))
  symb-occs
  d
  where
  t' = hnf Γ unfold-head (qualif-type Γ t) tt
  v' = if s iff localScope then pi % v else mn # v
  q' = qualif-insert-params q v' v ps

ctxt-const-def : posinfo → var → type → ctxt → ctxt
ctxt-const-def pi c t Γ@(mk-ctxt mod@(fn , mn , ps , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps , q')
  ((trie-insert-append2 syms fn mn c) , mn-fn)
  (trie-insert i c' (const-def t , fn , pi))
  symb-occs
  d
  where
  c' = mn # c
  q' = qualif-insert-params q c' c ps

-- assumption: classifier (i.e. type) already qualified
ctxt-term-def : posinfo → defScope → opacity → var → term → type → ctxt → ctxt
ctxt-term-def pi s op v t tp Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps , q')
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (term-def (def-params s ps) op t' tp , fn , pi))
  symb-occs
  d
  where
  t' = hnf Γ unfold-head (qualif-term Γ t) tt
  v' = if s iff localScope then pi % v else mn # v
  q' = qualif-insert-params q v' v ps

ctxt-term-udef : posinfo → defScope → opacity → var → term → ctxt → ctxt
ctxt-term-udef pi s op v t Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs d) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q v' v ps)
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (term-udef (def-params s ps) op t' , fn , pi))
  symb-occs
  d
  where
  t' = hnf Γ unfold-head (qualif-term Γ t) tt
  v' = if s iff localScope then pi % v else mn # v

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout

module lib.types.Join  where

module _ {i j} (A : Type i) (B : Type j) where

  *-span : Span
  *-span = span A B (A × B) fst snd

  infix 80 _*_

  _*_ : Type _
  _*_ = Pushout *-span

module JoinElim {i j} {A : Type i} {B : Type j} {k} {P : A * B → Type k}
  (left* : (a : A) → P (left a)) (right* : (b : B) → P (right b))
  (glue* : (ab : A × B) → left* (fst ab) == right* (snd ab) [ P ↓ glue ab ])
  = PushoutElim left* right* glue*
open JoinElim public using () renaming (f to Join-elim)

module JoinRec {i j} {A : Type i} {B : Type j} {k} {D : Type k}
  (left* : (a : A) → D) (right* : (b : B) → D)
  (glue* : (ab : A × B) → left* (fst ab) == right* (snd ab))
  = PushoutRec left* right* glue*
open JoinRec public using () renaming (f to Join-rec)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  *-⊙span : ⊙Span
  *-⊙span = ⊙span X Y (X ⊙× Y) ⊙fst ⊙snd

  infix 80 _⊙*_

  _⊙*_ : Ptd _
  _⊙*_ = ⊙Pushout *-⊙span

module _ {i i' j j'} {A : Type i} {A' : Type i'} {B : Type j} {B' : Type j'} where

  equiv-* : A ≃ A' → B ≃ B' → A * B ≃ A' * B'
  equiv-* eqA eqB = equiv to from to-from from-to where
    module To = JoinRec {D = A' * B'} (left ∘ –> eqA) (right ∘ –> eqB) (λ{(a , b) → glue (–> eqA a , –> eqB b)})
    module From = JoinRec {D = A * B} (left ∘ <– eqA) (right ∘ <– eqB) (λ{(a , b) → glue (<– eqA a , <– eqB b)})

    to : A * B → A' * B'
    to = To.f

    from : A' * B' → A * B
    from = From.f

    to-from : ∀ y → to (from y) == y
    to-from = Join-elim (ap left ∘ <–-inv-r eqA) (ap right ∘ <–-inv-r eqB) to-from-glue where
      to-from-glue : ∀ (ab : A' × B')
        → ap left (<–-inv-r eqA (fst ab)) == ap right (<–-inv-r eqB (snd ab)) [ (λ y → to (from y) == y) ↓ glue ab ]
      to-from-glue (a , b) = ↓-app=idf-in $
        ap left (<–-inv-r eqA a) ∙' glue (a , b)
          =⟨ htpy-natural'-app=cst (λ a → glue (a , b)) (<–-inv-r eqA a) ⟩
        glue (–> eqA (<– eqA a) , b)
          =⟨ ! $ htpy-natural-cst=app (λ b → glue (–> eqA (<– eqA a) , b)) (<–-inv-r eqB b) ⟩
        glue (–> eqA (<– eqA a) , –> eqB (<– eqB b)) ∙ ap right (<–-inv-r eqB b)
          =⟨ ! $ To.glue-β (<– eqA a , <– eqB b) |in-ctx (_∙ ap right (<–-inv-r eqB b)) ⟩
        ap to (glue (<– eqA a , <– eqB b)) ∙ ap right (<–-inv-r eqB b)
          =⟨ ! $ From.glue-β (a , b) |in-ctx (λ p → ap to p ∙ ap right (<–-inv-r eqB b)) ⟩
        ap to (ap from (glue (a , b))) ∙ ap right (<–-inv-r eqB b)
          =⟨ ! $ ap-∘ to from (glue (a , b)) |in-ctx (_∙ ap right (<–-inv-r eqB b)) ⟩
        ap (to ∘ from) (glue (a , b)) ∙ ap right (<–-inv-r eqB b)
          ∎

    from-to : ∀ x → from (to x) == x
    from-to = Join-elim (ap left ∘ <–-inv-l eqA) (ap right ∘ <–-inv-l eqB) from-to-glue where
      from-to-glue : ∀ (ab : A × B)
        → ap left (<–-inv-l eqA (fst ab)) == ap right (<–-inv-l eqB (snd ab)) [ (λ x → from (to x) == x) ↓ glue ab ]
      from-to-glue (a , b) = ↓-app=idf-in $
        ap left (<–-inv-l eqA a) ∙' glue (a , b)
          =⟨ htpy-natural'-app=cst (λ a → glue (a , b)) (<–-inv-l eqA a) ⟩
        glue (<– eqA (–> eqA a) , b)
          =⟨ ! $ htpy-natural-cst=app (λ b → glue (<– eqA (–> eqA a) , b)) (<–-inv-l eqB b) ⟩
        glue (<– eqA (–> eqA a) , <– eqB (–> eqB b)) ∙ ap right (<–-inv-l eqB b)
          =⟨ ! $ From.glue-β (–> eqA a , –> eqB b) |in-ctx (_∙ ap right (<–-inv-l eqB b)) ⟩
        ap from (glue (–> eqA a , –> eqB b)) ∙ ap right (<–-inv-l eqB b)
          =⟨ ! $ To.glue-β (a , b) |in-ctx (λ p → ap from p ∙ ap right (<–-inv-l eqB b)) ⟩
        ap from (ap to (glue (a , b))) ∙ ap right (<–-inv-l eqB b)
          =⟨ ! $ ap-∘ from to (glue (a , b)) |in-ctx (_∙ ap right (<–-inv-l eqB b)) ⟩
        ap (from ∘ to) (glue (a , b)) ∙ ap right (<–-inv-l eqB b)
          ∎

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'} where

  ⊙equiv-⊙* : X ⊙≃ X' → Y ⊙≃ Y' → X ⊙* Y ⊙≃ X' ⊙* Y'
  ⊙equiv-⊙* ⊙eqX ⊙eqY = ⊙≃-in (equiv-* (fst (⊙≃-out ⊙eqX)) (fst (⊙≃-out ⊙eqY))) (ap left (snd (⊙≃-out ⊙eqX)))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module plfa.part1.Induction where

import Relation.Binary.PropositionalEquality as Eq

open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)

  -- A relation is said to be a congruence for
  -- a given function if it is preserved by applying that function

  -- If e is evidence that x ≡ y,
  -- then cong f e is evidence that f x ≡ f y,
  -- for any function f

  -- The correspondence between proof by induction and
  -- definition by recursion is one of the most appealing
  -- aspects of Agda

  -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
  --           ^- suc               ^- (m + n) + p ≡ m + (n + p)
  -- ----------------------------------------------------------- (=> implies)
  -- suc ((m + n) + p) ≡ suc (m + (n + p))

  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))

  -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
  -- cong f refl = refl

  ≡⟨⟩
    suc m + (n + p)
  ∎

+-assoc-2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p)
+-assoc-2 n p =
  begin
    (2 + n) + p
  ≡⟨⟩
    suc (1 + n) + p
  ≡⟨⟩
    suc ((1 + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc (1 + (n + p))
  ≡⟨⟩
    2 + (n + p)
  ∎
  where
  +-assoc-1 : ∀ (n p : ℕ) -> (1 + n) + p ≡ 1 + (n + p)
  +-assoc-1 n p =
    begin
      (1 + n) + p
    ≡⟨⟩
      suc (0 + n) + p
    ≡⟨⟩
      suc ((0 + n) + p)
    ≡⟨ cong suc (+-assoc-0 n p) ⟩
      suc (0 + (n + p))
    ≡⟨⟩
      1 + (n + p)
    ∎
    where
      +-assoc-0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p)
      +-assoc-0 n p =
        begin
          (0 + n) + p
        ≡⟨⟩
          n + p
        ≡⟨⟩
          0 + (n + p)
        ∎

+-identityᴿ : ∀ (m : ℕ) → m + zero ≡ m
+-identityᴿ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityᴿ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityᴿ m) ⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityᴿ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

-- Rearranging

-- We can apply associativity to
-- rearrange parentheses however we like

+-rearrange
  : ∀ (m n p q : ℕ)
  → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q))

  ≡⟨ cong (m +_) (sym (+-assoc n p q)) ⟩
    m + ((n + p) + q)

  -- +-assoc : (m + n) + p ≡ m + (n + p)
  -- sym (+-assoc) : m + (n + p) ≡ (m + n) + p

  ≡⟨ sym (+-assoc m (n + p) q) ⟩
    (m + (n + p)) + q
  ∎

-- Associativity with rewrite

-- Rewriting avoids not only chains of
-- equations but also the need to invoke cong

+-assoc' : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc' zero n p                           = refl
+-assoc' (suc m) n p rewrite +-assoc' m n p = refl

+-identity' : ∀ (n : ℕ) → n + zero ≡ n
+-identity' zero = refl
+-identity' (suc n) rewrite +-identity' n = refl

+-suc' : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc' zero n = refl
+-suc' (suc m) n rewrite +-suc' m n = refl

+-comm' : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm' m zero rewrite +-identity' m = refl
+-comm' m (suc n) rewrite +-suc' m n | +-comm' m n = refl

-- Building proofs interactively

+-assoc'' : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc'' zero n p = refl
+-assoc'' (suc m) n p rewrite +-assoc'' m n p = refl

-- Exercise

-- Note:
-- sym -- rewrites the left side of the Goal

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap zero n p = refl
+-swap (suc m) n p rewrite
    +-assoc'' m n p
  | +-suc n (m + p)
  | +-swap m n p
  = refl

-- (suc m + n) * p ≡ suc m * p + n * p
-- p + (m * p + n * p) ≡ p + m * p + n * p

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite
    *-distrib-+ m n p
  | sym (+-assoc p (m * p) (n * p))
  = refl

-- (n + m * n) * p ≡ n * p + m * (n * p)

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite
    *-distrib-+ n (m * n) p
  | *-assoc m n p
  = refl

max_stars_repo_name: vyorkin/plfa

max_issues_repo_name: vyorkin/plfa

max_forks_repo_name: vyorkin/plfa


text:
module ProjectingRecordMeta where

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

-- Andreas, Feb/Apr 2011
record Prod (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

open Prod public

testProj : {A B : Set}(y z : Prod A B) ->
  let X : Prod A B
      X = _       -- Solution: fst y , snd z
  in (C : Set) -> (fst X == fst y -> snd X == snd z -> C) -> C
testProj y z C k = k refl refl
-- ok, Agda handles projections properly during unification

testProj' : {A B : Set}(y z : Prod A B) ->
  let X : Prod A B
      X = _       -- Solution: fst y , snd z
  in Prod (fst X == fst y) (snd X == snd z)
testProj' y z = refl , refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- "Finite" sets indexed on coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Cofin where

open import Coinduction
open import Data.Conat as Conat using (Coℕ; suc; ∞ℕ)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)

------------------------------------------------------------------------
-- The type

-- Note that Cofin ∞ℕ is /not/ finite. Note also that this is not a
-- coinductive type, but it is indexed on a coinductive type.

data Cofin : Coℕ → Set where
  zero : ∀ {n} → Cofin (suc n)
  suc  : ∀ {n} (i : Cofin (♭ n)) → Cofin (suc n)

------------------------------------------------------------------------
-- Some operations

fromℕ : ℕ → Cofin ∞ℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

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

fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n)
fromFin zero    = zero
fromFin (suc i) = suc (fromFin i)

toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n
toFin zero    ()
toFin (suc n) zero    = zero
toFin (suc n) (suc i) = suc (toFin n i)


text:
module Pi1r where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Groupoid

-- infix  2  _∎       -- equational reasoning for paths
-- infixr 2  _≡⟨_⟩_   -- equational reasoning for paths
infixr 10 _◎_
infixr 30 _⟷_

------------------------------------------------------------------------------
-- Level 0:
-- Types at this level are just plain sets with no interesting path structure.
-- The path structure is defined at levels 1 and beyond.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Programs
-- We use pointed types; programs map a pointed type to another
-- In other words, each program takes one particular value to another; if we
-- want to work on another value, we generally use another program

record U• : Set where
  constructor •[_,_]
  field
    ∣_∣ : U
    • : ⟦ ∣_∣ ⟧

open U•

-- examples of plain types, values, and pointed types

ONE• : U•
ONE• = •[ ONE , tt ]

BOOL : U
BOOL = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

TRUE : ⟦ BOOL ⟧
TRUE = inj₁ tt

FALSE : ⟦ BOOL ⟧
FALSE = inj₂ tt

BOOL•F : U•
BOOL•F = •[ BOOL , FALSE ]

BOOL•T : U•
BOOL•T = •[ BOOL , TRUE ]

-- The actual programs are the commutative semiring isomorphisms between
-- pointed types.

data _⟷_ : U• → U• → Set where
  unite₊  : ∀ {t v} → •[ PLUS ZERO t , inj₂ v ] ⟷ •[ t , v ]
  uniti₊  : ∀ {t v} → •[ t , v ] ⟷ •[ PLUS ZERO t , inj₂ v ]
  swap1₊  : ∀ {t₁ t₂ v₁} →
            •[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₁ , inj₂ v₁ ]
  swap2₊  : ∀ {t₁ t₂ v₂} →
            •[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₂ t₁ , inj₁ v₂ ]
  assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → •[ TIMES ONE t , (tt , v) ] ⟷ •[ t , v ]
  uniti⋆  : ∀ {t v} → •[ t , v ] ⟷ •[ TIMES ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} →
              •[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⟷
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⟷
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            •[ TIMES ZERO t , (absurd , v) ] ⟷ •[ ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
  id⟷    : ∀ {t v} → •[ t , v ] ⟷ •[ t , v ]
  _◎_    : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} → (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) →
           (•[ t₂ , v₂ ] ⟷ •[ t₃ , v₃ ]) →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ])
  _⊕1_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₃ t₄ , inj₁ v₃ ])
  _⊕2_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
          (•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₃ t₄ , (v₃ , v₄) ])
  loop : ∀ {t v} → •[ t , v ] ⟷ •[ t , v ]

! : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊ = uniti₊
! uniti₊ = unite₊
! swap1₊ = swap2₊
! swap2₊ = swap1₊
! assocl1₊ = assocr1₊
! assocl2₊ = assocr2₊
! assocl3₊ = assocr3₊
! assocr1₊ = assocl1₊
! assocr2₊ = assocl2₊
! assocr3₊ = assocl3₊
! unite⋆ = uniti⋆
! uniti⋆ = unite⋆
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! distz = factorz
! factorz = distz
! dist1 = factor1
! dist2 = factor2
! factor1 = dist1
! factor2 = dist2
! id⟷ = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕1 c₂) = ! c₁ ⊕1 ! c₂
! (c₁ ⊕2 c₂) = ! c₁ ⊕2 ! c₂
! (c₁ ⊗ c₂) = ! c₁ ⊗ ! c₂
! loop = loop

-- example programs

NOT•T : •[ BOOL , TRUE ] ⟷ •[ BOOL , FALSE ]
NOT•T = swap1₊

NOT•F : •[ BOOL , FALSE ] ⟷ •[ BOOL , TRUE ]
NOT•F = swap2₊

CNOT•Fx : {b : ⟦ BOOL ⟧} →
          •[ BOOL² , (FALSE , b) ] ⟷ •[ BOOL² , (FALSE , b) ]
CNOT•Fx = dist2 ◎ ((id⟷ ⊗ NOT•F) ⊕2 id⟷) ◎ factor2

CNOT•TF : •[ BOOL² , (TRUE , FALSE) ] ⟷ •[ BOOL² , (TRUE , TRUE) ]
CNOT•TF = dist1 ◎
          ((id⟷ ⊗ NOT•F) ⊕1 (id⟷ {TIMES ONE BOOL} {(tt , TRUE)})) ◎
          factor1

CNOT•TT : •[ BOOL² , (TRUE , TRUE) ] ⟷ •[ BOOL² , (TRUE , FALSE) ]
CNOT•TT = dist1 ◎
          ((id⟷ ⊗ NOT•T) ⊕1 (id⟷ {TIMES ONE BOOL} {(tt , TRUE)})) ◎
          factor1

-- The evaluation of a program is not done in order to figure out the output
-- value. Both the input and output values are encoded in the type of the
-- program; what the evaluation does is follow the path to constructively
-- reach the ouput value from the input value. Even though programs of the
-- same pointed types are, by definition, observationally equivalent, they
-- may follow different paths. At this point, we simply declare that all such
-- programs are "the same." At the next level, we will weaken this "path
-- irrelevant" equivalence and reason about which paths can be equated to
-- other paths via 2paths etc.

-- Even though individual types are sets, the universe of types is a
-- groupoid. The objects of this groupoid are the pointed types; the
-- morphisms are the programs; and the equivalence of programs is the
-- degenerate observational equivalence that equates every two programs that
-- are extensionally equivalent.

_obs≅_ : {t₁ t₂ : U•} → (c₁ c₂ : t₁ ⟷ t₂) → Set
c₁ obs≅ c₂ = ⊤

UG : 1Groupoid
UG = record
       { set = U•
       ; _↝_ = _⟷_
       ; _≈_ = _obs≅_
       ; id = id⟷
       ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
       ; _⁻¹ = !
       ; lneutr = λ _ → tt
       ; rneutr = λ _ → tt
       ; assoc = λ _ _ _ → tt
       ; equiv = record { refl = tt
                        ; sym = λ _ → tt
                        ; trans = λ _ _ → tt
                        }
       ; linv = λ _ → tt
       ; rinv = λ _ → tt
       ; ∘-resp-≈ = λ _ _ → tt
       }

------------------------------------------------------------------------------
-- Level 1:
-- Types are sets of paths. The paths are defined at the previous level
-- (level 0). At level 1, there is no interesting 2path structure. From
-- the perspective of level 0, we have points with non-trivial paths between
-- them, i.e., we have a groupoid. The paths cross type boundaries, i.e., we
-- have heterogeneous equality

-- types

data 1U : Set where
  1ZERO  : 1U              -- empty set of paths
  1ONE   : 1U              -- a trivial path
  1PLUS  : 1U → 1U → 1U      -- disjoint union of paths
  1TIMES : 1U → 1U → 1U      -- pairs of paths
  PATH  : (t₁ t₂ : U•) → 1U -- level 0 paths between values

-- values

data Path (t₁ t₂ : U•) : Set where
  path : (c : t₁ ⟷ t₂) → Path t₁ t₂

1⟦_⟧ : 1U → Set
1⟦ 1ZERO ⟧             = ⊥
1⟦ 1ONE ⟧              = ⊤
1⟦ 1PLUS t₁ t₂ ⟧       = 1⟦ t₁ ⟧ ⊎ 1⟦ t₂ ⟧
1⟦ 1TIMES t₁ t₂ ⟧      = 1⟦ t₁ ⟧ × 1⟦ t₂ ⟧
1⟦ PATH t₁ t₂ ⟧ = Path t₁ t₂

-- examples

T⟷F : Set
T⟷F = Path BOOL•T BOOL•F

F⟷T : Set
F⟷T = Path BOOL•F BOOL•T

-- all the following are paths from T to F; we will show below that they
-- are equivalent using 2paths

p₁ p₂ p₃ p₄ p₅ : T⟷F
p₁ = path NOT•T
p₂ = path (id⟷ ◎ NOT•T)
p₃ = path (NOT•T ◎ NOT•F ◎ NOT•T)
p₄ = path (NOT•T ◎ id⟷)
p₅ = path (uniti⋆ ◎ swap⋆ ◎ (NOT•T ⊗ id⟷) ◎ swap⋆ ◎ unite⋆)

p₆ : (T⟷F × T⟷F) ⊎ F⟷T
p₆ = inj₁ (p₁ , p₂)

-- Programs map paths to paths. We also use pointed types.

record 1U• : Set where
  constructor 1•[_,_]
  field
    1∣_∣ : 1U
    1• : 1⟦ 1∣_∣ ⟧

open 1U•

data _⇔_ : 1U• → 1U• → Set where
  unite₊  : ∀ {t v} → 1•[ 1PLUS 1ZERO t , inj₂ v ] ⇔ 1•[ t , v ]
  uniti₊  : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ 1PLUS 1ZERO t , inj₂ v ]
  swap1₊  : ∀ {t₁ t₂ v₁} →
            1•[ 1PLUS t₁ t₂ , inj₁ v₁ ] ⇔ 1•[ 1PLUS t₂ t₁ , inj₂ v₁ ]
  swap2₊  : ∀ {t₁ t₂ v₂} →
            1•[ 1PLUS t₁ t₂ , inj₂ v₂ ] ⇔ 1•[ 1PLUS t₂ t₁ , inj₁ v₂ ]
  assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₁ v₁ ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → 1•[ 1TIMES 1ONE t , (tt , v) ] ⇔ 1•[ t , v ]
  uniti⋆  : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ 1TIMES 1ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} →
              1•[ 1TIMES t₁ t₂ , (v₁ , v₂) ] ⇔ 1•[ 1TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            1•[ 1TIMES t₁ (1TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⇔
            1•[ 1TIMES (1TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            1•[ 1TIMES (1TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⇔
            1•[ 1TIMES t₁ (1TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            1•[ 1TIMES 1ZERO t , (absurd , v) ] ⇔ 1•[ 1ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            1•[ 1ZERO , absurd ] ⇔ 1•[ 1TIMES 1ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⇔
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⇔
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⇔
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⇔
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
  id⇔    : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ t , v ]
  _◎_    : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} → (1•[ t₁ , v₁ ] ⇔ 1•[ t₂ , v₂ ]) →
           (1•[ t₂ , v₂ ] ⇔ 1•[ t₃ , v₃ ]) →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ])
  _⊕1_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ]) → (1•[ t₂ , v₂ ] ⇔ 1•[ t₄ , v₄ ]) →
           (1•[ 1PLUS t₁ t₂ , inj₁ v₁ ] ⇔ 1•[ 1PLUS t₃ t₄ , inj₁ v₃ ])
  _⊕2_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ]) → (1•[ t₂ , v₂ ] ⇔ 1•[ t₄ , v₄ ]) →
           (1•[ 1PLUS t₁ t₂ , inj₂ v₂ ] ⇔ 1•[ 1PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ]) → (1•[ t₂ , v₂ ] ⇔ 1•[ t₄ , v₄ ]) →
          (1•[ 1TIMES t₁ t₂ , (v₁ , v₂) ] ⇔ 1•[ 1TIMES t₃ t₄ , (v₃ , v₄) ])
  lidl : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path (id⟷ ◎ c) ] ⇔ 1•[ PATH t₁ t₂ , path c ]
  lidr : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path c ] ⇔ 1•[ PATH t₁ t₂ , path (id⟷ ◎ c) ]
  ridl : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path (c ◎ id⟷) ] ⇔ 1•[ PATH t₁ t₂ , path c ]
  ridr : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path c ] ⇔ 1•[ PATH t₁ t₂ , path (c ◎ id⟷) ]
  assocl : ∀ {t₁ t₂ t₃ t₄}  →
          {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          1•[ PATH t₁ t₄ , path (c₁ ◎ (c₂ ◎ c₃)) ] ⇔
          1•[ PATH t₁ t₄ , path ((c₁ ◎ c₂) ◎ c₃) ]
  assocr : ∀ {t₁ t₂ t₃ t₄}  →
          {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          1•[ PATH t₁ t₄ , path ((c₁ ◎ c₂) ◎ c₃) ] ⇔
          1•[ PATH t₁ t₄ , path (c₁ ◎ (c₂ ◎ c₃)) ]
  unit₊l : ∀ {t v} →
          1•[ PATH (•[ PLUS ZERO t , inj₂ v ]) (•[ PLUS ZERO t , inj₂ v ]) ,
          path (unite₊ ◎ uniti₊) ] ⇔
          1•[ PATH (•[ PLUS ZERO t , inj₂ v ]) (•[ PLUS ZERO t , inj₂ v ]) ,
          path id⟷ ]
  unit₊r : ∀ {t v} →
          1•[ PATH (•[ PLUS ZERO t , inj₂ v ]) (•[ PLUS ZERO t , inj₂ v ]) ,
          path id⟷ ] ⇔
          1•[ PATH (•[ PLUS ZERO t , inj₂ v ]) (•[ PLUS ZERO t , inj₂ v ]) ,
          path (unite₊ ◎ uniti₊) ]
  resp◎   : ∀ {t₁ t₂ t₃} →
           {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₁ ⟷ t₂} {c₄ : t₂ ⟷ t₃} →
           (1•[ PATH t₁ t₂ , path c₁ ] ⇔ 1•[ PATH t₁ t₂ , path c₃ ]) →
           (1•[ PATH t₂ t₃ , path c₂ ] ⇔ 1•[ PATH t₂ t₃ , path c₄ ]) →
           1•[ PATH t₁ t₃ , path (c₁ ◎ c₂) ] ⇔ 1•[ PATH t₁ t₃ , path (c₃ ◎ c₄) ]

1! : {t₁ t₂ : 1U•} → (t₁ ⇔ t₂) → (t₂ ⇔ t₁)
1! unite₊ = uniti₊
1! uniti₊ = unite₊
1! swap1₊ = swap2₊
1! swap2₊ = swap1₊
1! assocl1₊ = assocr1₊
1! assocl2₊ = assocr2₊
1! assocl3₊ = assocr3₊
1! assocr1₊ = assocl1₊
1! assocr2₊ = assocl2₊
1! assocr3₊ = assocl3₊
1! unite⋆ = uniti⋆
1! uniti⋆ = unite⋆
1! swap⋆ = swap⋆
1! assocl⋆ = assocr⋆
1! assocr⋆ = assocl⋆
1! distz = factorz
1! factorz = distz
1! dist1 = factor1
1! dist2 = factor2
1! factor1 = dist1
1! factor2 = dist2
1! id⇔ = id⇔
1! (c₁ ◎ c₂) = 1! c₂ ◎ 1! c₁
1! (c₁ ⊕1 c₂) = 1! c₁ ⊕1 1! c₂
1! (c₁ ⊕2 c₂) = 1! c₁ ⊕2 1! c₂
1! (c₁ ⊗ c₂) = 1! c₁ ⊗ 1! c₂
1! (resp◎ c₁ c₂) = resp◎ (1! c₁) (1! c₂)
1! ridl = ridr
1! ridr = ridl
1! lidl = lidr
1! lidr = lidl
1! assocl = assocr
1! assocr = assocl
1! unit₊l = unit₊r
1! unit₊r = unit₊l

1!≡ : {t₁ t₂ : 1U•} → (c : t₁ ⇔ t₂) → 1! (1! c) ≡ c
1!≡ unite₊ = refl
1!≡ uniti₊ = refl
1!≡ swap1₊ = refl
1!≡ swap2₊ = refl
1!≡ assocl1₊ = refl
1!≡ assocl2₊ = refl
1!≡ assocl3₊ = refl
1!≡ assocr1₊ = refl
1!≡ assocr2₊ = refl
1!≡ assocr3₊ = refl
1!≡ unite⋆ = refl
1!≡ uniti⋆ = refl
1!≡ swap⋆ = refl
1!≡ assocl⋆ = refl
1!≡ assocr⋆ = refl
1!≡ distz = refl
1!≡ factorz = refl
1!≡ dist1 = refl
1!≡ dist2 = refl
1!≡ factor1 = refl
1!≡ factor2 = refl
1!≡ id⇔ = refl
1!≡ (c₁ ◎ c₂) = cong₂ (λ c₁ c₂ → c₁ ◎ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ (c₁ ⊕1 c₂) = cong₂ (λ c₁ c₂ → c₁ ⊕1 c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ (c₁ ⊕2 c₂) = cong₂ (λ c₁ c₂ → c₁ ⊕2 c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ (c₁ ⊗ c₂) = cong₂ (λ c₁ c₂ → c₁ ⊗ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ lidl = refl
1!≡ lidr = refl
1!≡ ridl = refl
1!≡ ridr = refl
1!≡ (resp◎ c₁ c₂) = cong₂ (λ c₁ c₂ → resp◎ c₁ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ assocl = refl
1!≡ assocr = refl
1!≡ unit₊l = refl
1!≡ unit₊r = refl

-- sane syntax

α₁ : 1•[ PATH BOOL•T BOOL•F , p₁ ] ⇔ 1•[ PATH BOOL•T BOOL•F , p₁ ]
α₁ = id⇔

α₂ : 1•[ PATH BOOL•T BOOL•F , p₁ ] ⇔ 1•[ PATH BOOL•T BOOL•F , p₂ ]
α₂ = lidr

{--
_≡⟨_⟩_ : {t₁ t₂ : U•} (c₁ : t₁ ⟷ t₂) {c₂ : t₁ ⟷ t₂} {c₃ : t₁ ⟷ t₂} →
         (2•[ PATH c₁ , path c₁ ] ⇔ 2•[ PATH c₂ , path c₂ ]) →
         (2•[ PATH c₂ , path c₂ ] ⇔ 2•[ PATH c₃ , path c₃ ]) →
         (2•[ PATH c₁ , path c₁ ] ⇔ 2•[ PATH c₃ , path c₃ ])
_ ≡⟨ α ⟩ β = α ◎ β

_∎ : {t₁ t₂ : U•} → (c : t₁ ⟷ t₂) →
     2•[ PATH c , path c ] ⇔ 2•[ PATH c , path c ]
_∎ c = id⟷
--}

-- example programs

-- level 0 is a groupoid with a non-trivial path equivalence the various inv*
-- rules are not justified by the groupoid proof; they are justified by the
-- need for computational rules. So it is important to have not just a
-- groupoid structure but a groupoid structure that we can compute with. So
-- if we say that we want p ◎ p⁻¹ to be id, we must have computational rules
-- that allow us to derive this for any path p, and similarly for all the
-- other groupoid rules. (cf. The canonicity for 2D type theory by Licata and
-- Harper)

linv : {t₁ t₂ : U•} → (c : t₁ ⟷ t₂) →
       1•[ PATH t₁ t₁ , path (c ◎ ! c) ] ⇔ 1•[ PATH t₁ t₁ , path id⟷ ]
linv unite₊ = unit₊l
linv uniti₊ = {!!}
linv swap1₊ = {!!}
linv swap2₊ = {!!}
linv assocl1₊ = {!!}
linv assocl2₊ = {!!}
linv assocl3₊ = {!!}
linv assocr1₊ = {!!}
linv assocr2₊ = {!!}
linv assocr3₊ = {!!}
linv unite⋆ = {!!}
linv uniti⋆ = {!!}
linv swap⋆ = {!!}
linv assocl⋆ = {!!}
linv assocr⋆ = {!!}
linv distz = {!!}
linv factorz = {!!}
linv dist1 = {!!}
linv dist2 = {!!}
linv factor1 = {!!}
linv factor2 = {!!}
linv id⟷ = {!!}
linv (c ◎ c₁) = {!!}
linv (c ⊕1 c₁) = {!!}
linv (c ⊕2 c₁) = {!!}
linv (c ⊗ c₁) = {!!}
linv loop = {!!}

G : 1Groupoid
G = record
        { set = U•
        ; _↝_ = _⟷_
        ; _≈_ = λ {t₁} {t₂} c₀ c₁ →
                1•[ PATH t₁ t₂ , path c₀ ] ⇔ 1•[ PATH t₁ t₂ , path c₁ ]
        ; id = id⟷
        ; _∘_ = λ c₀ c₁ → c₁ ◎ c₀
        ; _⁻¹ = !
        ; lneutr = λ _ → ridl
        ; rneutr = λ _ → lidl
        ; assoc = λ _ _ _ → assocl
        ; equiv = record { refl = id⇔
                                ; sym = λ c → 1! c
                                ; trans = λ c₀ c₁ → c₀ ◎ c₁ }
        ; linv = λ {t₁} {t₂} c → linv c
        ; rinv = λ {t₁} {t₂} c → {!!}
        ; ∘-resp-≈ = λ f⟷h g⟷i → resp◎ g⟷i f⟷h
        }

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

-- A Categorical WeakInverse induces an Adjoint Equivalence

module Categories.Category.Equivalence.Properties where

open import Level

open import Data.Product using (Σ-syntax; _,_; proj₁)

open import Categories.Adjoint.Equivalence using (⊣Equivalence)
open import Categories.Adjoint
open import Categories.Adjoint.TwoSided using (_⊣⊢_; withZig)
open import Categories.Category
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
open import Categories.Morphism
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties using ([_]-resp-Iso)
open import Categories.NaturalTransformation using (ntHelper; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃
  using (NaturalIsomorphism ; unitorˡ; unitorʳ; associator; _ⓘᵥ_; _ⓘˡ_; _ⓘʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso)

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

module _ {F : Functor C D} {G : Functor D C} (W : WeakInverse F G) where
  open WeakInverse W

  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  -- adjoint equivalence
  F⊣⊢G : F ⊣⊢ G
  F⊣⊢G = withZig record
    { unit   = ≃.sym G∘F≈id
    ; counit =
      let open D
          open HomReasoning
          open MR D
          open MP D
      in record
        { F⇒G = ntHelper record
          { η       = λ X → F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
          ; commute = λ {X Y} f → begin
            (F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ Y))) ∘ F.F₁ (G.F₁ f)
              ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G.F₁ f))) ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X)))
              ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y) C.∘ G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G.F₁ f)) ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G.F₁ f C.∘ G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η Y ∘ (F.F₁ (G.F₁ f) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute f) Equiv.refl ⟩
            (f ∘ F∘G≈id.⇒.η X) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ assoc ⟩
            f ∘ F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ∎
          }
        ; F⇐G = ntHelper record
          { η       = λ X → (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
          ; commute = λ {X Y} f → begin
            ((F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F∘G≈id.⇐.η Y) ∘ f
              ≈⟨ pullʳ (F∘G≈id.⇐.commute f) ⟩
            (F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F.F₁ (G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ center (⟺ F.homomorphism) ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y) C.∘ G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇐.commute (G.F₁ f)) ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G.F₁ (F.F₁ (G.F₁ f)) C.∘ G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute _) Equiv.refl ⟩
            (F.F₁ (G.F₁ f) ∘ F∘G≈id.⇒.η (F.F₀ (G.F₀ X))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ center Equiv.refl ⟩
            F.F₁ (G.F₁ f) ∘ (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ∎
          }
        ; iso = λ X → Iso-∘ (Iso-∘ (Iso-swap (F∘G≈id.iso _)) ([ F ]-resp-Iso (G∘F≈id.iso _)))
                            (F∘G≈id.iso X)
        }
    ; zig    = λ {A} →
      let open D
          open HomReasoning
          open MR D
      in begin
      (F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ (F.F₀ A))))
        ∘ F.F₁ (G∘F≈id.⇐.η A)
        ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G∘F≈id.⇐.η A))) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘
        F.F₁ (G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A)) C.∘ G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G∘F≈id.⇐.η A)) ⟩∘⟨refl ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇐.η A C.∘ G∘F≈id.⇒.η A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl⟩∘⟨ elimˡ ((F.F-resp-≈ (G∘F≈id.iso.isoˡ _)) ○ F.identity) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ F∘G≈id.iso.isoʳ _ ⟩
      id
        ∎
    }

  module F⊣⊢G = _⊣⊢_ F⊣⊢G

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (SE : StrongEquivalence C D) where
  open StrongEquivalence SE

  C≅D : ⊣Equivalence C D
  C≅D = record
    { L    = F
    ; R    = G
    ; L⊣⊢R = F⊣⊢G weak-inverse
    }

  module C≅D = ⊣Equivalence C≅D

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F ⊣ G) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  open Adjoint F⊣G

  -- If the unit and the counit of an adjuction are pointwise isomorphisms, then they form an equivalence of categories.
  pointwise-iso-equivalence : (∀ X → Σ[ f ∈ D [ X , F.F₀ (G.F₀ X) ] ] Iso D (counit.η X) f) → (∀ X → Σ[ f ∈ C [  G.F₀ (F.F₀ X) , X ] ] Iso C (unit.η X) f) → WeakInverse F G
  pointwise-iso-equivalence counit-iso unit-iso = record
    { F∘G≈id =
      let iso X =
            let (to , is-iso) = counit-iso X
            in record { from = counit.η X ; to = to ; iso = is-iso }
      in pointwise-iso iso counit.commute
    ; G∘F≈id =
      let iso X =
            let (to , is-iso) = unit-iso X
            in record { from = unit.η X ; to = to ; iso = is-iso }
      in ≃.sym (pointwise-iso iso unit.commute)
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2019-08-08, issue #3972 (and #3967)

-- In the presence of an unreachable clause, the serializer crashed on a unsolve meta.

-- It seems this issue was fixed along #3966: only the ranges of unreachable clauses
-- are now serialized.

open import Agda.Builtin.Equality public

postulate
  List : Set → Set

data Coo {A} (xs : List A) : Set where
  coo : Coo xs → Coo xs

test : {A : Set} (xs : List A) (z : Coo xs) → Set₁
test xs z = cs xs z refl
  where
  cs : (xs : List _)  -- filling this meta _=A removes the internal error
       (z : Coo xs)
       (eq : xs ≡ xs)
       → Set₁
  cs xs (coo z) refl = Set
  cs xs (coo z) eq = Set  -- unreachable

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --type-in-type #-}
module functors where
open import prelude

record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where
  constructor 𝒾:_▸:_𝒾▸:_▸𝒾:
  infixl 8 _▸_
  field
    𝒾 : ∀ {x} → 𝒞[ x , x ]
    _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ]
    𝒾▸ : ∀ {x y} (f : 𝒞[ x , y ]) → (𝒾 ▸ f) ≡ f
    ▸𝒾 : ∀ {x y} (f : 𝒞[ x , y ]) → (f ▸ 𝒾) ≡ f
open Category ⦃...⦄ public

record Functor {A : Set} {𝒜[_,_] : A → A → Set}
               {B : Set} {ℬ[_,_] : B → B → Set}
               (f : A → B) : Set where
  constructor φ:_𝒾:_▸:
  field
    ⦃ cat₁ ⦄ : Category {A} 𝒜[_,_]
    ⦃ cat₂ ⦄ : Category {B} ℬ[_,_]
    φ : ∀ {a b} → 𝒜[ a , b ] → ℬ[ f a , f b ]
    functor-id : ∀ {a} → φ {a} 𝒾 ≡ 𝒾
    functor-comp : ∀ {A B C} → (f : 𝒜[ A , B ]) (g : 𝒜[ B , C ])
                 → φ (f ▸ g) ≡ φ f ▸ φ g
open Functor ⦃...⦄ public

record Nat {A : Set} {𝒜[_,_] : A → A → Set}
           {B : Set} {ℬ[_,_] : B → B → Set}
           {F : A → B} {G : A → B}
           (α : (x : A) → ℬ[ F x , G x ]) : Set where
  field
    overlap ⦃ fun₁ ⦄ : Functor {A} {𝒜[_,_]} {B} {ℬ[_,_]} F
    overlap ⦃ fun₂ ⦄ : Functor {A} {𝒜[_,_]} {B} {ℬ[_,_]} G
    nat : ∀ {x y : A} (f : 𝒜[ x , y ]) → let _▹_ = _▸_ ⦃ cat₂ ⦄
                                          in φ f ▹ α y ≡ α x ▹ φ f

module _ {A : Set} {𝒜[_,_] : A → A → Set}  where
    instance
        id-functor : ⦃ Category 𝒜[_,_] ⦄ → Functor id
        id-functor = φ: id
                     𝒾: refl
                     ▸: λ f g → refl
    record Monad (f : A → A) : Set where
      field
        ⦃ functor ⦄ : Functor {_} {𝒜[_,_]} {_} {𝒜[_,_]} f
        η : ∀ {a} → 𝒜[ a , f a ]
        μ : ∀ {a} → 𝒜[ f (f a) , f a ]
    open Monad ⦃...⦄ public

{-
    record Lift[_⇒_] (pre post : (Set → Set) → Set) (t : (Set → Set) → Set → Set) : Set where
      field
        ⦃ lifted ⦄ : ∀ {f} → post (t f)
        lift : {f : Set → Set} {a : Set} → ⦃ pre f ⦄ → f a → t f a
    open Lift[_⇒_] ⦃...⦄ public
-}

Cat[_,_] : Set → Set → Set
Cat[ a , b ] = a → b

instance
  Cat-cat : Category Cat[_,_]
  Cat-cat = record { 𝒾 = id ; _▸_ = λ f g → g ∘ f ; 𝒾▸ = λ _ → refl; ▸𝒾 = λ _ → refl}
instance
  ≡-cat : ∀ {A} → Category {A} (λ a b → a ≡ b)
  𝒾 {{≡-cat}} = refl
  _▸_ {{≡-cat}} = trans
  𝒾▸ {{≡-cat}} _ = refl
  ▸𝒾 {{≡-cat}} x≡y rewrite x≡y = refl
instance
    ×-cat : ∀ {A 𝒜[_,_]} ⦃ 𝒜 : Category {A} 𝒜[_,_] ⦄
              {B ℬ[_,_]} ⦃ ℬ : Category {B} ℬ[_,_] ⦄
          → Category {A × B} (λ (a , b) (a′ , b′) → 𝒜[ a , a′ ] × ℬ[ b , b′ ])
    𝒾 {{×-cat}} = 𝒾 , 𝒾
    _▸_ {{×-cat}} (f , f′ ) ( g , g′ ) = f ▸ g , f′ ▸ g′
    𝒾▸ {{×-cat}} (f , g) = 𝒾▸ f ×⁼ 𝒾▸ g
    ▸𝒾 {{×-cat}} (f , g) = ▸𝒾 f ×⁼ ▸𝒾 g

data _ᵒᵖ {A : Set} (𝒜 : A → A → Set) : A → A → Set where
  _ᵗ : ∀ {y x} → 𝒜(y )( x) → (𝒜 ᵒᵖ)(x )( y)

instance
    op-cat  : {A : Set} {𝒜[_,_] : A → A → Set} ⦃ 𝒜 : Category {A} 𝒜[_,_] ⦄
            → Category (𝒜[_,_] ᵒᵖ)
    𝒾 {{op-cat}}  = 𝒾 ᵗ
    _▸_ {{op-cat}} (f ᵗ) (g ᵗ) = (g ▸ f) ᵗ
    𝒾▸ {{op-cat}} (f ᵗ) = _ᵗ ⟨$⟩ ▸𝒾 f
    ▸𝒾 {{op-cat}} (f ᵗ) = _ᵗ ⟨$⟩ 𝒾▸ f

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Neutral {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Symmetry

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Neutral reflexive types are reducible.
neu : ∀ {l Γ A} (neA : Neutral A)
    → Γ ⊢ A
    → Γ ⊢ A ~ A ∷ U
    → Γ ⊩⟨ l ⟩ A
neu neA A A~A = ne′ _ (idRed:*: A) neA A~A

  -- Helper function for reducible neutral equality of a specific type of derivation.
neuEq′ : ∀ {l Γ A B} ([A] : Γ ⊩⟨ l ⟩ne A)
         (neA : Neutral A)
         (neB : Neutral B)
       → Γ ⊢ A → Γ ⊢ B
       → Γ ⊢ A ~ B ∷ U
       → Γ ⊩⟨ l ⟩ A ≡ B / ne-intr [A]
neuEq′ (noemb (ne K [ ⊢A , ⊢B , D ] neK K≡K)) neA neB A B A~B =
  let A≡K = whnfRed* D (ne neA)
  in  ιx (ne₌ _ (idRed:*: B) neB (PE.subst (λ x → _ ⊢ x ~ _ ∷ _) A≡K A~B))
neuEq′ (emb 0<1 x) neA neB A B A~B  = ιx (neuEq′ x neA neB A B A~B)

-- Neutrally equal types are of reducible equality.
neuEq : ∀ {l Γ A B} ([A] : Γ ⊩⟨ l ⟩ A)
        (neA : Neutral A)
        (neB : Neutral B)
      → Γ ⊢ A → Γ ⊢ B
      → Γ ⊢ A ~ B ∷ U
      → Γ ⊩⟨ l ⟩ A ≡ B / [A]
neuEq [A] neA neB A B A~B =
  irrelevanceEq (ne-intr (ne-elim neA [A]))
                [A]
                (neuEq′ (ne-elim neA [A]) neA neB A B A~B)

mutual
  -- Neutral reflexive terms are reducible.
  neuTerm : ∀ {l Γ A n} ([A] : Γ ⊩⟨ l ⟩ A) (neN : Neutral n)
          → Γ ⊢ n ∷ A
          → Γ ⊢ n ~ n ∷ A
          → Γ ⊩⟨ l ⟩ n ∷ A / [A]
  neuTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) neN n n~n =
    Uₜ _ (idRedTerm:*: n) (ne neN) (~-to-≅ₜ n~n) (neu neN (univ n) n~n)
  neuTerm (ℕᵣ [ ⊢A , ⊢B , D ]) neN n n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in ιx (ℕₜ _ (idRedTerm:*: (conv n A≡ℕ)) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′)))
  neuTerm (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in ιx (neₜ _ (idRedTerm:*: (conv n A≡K)) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K)))
  neuTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (idRedTerm:*: (conv n A≡ΠFG)) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b
                            (ρn ∘ⱼ a)
                            (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                            (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))
  neuTerm (emb′ 0<1 x) neN n n~n = ιx (neuTerm x neN n n~n)

  -- Neutrally equal terms are of reducible equality.
  neuEqTerm : ∀ {l Γ A n n′} ([A] : Γ ⊩⟨ l ⟩ A)
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ n  ∷ A
            → Γ ⊢ n′ ∷ A
            → Γ ⊢ n ~ n′ ∷ A
            → Γ ⊩⟨ l ⟩ n ≡ n′ ∷ A / [A]
  neuEqTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) neN neN′ n n′ n~n′ =
    let [n]  = neu neN  (univ n) (~-trans n~n′ (~-sym n~n′))
        [n′] = neu neN′ (univ n′) (~-trans (~-sym n~n′) n~n′)
    in  Uₜ₌ _ _ (idRedTerm:*: n) (idRedTerm:*: n′) (ne neN) (ne neN′)
            (~-to-≅ₜ n~n′) [n] [n′] (neuEq [n] neN neN′ (univ n) (univ n′) n~n′)
  neuEqTerm (ℕᵣ [ ⊢A , ⊢B , D ]) neN neN′ n n′ n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in ιx (ℕₜ₌ _ _ (idRedTerm:*: (conv n A≡ℕ)) (idRedTerm:*: (conv n′ A≡ℕ))
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁)))
  neuEqTerm (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in ιx (neₜ₌ _ _ (idRedTerm:*: (conv n A≡K)) (idRedTerm:*: (conv n′ A≡K))
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K)))
  neuEqTerm (Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let [ΠFG] = Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (idRedTerm:*: (conv n A≡ΠFG)) (idRedTerm:*: (conv n′ A≡ΠFG))
            (ne neN) (ne neN′) n≡n′
            (neuTerm [ΠFG] neN n n~n) (neuTerm [ΠFG] neN′ n′ n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = wkTerm [ρ] ⊢Δ n
                   ρn′ = wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a))
  neuEqTerm (emb′ 0<1 x) neN neN′ n n′ n~n′ = ιx (neuEqTerm x neN neN′ n n′ n~n′)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

-- Define all the permutations that occur in Pi
-- These are defined by transport, using univalence

module Permutation where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open import Data.Nat            using    (_+_;_*_)
open import Data.Fin            using    (Fin)
open import Relation.Binary     using    (Setoid)
open import Function.Equality   using    (_⟨$⟩_)

open import Equiv using (_≃_; id≃; sym≃; trans≃; _●_)
open import ConcretePermutation
open import ConcretePermutationProperties
open import SEquivSCPermEquiv
open import FinEquivTypeEquiv using (module PlusE; module TimesE)
open import EquivEquiv

open import Proofs using (
  -- FiniteFunctions
  finext
  )

infixr 5 _●p_

infix 8 _⊎p_
infixr 7 _×p_

------------------------------------------------------------------------------

-- useful short-hands; these should all be moved elsewhere.
e⇒p : ∀ {m n} → (Fin m ≃ Fin n) → CPerm m n
e⇒p e = _≃S_.g univalence ⟨$⟩ e

p⇒e : ∀ {m n} → CPerm m n → (Fin m ≃ Fin n)
p⇒e p = _≃S_.f univalence ⟨$⟩ p

αu : ∀ {m n} → {e f : Fin m ≃ Fin n} → e ≋ f → p⇒e (e⇒p e) ≋ f
αu e≋f = _≃S_.α univalence e≋f

βu : ∀ {m n} → {p q : CPerm m n} → p ≡ q → e⇒p (p⇒e p) ≡ q
βu p≡q = _≃S_.β univalence p≡q

α₁ : ∀ {m n} → {e : Fin m ≃ Fin n} → p⇒e (e⇒p e) ≋ e
α₁ {e = e} = αu (id≋ {x = e}) -- Agda can infer here, but this helps later?

-- inside an e⇒p, we can freely replace equivalences
-- this expresses the fundamental property that equivalent equivalences
-- map to THE SAME permutation.
≋⇒≡ : ∀ {m n} → {e₁ e₂ : Fin m ≃ Fin n} → e₁ ≋ e₂ → e⇒p e₁ ≡ e⇒p e₂
≋⇒≡ {e₁} {e₂} (eq fwd bwd) = p≡ (finext bwd)

-- combination of above, where we use αu on left/right of ●
right-α-over-● : ∀ {m n o} → (e₁ : Fin n ≃ Fin o) → (e₂ : Fin m ≃ Fin n) →
    (e₁ ● (p⇒e (e⇒p e₂))) ≋ (e₁ ● e₂)
right-α-over-● e₁ e₂ = (id≋ {x = e₁}) ◎ (αu {e = e₂} id≋)

left-α-over-● : ∀ {m n o} → (e₁ : Fin n ≃ Fin o) → (e₂ : Fin m ≃ Fin n) →
    ((p⇒e (e⇒p e₁)) ● e₂) ≋ (e₁ ● e₂)
left-α-over-● e₁ e₂ = (αu {e = e₁} id≋) ◎ (id≋ {x = e₂})

------------------------------------------------------------------------------
-- zero permutation
0p : CPerm 0 0
0p = e⇒p (id≃ {A = Fin 0})

-- identity permutation
idp : ∀ {n} → CPerm n n
idp {n} = e⇒p (id≃ {A = Fin n})

-- disjoint union
_⊎p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ + n₁) (m₂ + n₂)
p₁ ⊎p p₂ = e⇒p ((p⇒e p₁) +F (p⇒e p₂))
  where open PlusE

-- cartesian product
_×p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ * n₁) (m₂ * n₂)
p₁ ×p p₂ = e⇒p ((p⇒e p₁) *F (p⇒e p₂))
  where open TimesE

-- symmetry
symp : ∀ {m n} → CPerm m n → CPerm n m
symp p = e⇒p (sym≃ (p⇒e p))

-- transitivity; note the 'transposition' of the arguments!
_●p_ : ∀ {m₁ m₂ m₃} → CPerm m₂ m₁ → CPerm m₃ m₂ → CPerm m₃ m₁
p₁ ●p p₂ = e⇒p ((p⇒e p₁) ● (p⇒e p₂))


text:
module PreludeShow where
import RTP -- magic module

import AlonzoPrelude as Prelude
open import PreludeNat
open import PreludeString
import PreludeList
open import PreludeBool

open Prelude
-- open Data.Integer, using (Int, pos, neg)
open PreludeList hiding (_++_)

showInt : Int -> String
showInt = RTP.primShowInt

showNat : Nat -> String
showNat n = showInt (RTP.primNatToInt n)

{-
showNat : Nat -> String
showNat zero = "0"
showNat n    =  reverseString $ show n
  where
    digit : Nat -> String
    digit 0 = "0"
    digit 1 = "1"
    digit 2 = "2"
    digit 3 = "3"
    digit 4 = "4"
    digit 5 = "5"
    digit 6 = "6"
    digit 7 = "7"
    digit 8 = "8"
    digit 9 = "9"
    digit _ = "?"

    show : Nat -> String
    show zero = ""
    show n    = digit (mod n 10) ++ show (div n 10)
-}

{-
showInt : Int -> String
showInt (pos n) = showNat n
showInt (neg n) = "-" ++ showNat (suc n)
-}

showChar : Char -> String
showChar = RTP.primShowChar

showBool : Bool -> String
showBool true = "true"
showBool false = "false"

primitive
  primShowFloat : Float -> String

showFloat : Float -> String
showFloat = primShowFloat


text:
-- | Trailing inductive copattern matches on the LHS can be savely
--   translated to record expressions on RHS, without jeopardizing
--   termination.
--
{-# LANGUAGE CPP #-}
module Agda.TypeChecking.CompiledClause.ToRHS where

-- import Control.Applicative
import Data.Monoid
import qualified Data.Map as Map
import Data.List (genericReplicate, nubBy, findIndex)
import Data.Function

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Monad
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty

import Agda.Utils.List
import Agda.Utils.Impossible
#include "../../undefined.h"


text:
module _ where

open import Agda.Builtin.Bool

module M (b : Bool) where

  module Inner where

    some-boolean : Bool
    some-boolean = b

postulate
  @0 a-postulate : Bool

@0 A : @0 Bool → Set
A b = Bool
  module A where
    module M′ = M b

bad : @0 Bool → Bool
bad = A.M′.Inner.some-boolean

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness --sized-types #-}

open import Data.Product
open import Data.Empty
open import Data.Sum
open import Data.Vec
open import Data.List as List
open import Data.Unit
open import Data.Fin
open import Data.Bool renaming (Bool to 𝔹)
open import Relation.Unary using (_∈_; _⊆_;_∉_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Size
open import Codata.Thunk

open import is-lib.InfSys
open import Common using (Message)

module FairSubtyping-IS {𝕋 : Set} (message : Message 𝕋) where

  open Message message
  open import SessionType message
  open import Session message
  open import Transitions message
  open import Convergence message
  open import Divergence message
  open import Discriminator message
  open import Action message using (Action)
  open import Subtyping message
  open import FairSubtyping message as FS
  open import HasTrace message
  open import Compliance message
  open import FairCompliance message
  open import Trace message
  open import FairCompliance-IS message

  private
    U : Set
    U = SessionType × SessionType

  data FSubIS-RN : Set where
    nil-any end-def : FSubIS-RN
    ii oo : FSubIS-RN

  data FSubCOIS-RN : Set where
    co-conv : FSubCOIS-RN

  nil-any-r : FinMetaRule U
  nil-any-r .Ctx = SessionType
  nil-any-r .comp T =
    [] ,
    ------------------
    (nil , T)

  end-def-r : FinMetaRule U
  end-def-r .Ctx = Σ[ (T , S) ∈ SessionType × SessionType ] End T × Defined S
  end-def-r .comp ((T , S) , _) =
    [] ,
    ------------------
    (T , S)

  ii-r : MetaRule U
  ii-r .Ctx = Σ[ (f , g) ∈ Continuation × Continuation ] dom f ⊆ dom g
  ii-r .Pos ((f , _) , _) = Σ[ t ∈ 𝕋 ] t ∈ dom f
  ii-r .prems ((f , g) , _) (t , _) = f t .force , g t .force
  ii-r .conclu ((f , g) , _) = inp f , inp g

  oo-r : MetaRule U
  oo-r .Ctx = Σ[ (f , g) ∈ Continuation × Continuation ] dom g ⊆ dom f × Witness g
  oo-r .Pos ((_ , g) , _) = Σ[ t ∈ 𝕋 ] t ∈ dom g
  oo-r .prems ((f , g) , _) (t , _) = f t .force , g t .force
  oo-r .conclu ((f , g) , _) = out f , out g

  co-conv-r : FinMetaRule U
  co-conv-r .Ctx = Σ[ (T , S) ∈ SessionType × SessionType ] T ↓ S
  co-conv-r .comp ((T , S) , _) =
    [] ,
    ------------------
    (T , S)

  FSubIS : IS U
  FSubIS .Names = FSubIS-RN
  FSubIS .rules nil-any = from nil-any-r
  FSubIS .rules end-def = from end-def-r
  FSubIS .rules ii = ii-r
  FSubIS .rules oo = oo-r

  FSubCOIS : IS U
  FSubCOIS .Names = FSubCOIS-RN
  FSubCOIS .rules co-conv = from co-conv-r

  _≤F_ : SessionType → SessionType → Set
  T ≤F S = FCoInd⟦ FSubIS , FSubCOIS ⟧ (T , S)

  _≤Fᵢ_ : SessionType → SessionType → Set
  T ≤Fᵢ S = Ind⟦ FSubIS ∪ FSubCOIS ⟧ (T , S)

  _≤Fc_ : SessionType → SessionType → Set
  T ≤Fc S = CoInd⟦ FSubIS ⟧ (T , S)

  {- Specification using _⊢_ is correct wrt FairSubtypingS -}

  FSSpec-⊢ : U → Set
  FSSpec-⊢ (T , S) = ∀{R} → R ⊢ T → R ⊢ S

  spec-sound : ∀{T S} → FairSubtypingS T S → FSSpec-⊢ (T , S)
  spec-sound fs fc = fc-complete (fs (fc-sound fc))

  spec-complete : ∀{T S} → FSSpec-⊢ (T , S) → FairSubtypingS T S
  spec-complete fs fc = fc-sound (fs (fc-complete fc))

  ------------------------------------------------------

  {- Soundness -}
  -- Using bounded coinduction wrt SpecAux

  ≤Fᵢ->↓ : ∀{S T} → S ≤Fᵢ T → S ↓ T
  ≤Fᵢ->↓ (fold (inj₁ nil-any , _ , refl , _)) = nil-converges
  ≤Fᵢ->↓ (fold (inj₁ end-def , (_ , (end , def)) , refl , _)) = end-converges end def
  ≤Fᵢ->↓ (fold (inj₁ ii , _ , refl , pr)) = converge (pre-conv-inp-back λ x → ↓->preconv (≤Fᵢ->↓ (pr (_ , x))))
  ≤Fᵢ->↓ (fold (inj₁ oo , (_ , (incl , (t , ok-t))) , refl , pr)) =
    converge
      λ _ _ → [] , t , none , (_ , incl ok-t , step (out (incl ok-t)) refl) , (_ , ok-t , step (out ok-t) refl) , ≤Fᵢ->↓ (pr (t , ok-t))
  ≤Fᵢ->↓ (fold (inj₂ co-conv , (_ , conv) , refl , _)) = conv

  SpecAux : U → Set
  SpecAux (R , T) = Σ[ S ∈ SessionType ] S ≤F T × R ⊢ S

  ≤Fᵢ->defined : ∀{S T} → Defined S → S ≤Fᵢ T → Defined T
  ≤Fᵢ->defined def fs = conv->defined def (≤Fᵢ->↓ fs)

  spec-bounded-rec : ∀{R S} T → T ≤Fᵢ S → R ⊢ T → R ⊢ᵢ S
  spec-bounded-rec _ fs fc =
    let _ , reds , succ = con-sound (≤Fᵢ->↓ fs) (fc-sound fc) in
    maysucceed->⊢ᵢ reds succ

  spec-bounded : SpecAux ⊆ λ (R , S) → R ⊢ᵢ S
  spec-bounded (T , fs , fc) = spec-bounded-rec T (fcoind-to-ind fs) fc

  spec-cons : SpecAux ⊆ ISF[ FCompIS ] SpecAux
  spec-cons {(R , T)} (S , fs , fc) with fc .CoInd⟦_⟧.unfold
  spec-cons {(R , T)} (S , fs , fc) | client-end , ((_ , (win , def)) , _) , refl , _ =
    client-end , ((R , _) , (win , ≤Fᵢ->defined def (fcoind-to-ind fs))) , refl , λ ()
  spec-cons {(out r , _)} ((inp f) , fs , fc) | oi , (((.r , .f) , wit-r) , _) , refl , pr with fs .CoInd⟦_⟧.unfold
  ... | end-def , (((.(inp f) , _) , (inp e , _)) , _) , refl , _ = ⊥-elim (e _ (proj₂ (fc->defined (pr wit-r))))
  ... | ii , (((.f , g) , _) , _) , refl , pr' = oi , (_ , wit-r) , refl , λ wit → _ , pr' (_ , proj₂ (fc->defined (pr wit))) , pr wit
  spec-cons {(inp r , T)} (out f , fs , fc) | io , (((.r , .f) , wit-f) , _) , refl , pr with fs .CoInd⟦_⟧.unfold
  ... | end-def , (((.(out f) , _) , (out e , _)) , _) , refl , _ = ⊥-elim (e _ (proj₂ wit-f))
  ... | oo , (((.f , g) , (incl , wit-g)) , _) , refl , pr' = io , (_ , wit-g) , refl , λ wit → _ , pr' wit , pr (_ , incl (proj₂ wit))

  spec-aux-sound : SpecAux ⊆ λ (R , S) → R ⊢ S
  spec-aux-sound = bounded-coind[ FCompIS , FCompCOIS ] SpecAux spec-bounded spec-cons

  fs-sound : ∀{T S} → T ≤F S → FSSpec-⊢ (T , S)
  fs-sound {T} fs fc = spec-aux-sound (T , fs , fc)

  {- Soundness & Completeness of Sub wrt ≤Fc -}

  ≤Fc->sub : ∀{S T} → S ≤Fc T → ∀ {i} → Sub S T i
  ≤Fc->sub fs with fs .CoInd⟦_⟧.unfold
  ... | nil-any , _ , refl , _ = nil<:any
  ... | end-def , (_ , (end , def)) , refl , _ = end<:def end def
  ... | ii , ((f , g) , incl) , refl , pr = inp<:inp incl λ x → λ where .force → if-def x
    where
      if-def : (t : 𝕋) → ∀{i} → Sub (f t .force) (g t .force) i
      if-def t with t ∈? f
      ... | yes ok-t = ≤Fc->sub (pr (_ , ok-t))
      ... | no no-t = subst (λ x → Sub x (g t .force) _) (sym (not-def->nil no-t)) nil<:any
  ... | oo , (_ , (incl , wit)) , refl , pr = out<:out wit incl λ ok-x → λ where .force → ≤Fc->sub (pr (_ , ok-x))

  sub->≤Fc : ∀{S T} → (∀{i} → Sub S T i) → S ≤Fc T
  CoInd⟦_⟧.unfold (sub->≤Fc fs) with fs
  ... | nil<:any = nil-any , _ , refl , λ ()
  ... | end<:def end def = end-def , (_ , (end , def)) , refl , λ ()
  ... | inp<:inp incl pr = ii , (_ , incl) , refl , λ (p , _) → sub->≤Fc (pr p .force)
  ... | out<:out wit incl pr = oo , (_ , (incl , wit)) , refl , λ (_ , ok) → sub->≤Fc (pr ok .force)

  {- Auxiliary -}

  -- Only premise for rules using sample-cont in ⊢
  sample-cont-prem : ∀{f : Continuation}{t R} → R ⊢ f t .force
    → (pos : Σ[ p ∈ 𝕋 ] p ∈ dom (sample-cont t R nil)) → (sample-cont t R nil) (proj₁ pos) .force ⊢ f (proj₁ pos) .force
  sample-cont-prem {f} {t} pr (p , ok-p) with p ?= t
  ... | yes refl = pr
  sample-cont-prem {f} {t} pr (p , ()) | no ¬eq

  -- Premises using sample-cont-dual in ⊢
  sample-cont-prems : ∀{f : Continuation}{t} → t ∉ dom f
    → (pos : Σ[ p ∈ 𝕋 ] p ∈ dom f) → (sample-cont t nil win) (proj₁ pos) .force ⊢ f (proj₁ pos) .force
  sample-cont-prems {f} {t} no-t (p , ok-p) with p ?= t
  ... | yes refl = ⊥-elim (no-t ok-p)
  ... | no ¬eq = win⊢def ok-p

  -- Premises using sample-cont-dual in ⊢
  sample-cont-prems' : ∀{f : Continuation}{t R} → R ⊢ f t .force
    → (pos : Σ[ p ∈ 𝕋 ] p ∈ dom f) → (sample-cont t R win) (proj₁ pos) .force ⊢ f (proj₁ pos) .force
  sample-cont-prems' {f} {t} pr (p , ok-p) with p ?= t
  ... | yes refl = pr
  ... | no ¬eq = win⊢def ok-p

  spec-inp->incl : ∀{f g} → FSSpec-⊢ (inp f , inp g) → dom f ⊆ dom g
  spec-inp->incl {f} {g} fs {t} ok-t with fs (apply-fcoind oi ((sample-cont t win nil , f) , wit-cont out) (sample-cont-prem {f} {t} (win⊢def ok-t))) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (out e , _)) , _) , refl , _ = ⊥-elim (e t (proj₂ (wit-cont out)))
  ... | oi , _ , refl , pr = proj₂ (fc->defined (pr (t , proj₂ (wit-cont out))))

  spec-out->incl : ∀{f g} → FSSpec-⊢ (out f , out g) → Witness f → dom g ⊆ dom f
  spec-out->incl {f} {g} fs wit {t} ok-t with t ∈? f
  ... | yes ok = ok
  ... | no no-t with (fs (apply-fcoind io ((sample-cont t nil win ,  f) , wit) (sample-cont-prems {f} {t} no-t))) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (() , _)) , _) , refl , _
  ... | io , _ , refl , pr = ⊥-elim (cont-not-def (proj₁ (fc->defined (pr (t , ok-t)))))

  spec-out->wit : ∀{f g} → Witness f →  FSSpec-⊢ (out f , out g) → Witness g
  spec-out->wit {f} {g} wit-f fs with Empty? g
  ... | inj₂ wit = wit
  ... | inj₁ e with (fs (apply-fcoind io ((full-cont win , f) , wit-f) λ (_ , ok) → win⊢def ok)) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (() , _)) , _) , refl , _
  ... | io , ((_ , wit-g) , _) , refl , _ = ⊥-elim (e _ (proj₂ wit-g))

  {- Boundedness & Consistency -}

  fsspec-cons : FSSpec-⊢ ⊆ ISF[ FSubIS ] FSSpec-⊢
  fsspec-cons {nil , T} fs = nil-any , _ , refl , λ ()
  fsspec-cons {inp f , nil} fs with (fs (apply-fcoind client-end ((win , _) , (Win-win , inp)) λ ())) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (_ , ())) , _) , refl , _
  fsspec-cons {inp f , inp g} fs = ii , ((f , g) , spec-inp->incl fs) , refl ,
    λ (p , _) {R} fc-r-f →
      let wit = wit-cont (proj₁ (fc->defined fc-r-f)) in
      let fc-Or-Ig = fs (apply-fcoind oi ((sample-cont p R nil , f) , wit) (sample-cont-prem {f} {p} fc-r-f)) in
      let fc-r-g = ⊢-after-out {sample-cont p R nil} {g} {p} (proj₂ wit) fc-Or-Ig in
      subst (λ x → x ⊢ g p .force) (sym force-eq) fc-r-g
  fsspec-cons {inp f , out g} fs with Empty? f
  ... | inj₁ e = end-def , (_ , (inp e , out)) , refl , λ ()
  ... | inj₂ (t , ok-t) with (fs (apply-fcoind oi ((sample-cont t win nil , f) , wit-cont out) (sample-cont-prem {f} {t} (win⊢def ok-t)))) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (out e , out)) , _) , refl , _ = ⊥-elim (e t (proj₂ (wit-cont out)))
  fsspec-cons {out f , nil} fs with (fs (apply-fcoind client-end ((win , _) , (Win-win , out)) λ ())) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (_ , ())) , _) , refl , _
  fsspec-cons {out f , inp g} fs with Empty? f
  ... | inj₁ e = end-def , (_ , (out e , inp)) , refl , λ ()
  ... | inj₂ (t , ok-t) with (fs (apply-fcoind io ((full-cont win , f) , (t , ok-t)) λ (_ , ok-p) → win⊢def ok-p)) .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (() , inp)) , _) , refl , _
  fsspec-cons {out f , out g} fs with Empty? f
  ... | inj₁ e = end-def , (_ , (out e , out)) , refl , λ ()
  ... | inj₂ (t , ok-t) =
    let wit-g = spec-out->wit (t , ok-t) fs in
    let incl = spec-out->incl fs (t , ok-t) in
    oo , ((f , g) , (incl , wit-g)) , refl , λ (p , ok-p) {R} fc-r-f →
      let fc-Ir-Og = fs (apply-fcoind io ((sample-cont p R win , f) , (t , ok-t)) (sample-cont-prems' {f} {p} fc-r-f)) in
      let fc-r-g = ⊢-after-in {sample-cont p R win} {g} {p} ok-p fc-Ir-Og in
      subst (λ x → x ⊢ g p .force) (sym force-eq) fc-r-g

  fsspec->sub : ∀{S T} → FSSpec-⊢ (S , T) → S ≤Fc T
  fsspec->sub = coind[ FSubIS ] FSSpec-⊢ fsspec-cons

  postulate
    not-conv-div : ∀{T S} → ¬ T ↓ S → T ↑ S

  fs-convergence : ∀{T S} → FairSubtypingS T S → T ↓ S
  fs-convergence {T} {S} fs with Common.excluded-middle {T ↓ S}
  fs-convergence {T} {S} fs | yes p = p
  fs-convergence {T} {S} fs | no p =
    let div = not-conv-div p in
    let sub = ≤Fc->sub (fsspec->sub (spec-sound fs)) in
    let d-comp = discriminator-compliant sub div in
    let ¬d-comp = discriminator-not-compliant sub div in
    ⊥-elim (¬d-comp (fs d-comp))

  fsspec-bounded : ∀{S T} → FSSpec-⊢ (S , T) → S ≤Fᵢ T
  fsspec-bounded fs = apply-ind (inj₂ co-conv) (_ , (fs-convergence (spec-complete fs))) λ ()

  {- Completeness -}

  fs-complete : ∀{S T} → FSSpec-⊢ (S , T) → S ≤F T
  fs-complete = bounded-coind[ FSubIS , FSubCOIS ] FSSpec-⊢ fsspec-bounded fsspec-cons

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
-- Andreas, 2016-10-11, AIM XXIV
-- We cannot bind NATURAL to an abstract version of Nat.

abstract
  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}


text:
-- Jesper, 2018-10-29 (comment on #3332): Besides for rewrite, builtin
-- equality is also used for primErase and primForceLemma. But I don't
-- see how it would hurt to have these use a Prop instead of a Set for
-- equality.

{-# OPTIONS --prop #-}

data _≡_ {A : Set} (a : A) : A → Prop where
  refl : a ≡ a
{-# BUILTIN EQUALITY _≡_ #-}


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

macro
  five : Term → TC ⊤
  five hole = unify hole (lit (nat 5))

-- Here you get hole = _X (λ {n} → y {_n})
-- and fail to solve _n.
yellow : ({n : Nat} → Set) → Nat
yellow y = five

-- Here you get hole = _X ⦃ n ⦄ (λ ⦃ n' ⦄ → y ⦃ _n ⦄)
-- and fail to solve _n due to the multiple candidates n and n'.
more-yellow : ⦃ n : Nat ⦄ → (⦃ n : Nat ⦄ → Set) → Nat
more-yellow y = five

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Symmetric
open import Data.Sum

module Categories.Category.Monoidal.CompactClosed {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Category.Monoidal.Rigid

open Category C
open Commutation C

record CompactClosed : Set (levelOfTerm M) where
  field
    symmetric : Symmetric M
    rigid     : LeftRigid M ⊎ RightRigid M


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

data Unit : Set where
  unit : Unit

_+_ : Unit → Unit → Unit
unit + x = x

data _≡_ (x : Unit) : Unit → Set where
  refl : x ≡ x

{-# BUILTIN REWRITE _≡_ #-}

postulate
  f  : Unit → Unit
  fu : f unit ≡ unit

{-# REWRITE fu #-}

g : Unit → Unit
g unit = unit

data D (h : Unit → Unit) (x : Unit) : Set where
  wrap : Unit → D h x

run : ∀ {h x} → D h x → Unit
run (wrap x) = x

postulate
  d₁ : ∀ n x y (p : D y n) → x (run p + n) ≡ y (run p + n) → D x n

d₂ : ∀ s n → D s n
d₂ _ _ = wrap unit

d₃ : D (λ _ → unit) unit
d₃ = d₁ _ (λ _ → unit) (λ n → f (g n)) (d₂ (λ n → f (g n)) _) refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda