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

module localizations-rings where

import subrings
open subrings public

is-invertible-Ring :
  {l1 : Level} (R : Ring l1) (x : type-Ring R) → UU l1
is-invertible-Ring R =
  is-invertible-Monoid (multiplicative-monoid-Ring R)

is-prop-is-invertible-Ring :
  {l1 : Level} (R : Ring l1) (x : type-Ring R) →
  is-prop (is-invertible-Ring R x)
is-prop-is-invertible-Ring R =
  is-prop-is-invertible-Monoid (multiplicative-monoid-Ring R)

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

{- We introduce homomorphism that invert specific elements -}

inverts-element-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (x : type-Ring R1) →
  (f : hom-Ring R1 R2) → UU l2
inverts-element-hom-Ring R1 R2 x f =
  is-invertible-Ring R2 (map-hom-Ring R1 R2 f x)

is-prop-inverts-element-hom-Ring :
  {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (x : type-Ring R)
  (f : hom-Ring R S) → is-prop (inverts-element-hom-Ring R S x f)
is-prop-inverts-element-hom-Ring R S x f =
  is-prop-is-invertible-Ring S (map-hom-Ring R S f x)

inv-inverts-element-hom-Ring :
  {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (x : type-Ring R)
  (f : hom-Ring R S) → inverts-element-hom-Ring R S x f → type-Ring S
inv-inverts-element-hom-Ring R S x f H = pr1 H

is-left-inverse-inv-inverts-element-hom-Ring :
  {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  Id ( mul-Ring S
       ( inv-inverts-element-hom-Ring R S x f H)
       ( map-hom-Ring R S f x))
     ( unit-Ring S)
is-left-inverse-inv-inverts-element-hom-Ring R S x f H = pr1 (pr2 H)

is-right-inverse-inv-inverts-element-hom-Ring :
  {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  Id ( mul-Ring S
       ( map-hom-Ring R S f x)
       ( inv-inverts-element-hom-Ring R S x f H))
     ( unit-Ring S)
is-right-inverse-inv-inverts-element-hom-Ring R S x f H = pr2 (pr2 H)

inverts-element-comp-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (g : hom-Ring S T) (f : hom-Ring R S) → inverts-element-hom-Ring R S x f →
  inverts-element-hom-Ring R T x (comp-hom-Ring R S T g f)
inverts-element-comp-hom-Ring R S T x g f H =
  pair
    ( map-hom-Ring S T g (inv-inverts-element-hom-Ring R S x f H))
    ( pair
      ( ( inv
          ( preserves-mul-hom-Ring S T g
            ( inv-inverts-element-hom-Ring R S x f H)
            ( map-hom-Ring R S f x))) ∙
        ( ( ap
            ( map-hom-Ring S T g)
            ( is-left-inverse-inv-inverts-element-hom-Ring R S x f H)) ∙
          ( preserves-unit-hom-Ring S T g)))
      ( ( inv
          ( preserves-mul-hom-Ring S T g
            ( map-hom-Ring R S f x)
            ( inv-inverts-element-hom-Ring R S x f H))) ∙
        ( ( ap
            ( map-hom-Ring S T g)
            ( is-right-inverse-inv-inverts-element-hom-Ring R S x f H)) ∙
          ( preserves-unit-hom-Ring S T g))))

{- We state the universal property of the localization of a Ring at a single
   element x ∈ R. -}

precomp-universal-property-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  hom-Ring S T → Σ (hom-Ring R T) (inverts-element-hom-Ring R T x)
precomp-universal-property-localization-Ring R S T x f H g =
  pair (comp-hom-Ring R S T g f) (inverts-element-comp-hom-Ring R S T x g f H)

universal-property-localization-Ring :
  (l : Level) {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (x : type-Ring R)
  (f : hom-Ring R S) → inverts-element-hom-Ring R S x f → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-localization-Ring l R S x f H =
  (T : Ring l) →
  is-equiv (precomp-universal-property-localization-Ring R S T x f H)

unique-extension-universal-property-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  universal-property-localization-Ring l3 R S x f H →
  (h : hom-Ring R T) (K : inverts-element-hom-Ring R T x h) →
  is-contr
    (Σ (hom-Ring S T) (λ g → htpy-hom-Ring R T (comp-hom-Ring R S T g f) h))
unique-extension-universal-property-localization-Ring R S T x f H up-f h K =
  is-contr-equiv'
    ( fib (precomp-universal-property-localization-Ring R S T x f H) (pair h K))
    ( equiv-tot ( λ g →
      ( equiv-htpy-hom-Ring-eq R T (comp-hom-Ring R S T g f) h) ∘e
      ( equiv-Eq-total-subtype-eq
        ( is-prop-inverts-element-hom-Ring R T x)
        ( precomp-universal-property-localization-Ring R S T x f H g)
        ( pair h K))))
    ( is-contr-map-is-equiv (up-f T) (pair h K))

center-unique-extension-universal-property-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  universal-property-localization-Ring l3 R S x f H →
  (h : hom-Ring R T) (K : inverts-element-hom-Ring R T x h) →
  Σ (hom-Ring S T) (λ g → htpy-hom-Ring R T (comp-hom-Ring R S T g f) h)
center-unique-extension-universal-property-localization-Ring R S T x f H up-f h K =
  center
    ( unique-extension-universal-property-localization-Ring
      R S T x f H up-f h K)

map-universal-property-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  universal-property-localization-Ring l3 R S x f H →
  (h : hom-Ring R T) (K : inverts-element-hom-Ring R T x h) → hom-Ring S T
map-universal-property-localization-Ring R S T x f H up-f h K =
  pr1 ( center-unique-extension-universal-property-localization-Ring
        R S T x f H up-f h K)

htpy-universal-property-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (H : inverts-element-hom-Ring R S x f) →
  (up-f : universal-property-localization-Ring l3 R S x f H) →
  (h : hom-Ring R T) (K : inverts-element-hom-Ring R T x h) →
  htpy-hom-Ring R T (comp-hom-Ring R S T (map-universal-property-localization-Ring R S T x f H up-f h K) f) h
htpy-universal-property-localization-Ring R S T x f H up-f h K =
  pr2 ( center-unique-extension-universal-property-localization-Ring
        R S T x f H up-f h K)

{- We show that the type of localizations of a ring R at an element x is
   contractible. -}

is-equiv-up-localization-up-localization-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
  (f : hom-Ring R S) (inverts-f : inverts-element-hom-Ring R S x f) →
  (g : hom-Ring R T) (inverts-g : inverts-element-hom-Ring R T x g) →
  (h : hom-Ring S T) (H : htpy-hom-Ring R T (comp-hom-Ring R S T h f) g) →
  ({l : Level} → universal-property-localization-Ring l R S x f inverts-f) →
  ({l : Level} → universal-property-localization-Ring l R T x g inverts-g) →
  is-iso-hom-Ring S T h
is-equiv-up-localization-up-localization-Ring R S T x f inverts-f g inverts-g h H up-f up-g = {!is-iso-is-equiv-hom-Ring!}

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

{- We introduce homomorphisms that invert all elements of a subset of a ring -}

inverts-subset-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R) →
  (f : hom-Ring R S) → UU (l1 ⊔ l2 ⊔ l3)
inverts-subset-hom-Ring R S P f =
  (x : type-Ring R) (p : type-Prop (P x)) → inverts-element-hom-Ring R S x f

is-prop-inverts-subset-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R) →
  (f : hom-Ring R S) → is-prop (inverts-subset-hom-Ring R S P f)
is-prop-inverts-subset-hom-Ring R S P f =
  is-prop-Π (λ x → is-prop-Π (λ p → is-prop-inverts-element-hom-Ring R S x f))

inv-inverts-subset-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R)
  (f : hom-Ring R S) (H : inverts-subset-hom-Ring R S P f)
  (x : type-Ring R) (p : type-Prop (P x)) → type-Ring S
inv-inverts-subset-hom-Ring R S P f H x p =
  inv-inverts-element-hom-Ring R S x f (H x p)

is-left-inverse-inv-inverts-subset-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R)
  (f : hom-Ring R S) (H : inverts-subset-hom-Ring R S P f)
  (x : type-Ring R) (p : type-Prop (P x)) →
  Id (mul-Ring S (inv-inverts-subset-hom-Ring R S P f H x p) (map-hom-Ring R S f x)) (unit-Ring S)
is-left-inverse-inv-inverts-subset-hom-Ring R S P f H x p =
  is-left-inverse-inv-inverts-element-hom-Ring R S x f (H x p)

is-right-inverse-inv-inverts-subset-hom-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R)
  (f : hom-Ring R S) (H : inverts-subset-hom-Ring R S P f)
  (x : type-Ring R) (p : type-Prop (P x)) →
  Id (mul-Ring S (map-hom-Ring R S f x) (inv-inverts-subset-hom-Ring R S P f H x p)) (unit-Ring S)
is-right-inverse-inv-inverts-subset-hom-Ring R S P f H x p =
  is-right-inverse-inv-inverts-element-hom-Ring R S x f (H x p)

inverts-subset-comp-hom-Ring :
  {l1 l2 l3 l4 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3)
  (P : subset-Ring l4 R) (g : hom-Ring S T) (f : hom-Ring R S) →
  inverts-subset-hom-Ring R S P f →
  inverts-subset-hom-Ring R T P (comp-hom-Ring R S T g f)
inverts-subset-comp-hom-Ring R S T P g f H x p =
  inverts-element-comp-hom-Ring R S T x g f (H x p)

{- We state the universal property of the localization of a Ring at a subset
   of R. -}

precomp-universal-property-localization-subset-Ring :
  {l1 l2 l3 l4 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3)
  (P : subset-Ring l4 R) →
  (f : hom-Ring R S) (H : inverts-subset-hom-Ring R S P f) →
  hom-Ring S T → Σ (hom-Ring R T) (inverts-subset-hom-Ring R T P)
precomp-universal-property-localization-subset-Ring R S T P f H g =
  pair (comp-hom-Ring R S T g f) (inverts-subset-comp-hom-Ring R S T P g f H)

universal-property-localization-subset-Ring :
  (l : Level) {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2)
  (P : subset-Ring l3 R) (f : hom-Ring R S) →
  inverts-subset-hom-Ring R S P f → UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-localization-subset-Ring l R S P f H =
  (T : Ring l) →
  is-equiv (precomp-universal-property-localization-subset-Ring R S T P f H)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
module reflnat where

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

_+_ : ℕ -> ℕ ->  ℕ
n + Z   = n
n + S m = S (n + m)

infixr 10 _+_

infixr 20 _*_
_*_ : ℕ -> ℕ ->  ℕ
n * Z   = Z
n * S m = n * m + n

data Bool : Set where
  tt : Bool
  ff : Bool

data ⊤ : Set where
  true : ⊤

data ⊥ : Set where

Atom : Bool -> Set
Atom tt = ⊤
Atom ff = ⊥

_==Bool_ : ℕ -> ℕ -> Bool
Z     ==Bool  Z     = tt
(S n) ==Bool  (S m) = n ==Bool m
_     ==Bool  _     = ff
-- Z     ==Bool (S _)  = ff
-- (S _) ==Bool Z      = ff

_==_ : ℕ -> ℕ -> Set
n == m = Atom ( n ==Bool m)

Refl : Set
Refl = (n : ℕ) -> n == n

refl : Refl
refl Z     = true
refl (S n) = refl n

ext: agda

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


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

variable
  @0 A : Set

data D : Set₁ where
  c : A → D


text:
module Logic.Predicate where

open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Type
open import Type.Properties.Inhabited

------------------------------------------
-- Existential quantification (Existance, Exists)

module _ {ℓ₁}{ℓ₂} where
  record ∃ {Obj : Type{ℓ₁}} (Pred : Obj → Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    eta-equality
    constructor [∃]-intro
    field
      witness   : Obj
      ⦃ proof ⦄ : Pred(witness)

  [∃]-witness : ∀{Obj}{Pred} → ∃{Obj}(Pred) → Obj
  [∃]-witness([∃]-intro(x) ⦃ _ ⦄ ) = x

  [∃]-proof : ∀{Obj}{Pred} → (e : ∃{Obj}(Pred)) → Pred([∃]-witness(e))
  [∃]-proof([∃]-intro(_) ⦃ proof ⦄ ) = proof

  [∃]-elim : ∀{ℓ₃}{Obj}{Pred}{Z : Stmt{ℓ₃}} → (∀{x : Obj} → Pred(x) → Z) → (∃{Obj} Pred) → Z
  [∃]-elim (f) ([∃]-intro(_) ⦃ proof ⦄) = f(proof)

  syntax ∃{T}(λ x → y) = ∃❪ x ꞉ T ❫․ y

  {- TODO: This would allow the syntax: ∃ₗ x ↦ P(x)
    ∃ₗ_ = ∃
    infixl 1 ∃ₗ_
  -}

private variable ℓ : Lvl.Level
private variable Obj X Y Z W : Type{ℓ}
private variable Pred P Q R : X → Type{ℓ}

[∃]-map-proof : (∀{x} → P(x) → Q(x)) → ((∃ P) → (∃ Q))
[∃]-map-proof (f) ([∃]-intro(x) ⦃ proof ⦄) = [∃]-intro(x) ⦃ f(proof) ⦄

[∃]-map : (f : X → X) → (∀{x} → P(x) → Q(f(x))) → ((∃ P) → (∃ Q))
[∃]-map f p ([∃]-intro(x) ⦃ proof ⦄) = [∃]-intro(f(x)) ⦃ p(proof) ⦄

[∃]-map₂ : (f : X → Y → Z) → (∀{x y} → P(x) → Q(y) → R(f x y)) → ((∃ P) → (∃ Q) → (∃ R))
[∃]-map₂ f p ([∃]-intro(x) ⦃ proof₁ ⦄) ([∃]-intro(y) ⦃ proof₂ ⦄) = [∃]-intro(f x y) ⦃ p proof₁ proof₂ ⦄

[∃]-map-proof-dependent : (ep : ∃ P) → (P(∃.witness ep) → Q(∃.witness ep)) → (∃ Q)
[∃]-map-proof-dependent ([∃]-intro(x) ⦃ proof ⦄) f = [∃]-intro(x) ⦃ f(proof) ⦄

------------------------------------------
-- Universal quantification (Forall, All)

∀ₗ : (Pred : Obj → Stmt{ℓ}) → Stmt
∀ₗ (Pred) = (∀{x} → Pred(x))

[∀]-intro : ((a : Obj) → Pred(a)) → ∀ₗ(x ↦ Pred(x))
[∀]-intro p{a} = p(a)

[∀]-elim : ∀ₗ(x ↦ Pred(x)) → (a : Obj) → Pred(a)
[∀]-elim p(a) = p{a}

-- Eliminates universal quantification for a non-empty domain using a witnessed existence which proves that the domain is non-empty.
[∀ₑ]-elim : ⦃ _ : ◊ Obj ⦄ → ∀{P : Obj → Stmt{ℓ}} → ∀ₗ(x ↦ P(x)) → P([◊]-existence)
[∀ₑ]-elim {Obj = Obj} ⦃ proof ⦄ {P} apx = [∀]-elim {Obj = Obj}{P} apx(◊.existence(proof))

syntax ∀ₗ{T}(λ x → y) = ∀❪ x ꞉ T ❫․ y

∀⁰ : (Pred : Stmt{ℓ}) → Stmt
∀⁰ = id

∀¹ : (Pred : X → Stmt{ℓ}) → Stmt
∀¹ (Pred) = ∀⁰(∀ₗ ∘₀ Pred)
-- ∀¹ (Pred) = (∀{x} → Pred(x))

∀² : (Pred : X → Y → Stmt{ℓ}) → Stmt
∀² (Pred) = ∀¹(∀ₗ ∘₁ Pred)
-- ∀² (Pred) = (∀{x}{y} → Pred(x)(y))

∀³ : (Pred : X → Y → Z → Stmt{ℓ}) → Stmt
∀³ (Pred) = ∀²(∀ₗ ∘₂ Pred)
-- ∀³ (Pred) = (∀{x}{y}{z} → Pred(x)(y)(z))

∀⁴ : (Pred : X → Y → Z → W → Stmt{ℓ}) → Stmt
∀⁴ (Pred) = ∀³(∀ₗ ∘₃ Pred)
-- ∀⁴ (Pred) = (∀{x}{y}{z}{w} → Pred(x)(y)(z)(w))

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:
------------------------------------------------------------------------
-- Parsing of matching parentheses, along with a correctness proof
------------------------------------------------------------------------

-- A solution to an exercise set by Helmut Schwichtenberg.

module TotalRecognisers.LeftRecursion.MatchingParentheses where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List
open import Data.List.Properties
open import Data.Product
open import Function.Equivalence
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable as Decidable

private
  module ListMonoid {A : Set} = Monoid (++-monoid A)

import TotalRecognisers.LeftRecursion as LR
import TotalRecognisers.LeftRecursion.Lib as Lib

-- Parentheses.

data Paren : Set where
  ⟦ ⟧ : Paren

-- Strings of matching parentheses.

data Matching : List Paren → Set where
  nil : Matching []
  app : ∀ {xs ys}
        (p₁ : Matching xs) (p₂ : Matching ys) → Matching (xs ++ ys)
  par : ∀ {xs} (p : Matching xs) → Matching ([ ⟦ ] ++ xs ++ [ ⟧ ])

-- Our goal: decide Matching.

Goal : Set
Goal = ∀ xs → Dec (Matching xs)

-- Equality of parentheses is decidable.

_≟-Paren_ : Decidable (_≡_ {A = Paren})
⟦ ≟-Paren ⟦ = yes P.refl
⟦ ≟-Paren ⟧ = no λ()
⟧ ≟-Paren ⟦ = no λ()
⟧ ≟-Paren ⟧ = yes P.refl

open LR Paren hiding (_∷_)
private
  open module Tok = Lib.Tok Paren _≟-Paren_ using (tok)

-- A (left and right recursive) grammar for matching parentheses. Note
-- the use of nonempty; without the two occurrences of nonempty the
-- grammar would not be well-formed.

matching : P _
matching =
    empty
  ∣ ♯ nonempty matching · ♯ nonempty matching
  ∣ ♯ (tok ⟦ · ♯ matching) · ♯ tok ⟧

-- We can decide membership of matching.

decide-matching : ∀ xs → Dec (xs ∈ matching)
decide-matching xs = xs ∈? matching

-- Membership of matching is equivalent to satisfaction of Matching.

∈m⇔M : ∀ {xs} → (xs ∈ matching) ⇔ Matching xs
∈m⇔M = equivalence to from
  where
  to : ∀ {xs} → xs ∈ matching → Matching xs
  to (∣-left (∣-left empty))                        = nil
  to (∣-left (∣-right (nonempty p₁ · nonempty p₂))) = app (to p₁) (to p₂)
  to (∣-right (⟦∈ · p · ⟧∈))
    rewrite Tok.sound ⟦∈ | Tok.sound ⟧∈             = par (to p)

  from : ∀ {xs} → Matching xs → xs ∈ matching
  from nil                                    = ∣-left (∣-left empty)
  from (app {xs = []}                  p₁ p₂) = from p₂
  from (app {xs = x ∷ xs} {ys = []}    p₁ p₂) rewrite proj₂ ListMonoid.identity xs = from p₁
  from (app {xs = _ ∷ _}  {ys = _ ∷ _} p₁ p₂) = ∣-left (∣-right {n₁ = true} (nonempty (from p₁) · nonempty (from p₂)))
  from (par p)                                = ∣-right {n₁ = true} (Tok.complete · from p · Tok.complete)

-- And thus we reach our goal.

goal : Goal
goal xs = Decidable.map ∈m⇔M (decide-matching xs)

-- Some examples.

ex₁ : Dec (Matching [])
ex₁ = goal _ -- = yes nil

ex₂ : Dec (Matching (⟦ ∷ ⟧ ∷ []))
ex₂ = goal _ -- = yes (par nil)

ex₃ : Dec (Matching (⟦ ∷ ⟧ ∷ ⟦ ∷ ⟧ ∷ []))
ex₃ = goal _ -- = yes (app (par nil) (par nil))

ex₄ : Dec (Matching (⟦ ∷ ⟧ ∷ ⟦ ∷ []))
ex₄ = goal _ -- = no (λ x → …)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where every pair of elements are related (symmetrically)
------------------------------------------------------------------------

-- Core modules are not meant to be used directly outside of the
-- standard library.

-- This module should be removable if and when Agda issue
-- https://github.com/agda/agda/issues/3210 is fixed

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

open import Relation.Binary using (Rel)

module Data.List.Relation.Unary.AllPairs.Core
       {a ℓ} {A : Set a} (R : Rel A ℓ) where

open import Level
open import Data.List.Base
open import Data.List.Relation.Unary.All

------------------------------------------------------------------------
-- Definition

-- AllPairs R xs means that every pair of elements (x , y) in xs is a
-- member of relation R (as long as x comes before y in the list).

infixr 5 _∷_

data AllPairs : List A → Set (a ⊔ ℓ) where
  []  : AllPairs []
  _∷_ : ∀ {x xs} → All (R x) xs → AllPairs xs → AllPairs (x ∷ xs)


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Inference.ConstraintGen(x : X) where
  import OutsideIn.Constraints as C
  import OutsideIn.TypeSchema as TS
  import OutsideIn.Expressions as E
  import OutsideIn.Environments as V
  open X(x) renaming (funType to _⟶_; appType to _··_)
  open C(x)
  open TS(x)
  open E(x)
  open V(x)
  open import Data.Vec

  private module PlusN-m n        = Monad (PlusN-is-monad {n})
          module PlusN-f n        = Functor (Monad.is-functor (PlusN-is-monad {n}))
          module TypeSchema-f {n} = Functor (type-schema-is-functor {n})
          module Type-f           = Functor (type-is-functor)
          module QC-f             = Functor (qconstraint-is-functor)
          module Exp-f₁ {tv} {r}  = Functor (expression-is-functor₁ {tv} {r})
          module Exp-f₂ {ev} {r}  = Functor (expression-is-functor₂ {ev} {r})
          module Constraint-f {s} = Functor (constraint-is-functor {s})
          module Vec-f {n}        = Functor (vec-is-functor {n})
          open Monad (type-is-monad) using () renaming (unit to TVar)

  private

    upindex : {X : Set → Set}{tv : Set} → ⦃ is-functor : Functor X ⦄ → X tv → X (Ⓢ tv)
    upindex ⦃ is-functor ⦄ e = suc <$> e
      where open Functor (is-functor)

    _↑c : {tv : Set}{s : Strata} → (Constraint tv s) → (Constraint (Ⓢ tv) s)
    _↑c {s = s} = upindex ⦃ constraint-is-functor {s} ⦄

    _↑e : {ev tv : Set}{r : Shape} → (Expression ev tv r) → (Expression ev (Ⓢ tv) r)
    _↑e = upindex ⦃ expression-is-functor₂ ⦄

    _↑a : {ev tv : Set}{r : Shape} → (Alternatives ev tv r) → (Alternatives ev (Ⓢ tv) r)
    _↑a = upindex ⦃ alternatives-is-functor₂ ⦄

    _↑t : {tv : Set} → (Type tv) → (Type (Ⓢ tv))
    _↑t = upindex ⦃ type-is-functor ⦄

    _↑q : {tv : Set} → (QConstraint tv) → (QConstraint (Ⓢ tv))
    _↑q = upindex ⦃ qconstraint-is-functor ⦄

    infixr 7 _↑e
    infixr 7 _↑c
    infixr 7 _↑t
    infixr 7 _↑a

    applyAll : ∀{tv}(n : ℕ) → Type tv → Type (tv ⨁ n)
    applyAll zero x = x
    applyAll (suc n) x = applyAll n ((x ↑t) ·· (TVar zero))

    funType : ∀{tv}{n} → Vec (Type tv) n → Type tv → Type tv
    funType [] t = t
    funType (x ∷ xs) t = x ⟶ (funType xs t)

    upType : ∀ {n}{tv} → Type tv → Type (tv ⨁ n)
    upType {n} t = Type-f.map (Monad.unit (PlusN-is-monad {n})) t
    upGamma : ∀ {n}{ev}{tv} → Environment ev tv → Environment ev (tv ⨁ n)
    upGamma {n} Γ = TypeSchema-f.map (Monad.unit (PlusN-is-monad {n})) ∘ Γ
    upExp : ∀ {n}{ev}{tv}{r} → Expression ev tv r → Expression ev (tv ⨁ n) r
    upExp {n} e = Exp-f₂.map (Monad.unit (PlusN-is-monad {n})) e
    upAlts : ∀ {n}{ev}{tv}{r} → Alternatives ev tv r → Alternatives ev (tv ⨁ n) r
    upAlts {n} e = Functor.map alternatives-is-functor₂ (Monad.unit (PlusN-is-monad {n})) e

  mutual

    syntax alternativeConstraintGen Γ α₀ α₁ alt C = Γ ►′ alt ∶ α₀ ⟶ α₁ ↝ C
    data alternativeConstraintGen {ev : Set}{tv : Set}(Γ : Environment ev tv)(α₀ α₁ : Type tv) :
                                   {r : Shape} → Alternative ev tv r → Constraint tv Extended → Set where
      Simple : ∀ {r}{n}{v : Name ev (Datacon n)}{e : Expression _ _ r}{a}{τs}{T}{C}
             → let δ = TVar zero
            in Γ v ≡ DC∀ a · τs ⟶ T
             → addAll (Vec-f.map (_↑t) τs) (upGamma {a} Γ ↑Γ) ► (upExp {a} e ↑e) ∶ δ ↝ C
             → Γ ►′ v →′ e ∶ α₀ ⟶ α₁ ↝ Ⅎ′ a · (Ⅎ δ ∼′ (upType {a} α₁ ↑t) ∧′ C) ∧′ applyAll a (TVar T) ∼′ upType {a} α₀
      GADT : ∀ {r}{n}{v : Name ev (Datacon n)}{e : Expression _ _ r}{a}{b}{Q}{τs}{T}{C}
           → let δ = TVar zero
          in Γ v ≡ DC∀′ a , b · Q ⇒ τs ⟶ T
           →   addAll (Vec-f.map (_↑t) τs) (upGamma {b} (upGamma {a} Γ) ↑Γ)
             ► (upExp {b} (upExp {a} e) ↑e) ∶ δ ↝ C
           → Γ ►′ v →′ e ∶ α₀ ⟶ α₁ ↝ Ⅎ′ a · Ⅎ′ b · (Imp′ Q (Ⅎ (C ∧′ δ ∼′ (upType {b} (upType {a} α₁) ↑t))))
                                                  ∧′ upType {b} (upType {a} α₀) ∼′ Type-f.map (PlusN-m.unit b) (applyAll a (TVar T))

    syntax alternativesConstraintGen Γ α₀ α₁ alts C = Γ ►► alts ∶ α₀ ⟶ α₁ ↝ C
    data alternativesConstraintGen {ev : Set}{tv : Set}(Γ : Environment ev tv)(α₀ α₁ : Type tv) :
                                   {r : Shape} → Alternatives ev tv r → Constraint tv Extended → Set where
      NoAlternative : Γ ►► esac ∶ α₀ ⟶ α₁ ↝ ε′
      AnAlternative : ∀ {r₁ r₂}{a : Alternative _ _ r₁}{as : Alternatives _ _ r₂}{C₁}{C₂}
                    → Γ ►′ a      ∶ α₀ ⟶ α₁ ↝ C₁
                    → Γ ►► as     ∶ α₀ ⟶ α₁ ↝ C₂
                    → Γ ►► a ∣ as ∶ α₀ ⟶ α₁ ↝ C₂

    syntax constraintGen a c b d = a ► b ∶ c ↝ d
    data constraintGen {ev : Set}{tv : Set}
                       (Γ : Environment ev tv)(τ : Type tv) : {r : Shape} →
                       Expression ev tv r → Constraint tv Extended → Set where
      VarCon₁ : ∀ {v}{n}{q}{t}
              → Γ (N v) ≡ ∀′ n · q ⇒ t
              → Γ ► Var (N v) ∶ τ ↝ Ⅎ′ n · QC q ∧′ upType {n} τ ∼′ t
      VarCon₂ : ∀ {n}{d}{a}{τs : Vec _ n}{k}
              → Γ (DC d) ≡ DC∀ a · τs ⟶ k
              → Γ ► Var (DC d) ∶ τ ↝ Ⅎ′ a · upType {a} τ ∼′ funType τs (applyAll a (TVar k))
      VarCon₃ : ∀ {n}{d}{a}{b}{Q}{τs : Vec _ n}{k}
              → Γ (DC d) ≡ DC∀′ a , b · Q ⇒ τs ⟶ k
              → Γ ► Var (DC d) ∶ τ ↝ Ⅎ′ a · Ⅎ′ b ·
                                       QC Q ∧′ upType {b} (upType {a} τ) ∼′ funType τs (upType {b} (applyAll a (TVar k)))
      App     : ∀ {r₁}{r₂}{e₁ : Expression _ _ r₁}{e₂ : Expression _ _ r₂}{C₁}{C₂}
              → let α₀ = TVar zero
                    α₁ = TVar (suc zero)
                    α₂ = TVar (suc (suc zero))
                 in upGamma {3} Γ ► upExp {3} e₁ ∶ α₀ ↝ C₁
                  → upGamma {3} Γ ► upExp {3} e₂ ∶ α₁ ↝ C₂
                  → Γ ► e₁ · e₂ ∶ τ ↝ Ⅎ Ⅎ Ⅎ C₁ ∧′ C₂ ∧′ α₀ ∼′ (α₁ ⟶ α₂) ∧′ upType {3} τ ∼′ α₂
      Abs :  ∀ {r}{e : Expression _ _ r}{C}
              → let α₀ = TVar zero
                    α₁ = TVar (suc zero)
                 in ⟨ ∀′ 0 · ε ⇒ α₀ ⟩, upGamma {2} Γ ► upExp {2} e ∶ α₁ ↝ C
                  → Γ ► λ′ e ∶ τ ↝ Ⅎ Ⅎ C ∧′ upType {2} τ ∼′ (α₀ ⟶ α₁)
      Let : ∀{r₁}{r₂}{x : Expression _ _ r₁}{y : Expression _ _ r₂}{C₁}{C₂}
          → let α₀ = TVar zero
                α₁ = TVar (suc zero)
             in                    upGamma {2} Γ ► upExp {2} x ∶ α₀ ↝ C₁
              → ⟨ ∀′ 0 · ε ⇒ α₀ ⟩, upGamma {2} Γ ► upExp {2} y ∶ α₁ ↝ C₂
              → Γ ► let₁ x in′ y ∶ τ ↝ Ⅎ Ⅎ C₁ ∧′ C₂ ∧′ upType {2} τ ∼′ α₁
      LetA : ∀{r₁}{r₂}{x : Expression _ _ r₁}{y : Expression _ _ r₂}{t}{C₁}{C₂}
           → let α₀ = TVar zero
                 α₁ = TVar (suc zero)
              in                    upGamma {2} Γ ► upExp {2} x ∶ α₀ ↝ C₁
               → ⟨ ∀′ 0 · ε ⇒ α₀ ⟩, upGamma {2} Γ ► upExp {2} y ∶ α₁ ↝ C₂
               → Γ ► let₂ x ∷ t in′ y ∶ τ ↝ Ⅎ Ⅎ C₁ ∧′ C₂ ∧′ upType {2} τ ∼′ α₁ ∧′ upType {2} t ∼′ α₀
      GLetA : ∀{n}{r₁}{r₂}{x : Expression _ _ r₁}{y : Expression _ _ r₂}{Q}{t}{C}{C₂}
           → let α₀ = upType {n} (TVar zero)
                 α₁ = upType {n} (TVar (suc zero))
                 up2 = PlusN-f.map n (PlusN-m.unit 2)
              in                     upGamma {n} (upGamma {2} Γ) ► Exp-f₂.map up2 x ∶ α₀ ↝ C
               → upGamma {n} (upGamma {2} (⟨ ∀′ n · Q ⇒ t ⟩, Γ)) ► upExp {n} (upExp {2} y) ∶ α₁ ↝ C₂
               → Γ ► let₃ n · x ∷ Q ⇒ t in′ y ∶ τ ↝ Ⅎ Ⅎ Ⅎ′ n · Imp′ (QC-f.map up2 Q)  (C ∧′ α₀ ∼′ Type-f.map up2 t)
                                                            ∧′ C₂ ∧′ upType {n} (upType {2} τ) ∼′ α₁
      Case : ∀{r₁}{r₂}{x : Expression _ _ r₁}{alts : Alternatives _ _ r₂}{C₁}{C₂}
           → let α₀ = TVar zero
                 α₁ = TVar (suc zero)
              in upGamma {2} Γ ► upExp {2} x ∶ α₀ ↝ C₁
               → upGamma {2} Γ ►► upAlts {2} alts ∶ α₀ ⟶ α₁ ↝ C₂
               → Γ ► case x of alts ∶ τ ↝ Ⅎ Ⅎ C₁ ∧′ C₂

  genConstraint : {ev : Set}{tv : Set}{r : Shape}
                  (Γ : Environment ev tv)(e : Expression ev tv r)(τ : Type tv) → ∃ (λ C → Γ ► e ∶ τ ↝ C)
  genConstraintAlternative : {ev : Set}{tv : Set}{r : Shape} (Γ : Environment ev tv)(a : Alternative ev tv r)(α₀ α₁ : Type tv)
                           → ∃ (λ C → Γ ►′ a ∶ α₀ ⟶ α₁ ↝ C)
  genConstraintAlternative Γ (n →′ e) α₀ α₁ with Γ n | inspect Γ n
  ... | DC∀ a · τs ⟶ k | iC p with genConstraint (addAll (Vec-f.map _↑t τs) (upGamma {a} Γ ↑Γ)) (upExp {a} e ↑e) (TVar zero)
  ...                          | C , p₂ = _ , Simple p p₂
  genConstraintAlternative Γ (n →′ e) α₀ α₁
      | DC∀′ a , b · Q ⇒ τs ⟶ k | iC p with genConstraint (addAll (Vec-f.map _↑t τs) (upGamma {b} (upGamma {a} Γ) ↑Γ))
                                                           (upExp {b} (upExp {a} e) ↑e)
                                                           (TVar zero)
  ...                                   | C , p₂ = _ , GADT p p₂
  genConstraintAlternatives : {ev : Set}{tv : Set}{r : Shape} (Γ : Environment ev tv)(a : Alternatives ev tv r)(α₀ α₁ : Type tv)
                            → ∃ (λ C → Γ ►► a ∶ α₀ ⟶ α₁ ↝ C)
  genConstraintAlternatives Γ esac α₀ α₁ = _ , NoAlternative
  genConstraintAlternatives Γ (a ∣ as) α₀ α₁ with genConstraintAlternative Γ a α₀ α₁ | genConstraintAlternatives Γ as α₀ α₁
  ... | C₁ , p₁ | C₂ , p₂ = _ , AnAlternative p₁ p₂
  genConstraint  Γ (Var (N v)) τ with Γ (N v) | inspect Γ (N v)
  ... | ∀′ n · q ⇒ t | iC prf = _ , VarCon₁ prf
  genConstraint  Γ (Var (DC d)) τ with Γ (DC d) | inspect Γ (DC d)
  ... | DC∀  a · τs ⟶ k         | iC prf = _ , VarCon₂ prf
  ... | DC∀′ a , b · q ⇒ τs ⟶ k | iC prf = _ , VarCon₃ prf
  genConstraint Γ (e₁ · e₂) τ with genConstraint (upGamma {3} Γ) (upExp {3} e₁) (TVar zero)
                                 | genConstraint (upGamma {3} Γ) (upExp {3} e₂) (TVar (suc zero))
  ... | C₁ , p₁ | C₂ , p₂ = _ , App p₁ p₂
  genConstraint Γ (λ′ e′) τ with genConstraint (⟨ ∀′ 0 · ε ⇒ TVar zero ⟩, upGamma {2} Γ) (upExp {2} e′) (TVar (suc zero))
  ... | C , p = _ , Abs p
  genConstraint  Γ (let₁ x in′ y) τ with genConstraint (upGamma {2} Γ) (upExp {2} x) (TVar zero)
                                       | genConstraint (⟨ ∀′ 0 · ε ⇒ TVar zero ⟩, upGamma {2} Γ) (upExp {2} y) (TVar (suc zero))
  ... | C₁ , p₁ | C₂ , p₂ = _ , Let p₁ p₂
  genConstraint Γ (let₂ x ∷ t in′ y) τ with genConstraint (upGamma {2} Γ) (upExp {2} x) (TVar zero)
                                       | genConstraint (⟨ ∀′ 0 · ε ⇒ TVar zero ⟩, upGamma {2} Γ) (upExp {2} y) (TVar (suc zero))
  ... | C₁ , p₁ | C₂ , p₂ = _ , LetA p₁ p₂
  genConstraint Γ (let₃ n · x ∷ Q ⇒ t in′ y) τ with genConstraint (upGamma {n} (upGamma {2} Γ))
                                                                  (Exp-f₂.map (PlusN-f.map n (PlusN-m.unit 2)) x)
                                                                  (upType {n} (TVar zero))
                                                  | genConstraint (upGamma {n} (upGamma {2} (⟨ ∀′ n · Q ⇒ t ⟩, Γ)))
                                                                  (upExp {n} (upExp {2} y))
                                                                  (upType {n} (TVar (suc zero)))
  ... | C₁ , p₁ | C₂ , p₂ = _ , GLetA p₁ p₂
  genConstraint Γ (case x of alts) τ with genConstraint (upGamma {2} Γ) (upExp {2} x) (TVar zero)
                                        | genConstraintAlternatives (upGamma {2} Γ) (upAlts {2} alts) (TVar zero) (TVar (suc zero))
  ... | C₁ , p₁ | C₂ , p₂ = _ , Case p₁ p₂

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
------------------------------------------------------------------------
-- The coinductive type family Coherently
------------------------------------------------------------------------

-- This type family is used to define the lenses in
-- Lens.Non-dependent.Higher.Coinductive and
-- Lens.Non-dependent.Higher.Coinductive.Small.

{-# OPTIONS --cubical --guardedness #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coherently.Coinductive
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

import Equality.Path.Univalence as EPU
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
import Bijection P.equality-with-J as PB
open import Container.Indexed equality-with-J
open import Container.Indexed.M.Codata eq
import Container.Indexed.M.Function equality-with-J as F
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PEq
open import Function-universe equality-with-J hiding (id; _∘_)
import Function-universe P.equality-with-J as PF
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∣_∣)
open import Univalence-axiom equality-with-J
import Univalence-axiom P.equality-with-J as PU

import Lens.Non-dependent.Higher.Coherently.Not-coinductive eq as NC

private
  variable
    a b ℓ p p₁ p₂ : Level
    A A₁ A₂ B C   : Type a
    f q x y       : A
    n             : ℕ

------------------------------------------------------------------------
-- The type family

-- Coherently P step f means that f and all variants of f built using
-- step (in a certain way) satisfy the property P.
--
-- Paolo Capriotti came up with a coinductive definition of lenses.
-- Andrea Vezzosi suggested that one could use a kind of indexed
-- M-type to make it easier to prove that two variants of coinductive
-- lenses are equivalent: the lemma Coherently-cong-≡ below is based
-- on his idea, and Coherently is a less general variant of the M-type
-- that he suggested. See also Coherently-with-restriction′ below,
-- which is defined as an indexed M-type.

record Coherently
         {A : Type a} {B : Type b}
         (P : {A : Type a} → (A → B) → Type p)
         (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B)
         (f : A → B) : Type p where
  coinductive
  field
    property : P f
    coherent : Coherently P step (step f property)

open Coherently public

------------------------------------------------------------------------
-- An equivalence

-- Coherently is pointwise equivalent to NC.Coherently (assuming
-- univalence).

Coherently≃Not-coinductive-coherently :
  {B : Type b}
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
  {f : A → B} →
  Univalence (lsuc a ⊔ b ⊔ p) →
  Univalence (lsuc a ⊔ b) →
  Coherently P step f ≃ NC.Coherently P step f
Coherently≃Not-coinductive-coherently
  {a = a} {B = B} {P = P} {step = step} {f = f} univ₁ univ₂ =
  block λ b →

  Coherently P step f     ↝⟨ Eq.↔→≃ to from
                               (_↔_.from ≡↔≡ ∘ to-from)
                               (_↔_.from ≡↔≡ ∘ from-to) ⟩
  M (CC step) (_ , f)     ↝⟨ carriers-of-final-coalgebras-equivalent
                               (M-coalgebra (CC step) , M-final univ₁ univ₂)
                               (F.M-coalgebra b ext (CC step) , F.M-final b ext ext)
                               _ ⟩
  F.M (CC step) (_ , f)   ↔⟨⟩
  NC.Coherently P step f  □
  where
  CC = NC.Coherently-container P

  to :
    {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} {f : A → B} →
    Coherently P step f → M (CC step) (_ , f)
  to c .out-M .proj₁   = c .property
  to c .out-M .proj₂ _ = to (c .coherent)

  from :
    {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} {f : A → B} →
    M (CC step) (_ , f) → Coherently P step f
  from c .property = c .out-M .proj₁
  from c .coherent = from (c .out-M .proj₂ _)

  to-from :
    {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} {f : A → B} →
    (c : M (CC step) (_ , f)) →
    to (from c) P.≡ c
  to-from c i .out-M .proj₁   = c .out-M .proj₁
  to-from c i .out-M .proj₂ _ = to-from (c .out-M .proj₂ _) i

  from-to :
    {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} {f : A → B} →
    (c : Coherently P step f) →
    from (to c) P.≡ c
  from-to c i .property = c .property
  from-to c i .coherent = from-to (c .coherent) i

------------------------------------------------------------------------
-- Preservation lemmas

private

  -- A preservation lemma for Coherently.
  --
  -- The lemma does not use the univalence argument, instead it uses
  -- EPU.univ (and EPU.≃⇒≡) directly.

  Coherently-cong-≡ :
    Block "Coherently-cong-≡" →
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
    {f : A → B} →
    Univalence p →
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f) →
    ({A : Type a} (f : A → B) (x : P₂ f) →
     step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
    Coherently P₁ step₁ f P.≡ Coherently P₂ step₂ f
  Coherently-cong-≡
    {a = a} {B = B} {p = p} ⊠ {P₁ = P₁} {P₂ = P₂}
    {step₁ = step₁} {step₂ = step₂} {f = f} _ P₁≃P₂′ step₁≡step₂ =

    P.cong (λ ((P , step) :
              ∃ λ (P : (A : Type a) → (A → B) → Type p) →
                  {A : Type a} (f : A → B) → P A f → ∥ A ∥¹ → B) →
             Coherently (P _) step f) $

    P.Σ-≡,≡→≡′

      (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
       EPU.≃⇒≡ (P₁≃P₂ f))

      (P.implicit-extensionality P.ext λ A → P.⟨ext⟩ λ f →
         P.subst (λ P → {A : Type a} (f : A → B) → P A f → ∥ A ∥¹ → B)
           (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
            EPU.≃⇒≡ (P₁≃P₂ f))
           step₁ f                                                      P.≡⟨ P.trans (P.cong (_$ f) $ P.sym $
                                                                                P.push-subst-implicit-application
                                                                                (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) → EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                (λ P A → (f : A → B) → P A f → ∥ A ∥¹ → B)
                                                                                {f = const _} {g = step₁}) $
                                                                             P.sym $ P.push-subst-application
                                                                                (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) → EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                (λ P f → P A f → ∥ A ∥¹ → B)
                                                                                {f = const f} {g = step₁} ⟩
         P.subst (λ P → P A f → ∥ A ∥¹ → B)
           (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
            EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                    P.≡⟨⟩

         P.subst (λ P → P → ∥ A ∥¹ → B)
           (EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                    P.≡⟨ P.sym $
                                                                             PU.transport-theorem
                                                                               (λ P → P → ∥ A ∥¹ → B)
                                                                               (PF.→-cong₁ _)
                                                                               (λ _ → P.refl)
                                                                               EPU.univ
                                                                               (P₁≃P₂ f)
                                                                               (step₁ f) ⟩
         PF.→-cong₁ _ (P₁≃P₂ f) (step₁ f)                               P.≡⟨⟩

         step₁ f ∘ PEq._≃_.from (P₁≃P₂ f)                               P.≡⟨ P.⟨ext⟩ (_↔_.to ≡↔≡ ∘ step₁≡step₂ f) ⟩∎

         step₂ f                                                        ∎)
    where
    P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f PEq.≃ P₂ f
    P₁≃P₂ f = _↔_.to ≃↔≃ (P₁≃P₂′ f)

  -- A "computation rule".

  to-Coherently-cong-≡-property :
    (bl : Block "Coherently-cong-≡")
    {A : Type a} {B : Type b}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
    {f : A → B}
    (univ : Univalence p)
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x)
    (c : Coherently P₁ step₁ f) →
    PU.≡⇒→ (Coherently-cong-≡ bl univ P₁≃P₂ step₁≡step₂) c .property P.≡
    _≃_.to (P₁≃P₂ f) (c .property)
  to-Coherently-cong-≡-property
    ⊠ {P₁ = P₁} {P₂ = P₂} {f = f} _ P₁≃P₂ step₁≡step₂ c =

    P.transport (λ _ → P₂ f) P.0̲
      (_≃_.to (P₁≃P₂ f) (P.transport (λ _ → P₁ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.to (P₁≃P₂ f)
                                                                                (P.transport (λ _ → P₁ f) P.0̲ (c .property))) $
                                                                                P.transport-refl P.0̲ ⟩

    _≃_.to (P₁≃P₂ f) (P.transport (λ _ → P₁ f) P.0̲ (c .property))      P.≡⟨ P.cong (λ g → _≃_.to (P₁≃P₂ f) (g (c .property))) $
                                                                                P.transport-refl P.0̲ ⟩∎
    _≃_.to (P₁≃P₂ f) (c .property)                                     ∎

  -- Another "computation rule".

  from-Coherently-cong-≡-property :
    (bl : Block "Coherently-cong-≡")
    {A : Type a} {B : Type b}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
    {f : A → B}
    (univ : Univalence p)
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x)
    (c : Coherently P₂ step₂ f) →
    PEq._≃_.from
      (PU.≡⇒≃ (Coherently-cong-≡ bl {step₁ = step₁} univ
                 P₁≃P₂ step₁≡step₂))
      c .property P.≡
    _≃_.from (P₁≃P₂ f) (c .property)
  from-Coherently-cong-≡-property
    ⊠ {P₁ = P₁} {P₂ = P₂} {f = f} _ P₁≃P₂ step₁≡step₂ c =

    P.transport (λ _ → P₁ f) P.0̲
      (_≃_.from (P₁≃P₂ f) (P.transport (λ _ → P₂ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.from (P₁≃P₂ f)
                                                                                (P.transport (λ _ → P₂ f) P.0̲ (c .property))) $
                                                                              P.transport-refl P.0̲ ⟩

    _≃_.from (P₁≃P₂ f) (P.transport (λ _ → P₂ f) P.0̲ (c .property))      P.≡⟨ P.cong (λ g → _≃_.from (P₁≃P₂ f) (g (c .property))) $
                                                                              P.transport-refl P.0̲ ⟩∎
    _≃_.from (P₁≃P₂ f) (c .property)                                     ∎

  -- A preservation lemma for Coherently.
  --
  -- The two directions of this equivalence compute the property
  -- fields in certain ways, see the "unit tests" below.
  --
  -- Note that P₁ and P₂ have to target the same universe. A more
  -- general result is given below (Coherently-cong).

  Coherently-cong-≃ :
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
    {f : A → B} →
    Univalence p →
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f) →
    ({A : Type a} (f : A → B) (x : P₂ f) →
     step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
    Coherently P₁ step₁ f ≃ Coherently P₂ step₂ f
  Coherently-cong-≃
    {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂} {f = f}
    univ P₁≃P₂ step₁≡step₂ =

    block λ bl →
    Eq.with-other-inverse
      (Eq.with-other-function
         (equiv bl)
         (to bl)
         (_↔_.from ≡↔≡ ∘ ≡to bl))
      (from bl)
      (_↔_.from ≡↔≡ ∘ ≡from bl)

    where

    equiv :
      Block "Coherently-cong-≡" →
      Coherently P₁ step₁ f ≃ Coherently P₂ step₂ f
    equiv bl =
      _↔_.from ≃↔≃ $ PU.≡⇒≃ $
      Coherently-cong-≡ bl univ P₁≃P₂ step₁≡step₂

    to :
      Block "Coherently-cong-≡" →
      Coherently P₁ step₁ f → Coherently P₂ step₂ f
    to _  c .property = _≃_.to (P₁≃P₂ f) (c .property)
    to bl c .coherent =
      P.subst
        (Coherently P₂ step₂)
        (P.cong (step₂ f) $
         to-Coherently-cong-≡-property bl univ P₁≃P₂ step₁≡step₂ c) $
      _≃_.to (equiv bl) c .coherent

    ≡to : ∀ bl c → _≃_.to (equiv bl) c P.≡ to bl c
    ≡to bl c i .property = to-Coherently-cong-≡-property
                             bl univ P₁≃P₂ step₁≡step₂ c i
    ≡to bl c i .coherent = lemma i
      where
      lemma :
        P.[ (λ i → Coherently P₂ step₂
                     (step₂ f
                        (to-Coherently-cong-≡-property
                           bl univ P₁≃P₂ step₁≡step₂ c i))) ]
          _≃_.to (equiv bl) c .coherent ≡
          P.subst
            (Coherently P₂ step₂)
            (P.cong (step₂ f) $
             to-Coherently-cong-≡-property bl univ P₁≃P₂ step₁≡step₂ c)
            (_≃_.to (equiv bl) c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

    from :
      Block "Coherently-cong-≡" →
      Coherently P₂ step₂ f → Coherently P₁ step₁ f
    from _  c .property = _≃_.from (P₁≃P₂ f) (c .property)
    from bl c .coherent =
      P.subst
        (Coherently P₁ step₁)
        (P.cong (step₁ f) $
         from-Coherently-cong-≡-property bl univ P₁≃P₂ step₁≡step₂ c) $
      _≃_.from (equiv bl) c .coherent

    ≡from : ∀ bl c → _≃_.from (equiv bl) c P.≡ from bl c
    ≡from bl c i .property = from-Coherently-cong-≡-property
                               bl univ P₁≃P₂ step₁≡step₂ c i
    ≡from bl c i .coherent = lemma i
      where
      lemma :
        P.[ (λ i → Coherently P₁ step₁
                     (step₁ f
                        (from-Coherently-cong-≡-property
                           bl univ P₁≃P₂ step₁≡step₂ c i))) ]
          _≃_.from (equiv bl) c .coherent ≡
          P.subst
            (Coherently P₁ step₁)
            (P.cong (step₁ f) $
             from-Coherently-cong-≡-property
               bl univ P₁≃P₂ step₁≡step₂ c)
            (_≃_.from (equiv bl) c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

  -- Unit tests that ensure that Coherently-cong-≃ computes the
  -- property fields in certain ways.

  module _
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
    {f : A → B}
    {univ : Univalence p}
    {P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f}
    {step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x}
    where

    _ :
      {c : Coherently P₁ step₁ f} →
      _≃_.to (Coherently-cong-≃ univ P₁≃P₂ step₁≡step₂) c .property ≡
      _≃_.to (P₁≃P₂ f) (c .property)
    _ = refl _

    _ :
      {c : Coherently P₂ step₂ f} →
      _≃_.from (Coherently-cong-≃ {step₁ = step₁} univ
                  P₁≃P₂ step₁≡step₂)
        c .property ≡
      _≃_.from (P₁≃P₂ f) (c .property)
    _ = refl _

  -- A lemma involving Coherently and ↑.

  Coherently-↑ :
    {A : Type a}
    {P : {A : Type a} → (A → B) → Type p}
    {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
    {f : A → B} →
    Coherently (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f ≃
    Coherently P step f
  Coherently-↑ {ℓ = ℓ} {P = P} {step = step} =
    Eq.↔→≃
      to
      from
      (_↔_.from ≡↔≡ ∘ to-from)
      (_↔_.from ≡↔≡ ∘ from-to)
    where
    to :
      Coherently (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f →
      Coherently P step f
    to c .property = lower (c .property)
    to c .coherent = to (c .coherent)

    from :
      Coherently P step f →
      Coherently (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f
    from c .property = lift (c .property)
    from c .coherent = from (c .coherent)

    to-from :
      (c : Coherently P step f) →
      to (from c) P.≡ c
    to-from c i .property = c .property
    to-from c i .coherent = to-from (c .coherent) i

    from-to :
      (c : Coherently (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f) →
      from (to c) P.≡ c
    from-to c i .property = c .property
    from-to c i .coherent = from-to (c .coherent) i

-- A preservation lemma for Coherently.
--
-- The two directions of this equivalence compute the property
-- fields in certain ways, see the "unit tests" below.

Coherently-cong :
  {A : Type a}
  {P₁ : {A : Type a} → (A → B) → Type p₁}
  {P₂ : {A : Type a} → (A → B) → Type p₂}
  {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
  {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
  {f : A → B} →
  Univalence (p₁ ⊔ p₂) →
  (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f) →
  ({A : Type a} (f : A → B) (x : P₂ f) →
   step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
  Coherently P₁ step₁ f ≃ Coherently P₂ step₂ f
Coherently-cong
  {p₁ = p₁} {p₂ = p₂}
  {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂} {f = f}
  univ P₁≃P₂ step₁≡step₂ =

  Coherently P₁ step₁ f                          ↝⟨ inverse Coherently-↑ ⟩

  Coherently (↑ p₂ ∘ P₁) ((_∘ lower) ∘ step₁) f  ↝⟨ Coherently-cong-≃
                                                      univ
                                                      (λ f →
    ↑ p₂ (P₁ f)                                          ↔⟨ B.↑↔ ⟩
    P₁ f                                                 ↝⟨ P₁≃P₂ f ⟩
    P₂ f                                                 ↔⟨ inverse B.↑↔ ⟩□
    ↑ p₁ (P₂ f)                                          □)
                                                      ((_∘ lower) ∘ step₁≡step₂) ⟩

  Coherently (↑ p₁ ∘ P₂) ((_∘ lower) ∘ step₂) f  ↝⟨ Coherently-↑ ⟩□

  Coherently P₂ step₂ f                          □

-- Unit tests that ensure that Coherently-cong computes the
-- property fields in certain ways.

module _
  {A : Type a}
  {P₁ : {A : Type a} → (A → B) → Type p₁}
  {P₂ : {A : Type a} → (A → B) → Type p₂}
  {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ → B}
  {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ → B}
  {f : A → B}
  {univ : Univalence (p₁ ⊔ p₂)}
  {P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f}
  {step₁≡step₂ :
     {A : Type a} (f : A → B) (x : P₂ f) →
     step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x}
  where

  _ :
    {c : Coherently P₁ step₁ f} →
    _≃_.to (Coherently-cong univ P₁≃P₂ step₁≡step₂) c .property ≡
    _≃_.to (P₁≃P₂ f) (c .property)
  _ = refl _

  _ :
    {c : Coherently P₂ step₂ f} →
    _≃_.from (Coherently-cong {step₁ = step₁} univ P₁≃P₂ step₁≡step₂)
      c .property ≡
    _≃_.from (P₁≃P₂ f) (c .property)
  _ = refl _

-- Another preservation lemma for Coherently.

Coherently-cong′ :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} →
  Univalence a →
  (A₁≃A₂ : A₁ ≃ A₂) →
  Coherently P step (f ∘ _≃_.to A₁≃A₂) ≃ Coherently P step f
Coherently-cong′ {f = f} {P = P} {step = step} univ A₁≃A₂ =
  ≃-elim₁ univ
    (λ A₁≃A₂ →
       Coherently P step (f ∘ _≃_.to A₁≃A₂) ≃
       Coherently P step f)
    Eq.id
    A₁≃A₂

------------------------------------------------------------------------
-- Another lemma

-- A "computation rule".

subst-Coherently-property :
  ∀ {A : C → Type a} {B : Type b}
    {P : C → {A : Type a} → (A → B) → Type p}
    {step : (c : C) {A : Type a} (f : A → B) → P c f → ∥ A ∥¹ → B}
    {f : (c : C) → A c → B} {eq : x ≡ y} {c} →
  subst (λ x → Coherently (P x) (step x) (f x)) eq c .property ≡
  subst (λ x → P x (f x)) eq (c .property)
subst-Coherently-property
  {P = P} {step = step} {f = f} {eq = eq} {c = c} =
  elim¹
    (λ eq →
       subst (λ x → Coherently (P x) (step x) (f x)) eq c .property ≡
       subst (λ x → P x (f x)) eq (c .property))
    (subst (λ x → Coherently (P x) (step x) (f x)) (refl _) c .property  ≡⟨ cong property $ subst-refl _ _ ⟩
     c .property                                                         ≡⟨ sym $ subst-refl _ _ ⟩∎
     subst (λ x → P x (f x)) (refl _) (c .property)                      ∎)
    eq

------------------------------------------------------------------------
-- Coherently-with-restriction

-- A variant of Coherently. An extra predicate Q is included, so that
-- one can restrict the "f" functions (and their domains).

record Coherently-with-restriction
         {A : Type a} {B : Type b}
         (P : {A : Type a} → (A → B) → Type p)
         (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B)
         (f : A → B)
         (Q : {A : Type a} → (A → B) → Type q)
         (pres : {A : Type a} {f : A → B} {p : P f} →
                 Q f → Q (step f p))
         (q : Q f) : Type p where
  coinductive
  field
    property : P f
    coherent :
      Coherently-with-restriction
        P step (step f property)
        Q pres (pres q)

open Coherently-with-restriction public

-- Coherently P step f is equivalent to
-- Coherently-with-restriction P step f Q pres q.

Coherently≃Coherently-with-restriction :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
  {f : A → B}
  {Q : {A : Type a} → (A → B) → Type q}
  {pres : {A : Type a} {f : A → B} {p : P f} → Q f → Q (step f p)}
  {q : Q f} →
  Coherently P step f ≃ Coherently-with-restriction P step f Q pres q
Coherently≃Coherently-with-restriction
  {P = P} {step = step} {Q = Q} {pres = pres} =
  Eq.↔→≃ to (from _)
    (λ c → _↔_.from ≡↔≡ (to-from c))
    (λ c → _↔_.from ≡↔≡ (from-to _ c))
  where
  to :
    Coherently P step f →
    Coherently-with-restriction P step f Q pres q
  to c .property = c .property
  to c .coherent = to (c .coherent)

  from :
    ∀ q →
    Coherently-with-restriction P step f Q pres q →
    Coherently P step f
  from _ c .property = c .property
  from _ c .coherent = from _ (c .coherent)

  to-from :
    (c : Coherently-with-restriction P step f Q pres q) →
    to (from q c) P.≡ c
  to-from c i .property = c .property
  to-from c i .coherent = to-from (c .coherent) i

  from-to : ∀ q (c : Coherently P step f) → from q (to c) P.≡ c
  from-to _ c i .property = c .property
  from-to q c i .coherent = from-to (pres q) (c .coherent) i

-- A container that is used to define Coherently-with-restriction′.

Coherently-with-restriction-container :
  {B : Type b}
  (P : {A : Type a} → (A → B) → Type p)
  (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
  (Q : {A : Type a} → (A → B) → Type q) →
  ({A : Type a} {f : A → B} {p : P f} → Q f → Q (step f p)) →
  Container (∃ λ (A : Type a) → ∃ λ (f : A → B) → Q f) p lzero
Coherently-with-restriction-container P step _ pres = λ where
  .Shape (_ , f , _)               → P f
  .Position _                      → ⊤
  .index {o = A , f , q} {s = p} _ → ∥ A ∥¹ , step f p , pres q

-- A variant of Coherently-with-restriction, defined using an indexed
-- container.

Coherently-with-restriction′ :
  {A : Type a} {B : Type b}
  (P : {A : Type a} → (A → B) → Type p)
  (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
  (f : A → B) →
  (Q : {A : Type a} → (A → B) → Type q) →
  ({A : Type a} {f : A → B} {p : P f} → Q f → Q (step f p)) →
  Q f →
  Type (lsuc a ⊔ b ⊔ p ⊔ q)
Coherently-with-restriction′ P step f Q pres q =
  M (Coherently-with-restriction-container P step Q pres) (_ , f , q)

-- Coherently-with-restriction P step f Q pres q is equivalent to
-- Coherently-with-restriction′ P step f Q pres q.

Coherently-with-restriction≃Coherently-with-restriction′ :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
  {f : A → B}
  {Q : {A : Type a} → (A → B) → Type q}
  {pres : {A : Type a} {f : A → B} {p : P f} → Q f → Q (step f p)}
  {q : Q f} →
  Coherently-with-restriction P step f Q pres q ≃
  Coherently-with-restriction′ P step f Q pres q
Coherently-with-restriction≃Coherently-with-restriction′
  {P = P} {step = step} {Q = Q} {pres = pres} =
  Eq.↔→≃ to (from _)
    (λ c → _↔_.from ≡↔≡ (to-from _ c))
    (λ c → _↔_.from ≡↔≡ (from-to c))
  where
  to :
    Coherently-with-restriction P step f Q pres q →
    Coherently-with-restriction′ P step f Q pres q
  to c .out-M .proj₁   = c .property
  to c .out-M .proj₂ _ = to (c .coherent)

  from :
    ∀ q →
    Coherently-with-restriction′ P step f Q pres q →
    Coherently-with-restriction P step f Q pres q
  from _ c .property = c .out-M .proj₁
  from _ c .coherent = from _ (c .out-M .proj₂ _)

  to-from :
    ∀ q (c : Coherently-with-restriction′ P step f Q pres q) →
    to (from q c) P.≡ c
  to-from _ c i .out-M .proj₁   = c .out-M .proj₁
  to-from q c i .out-M .proj₂ _ = to-from (pres q) (c .out-M .proj₂ _) i

  from-to :
    (c : Coherently-with-restriction P step f Q pres q) →
    from q (to c) P.≡ c
  from-to c i .property = c .property
  from-to c i .coherent = from-to (c .coherent) i

------------------------------------------------------------------------
-- H-levels

-- I think that Paolo Capriotti suggested that one could prove that
-- certain instances of Coherently have certain h-levels by using the
-- result (due to Ahrens, Capriotti and Spadotti, see "Non-wellfounded
-- trees in Homotopy Type Theory") that M-types for indexed containers
-- have h-level n if all shapes have h-level n. The use of containers
-- with "restrictions" is my idea.

-- If P f has h-level n for every function f for which Q holds, then
-- Coherently-with-restriction P step f Q pres q has h-level n
-- (assuming univalence).

H-level-Coherently-with-restriction :
  Univalence (lsuc a ⊔ b ⊔ p ⊔ q) →
  Univalence (lsuc a ⊔ b ⊔ q) →
  {B : Type b}
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
  {f : A → B}
  {Q : {A : Type a} → (A → B) → Type q}
  {pres : {A : Type a} {f : A → B} {p : P f} → Q f → Q (step f p)}
  {q : Q f} →
  ({A : Type a} {f : A → B} → Q f → H-level n (P f)) →
  H-level n (Coherently-with-restriction P step f Q pres q)
H-level-Coherently-with-restriction
  {n = n} univ₁ univ₂ {B = B} {P = P} {step = step} {f = f} {Q = Q}
  {pres = pres} {q = q} =

  (∀ {A} {f : A → B} → Q f → H-level n (P f))                        ↝⟨ (λ h (_ , _ , q) → h q) ⟩
  (((_ , f , _) : ∃ λ A → ∃ λ (f : A → B) → Q f) → H-level n (P f))  ↝⟨ (λ h → H-level-M univ₁ univ₂ h) ⟩
  H-level n (Coherently-with-restriction′ P step f Q pres q)         ↝⟨ H-level-cong _ n
                                                                          (inverse Coherently-with-restriction≃Coherently-with-restriction′) ⟩□
  H-level n (Coherently-with-restriction P step f Q pres q)          □

-- If P f has h-level n, and (for any f and p) P (step f p) has
-- h-level n when P f has h-level n, then Coherently P step f has
-- h-level n (assuming univalence).

H-level-Coherently :
  {B : Type b}
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B}
  {f : A → B} →
  Univalence (lsuc a ⊔ b ⊔ p) →
  H-level n (P f) →
  ({A : Type a} {f : A → B} {p : P f} →
   H-level n (P f) → H-level n (P (step f p))) →
  H-level n (Coherently P step f)
H-level-Coherently {n = n} {P = P} {step = step} {f = f} univ h₁ h₂ =
                                            $⟨ H-level-Coherently-with-restriction univ univ id ⟩
  H-level n
    (Coherently-with-restriction P step f
       (λ f → H-level n (P f)) h₂ h₁)       ↝⟨ H-level-cong _ n (inverse Coherently≃Coherently-with-restriction) ⦂ (_ → _) ⟩□

  H-level n (Coherently P step f)           □

-- A variant of H-level-Coherently for type-valued functions.

H-level-Coherently-→Type :
  {P : {A : Type a} → (A → Type f) → Type p}
  {step : {A : Type a} (F : A → Type f) → P F → ∥ A ∥¹ → Type f}
  {F : A → Type f} →
  Univalence (lsuc a ⊔ p ⊔ lsuc f) →
  Univalence (lsuc (a ⊔ f)) →
  ((a : A) → H-level n (F a)) →
  ({A : Type a} {F : A → Type f} →
   ((a : A) → H-level n (F a)) → H-level n (P F)) →
  ({A : Type a} {F : A → Type f} {p : P F} →
   ((a : A) → H-level n (F a)) →
   (a : A) → H-level n (step F p ∣ a ∣)) →
  H-level n (Coherently P step F)
H-level-Coherently-→Type
  {a = a} {f = f} {n = n} {P = P} {step = step} {F = F}
  univ₁ univ₂ h₁ h₂ h₃ =
                                              $⟨ H-level-Coherently-with-restriction univ₁ univ₂ h₂ ⟩
  H-level n
    (Coherently-with-restriction P step F
       (λ F → ∀ a → H-level n (F a)) h₃′ h₁)  ↝⟨ H-level-cong _ n (inverse Coherently≃Coherently-with-restriction) ⦂ (_ → _) ⟩□

  H-level n (Coherently P step F)             □
  where
  h₃′ :
    {A : Type a} {F : A → Type f} {p : P F} →
    ((a : A) → H-level n (F a)) →
    (a : ∥ A ∥¹) → H-level n (step F p a)
  h₃′ h = O.elim λ where
    .O.∣∣ʳ              → h₃ h
    .O.∣∣-constantʳ _ _ → H-level-propositional ext n _ _

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module Haskell.Prim.Real where

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Enum
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.Int
open import Haskell.Prim.Integer

-- infixr 8  _^_ _^^_
-- infixl 7  _/_ _`quot`_ _`rem`_ _`div`_ _`mod`_
-- infixl 7  _%_

data Ratio (a : Set) : Set where
    _:%_ : a -> a -> Ratio a

record Integral (a : Set) : Set where
  field
    toInteger : a -> Integer

open Integral ⦃ ... ⦄ public

instance
    isIntegralInt : Integral Int
    isIntegralInt . toInteger n = intToInteger n

infinity : Ratio Integer
notANumber : Ratio Integer
infinity   = (toInteger 1) :% (toInteger 0)
notANumber = (toInteger 0) :% (toInteger 0)

-- _%_ : {{Integral a}} -> a -> a -> Ratio a

numerator : Ratio a -> a

denominator : Ratio a -> a

-- reduce : {{Integral a}} -> a -> a -> Ratio a

numerator (x :% _) =  x
denominator (_ :% y) =  y

-- record Real {Num a} (a : Set) : Set where
--   field
--     toRational : a -> Ratio Integer


text:
------------------------------------------------------------------------------
-- The gcd is commutative
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Program.GCD.Total.CommutativeI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Program.GCD.Total.ConversionRulesI
open import FOTC.Program.GCD.Total.GCD

------------------------------------------------------------------------------
-- Informal proof:
-- 1. gcd 0 n = n        -- gcd def
--            = gcd n 0  -- gcd def

-- 2. gcd n 0 = n        -- gcd def
--            = gcd 0 n  -- gcd def

-- 3.1. Case: S m > S n
-- gcd (S m) (S n) = gcd (S m - S n) (S n)  -- gcd def
--                 = gcd (S n) (S m - S n)  -- IH
--                 = gcd (S n) (S m)        -- gcd def

-- 3.2. Case: S m ≮ S n
-- gcd (S m) (S n) = gcd (S m) (S n - S m)  -- gcd def
--                 = gcd (S n - S m) (S m)  -- IH
--                 = gcd (S n) (S m)        -- gcd def

------------------------------------------------------------------------------
-- Commutativity property.
Comm : D → D → Set
Comm t t' = gcd t t' ≡ gcd t' t
{-# ATP definition Comm #-}

x>y→y≯x : ∀ {m n} → N m → N n → m > n → n ≯ m
x>y→y≯x nzero          Nn             0>n   = ⊥-elim (0>x→⊥ Nn 0>n)
{-# CATCHALL #-}
x>y→y≯x Nm             nzero          _     = 0≯x Nm
x>y→y≯x (nsucc {m} Nm) (nsucc {n} Nn) Sm>Sn =
  trans (lt-SS m n) (x>y→y≯x Nm Nn (trans (sym (lt-SS n m)) Sm>Sn))

postulate x≯Sy→Sy>x : ∀ {m n} → N m → N n → m ≯ succ₁ n → succ₁ n > m
-- x≯Sy→Sy>x {n = n} nzero      Nn _ = <-0S n
-- x≯Sy→Sy>x {n = n} (nsucc {m} Nm) Nn h = {!!}

------------------------------------------------------------------------------
-- gcd 0 0 is commutative.
gcd-00-comm : Comm zero zero
gcd-00-comm = refl

------------------------------------------------------------------------------
-- gcd (succ₁ n) 0 is commutative.
gcd-S0-comm : ∀ n → Comm (succ₁ n) zero
gcd-S0-comm n = trans (gcd-S0 n) (sym (gcd-0S n))

------------------------------------------------------------------------------
-- gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is commutative.
gcd-S>S-comm : ∀ {m n} → N m → N n →
               Comm (succ₁ m ∸ succ₁ n) (succ₁ n) →
               succ₁ m > succ₁ n →
               Comm (succ₁ m) (succ₁ n)
gcd-S>S-comm {m} {n} Nm Nn ih Sm>Sn =
  gcd (succ₁ m) (succ₁ n)
    ≡⟨ gcd-S>S m n Sm>Sn ⟩
  gcd (succ₁ m ∸ succ₁ n) (succ₁ n)
    ≡⟨ ih ⟩
  gcd (succ₁ n) (succ₁ m ∸ succ₁ n)
    ≡⟨ sym (gcd-S≯S n m (x>y→y≯x (nsucc Nm) (nsucc Nn) Sm>Sn)) ⟩
  gcd (succ₁ n) (succ₁ m) ∎

------------------------------------------------------------------------------
-- gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is commutative.
gcd-S≯S-comm : ∀ {m n} → N m → N n →
               Comm (succ₁ m) (succ₁ n ∸ succ₁ m) →
               succ₁ m ≯ succ₁ n →
               Comm (succ₁ m) (succ₁ n)
gcd-S≯S-comm {m} {n} Nm Nn ih Sm≯Sn =
  gcd (succ₁ m) (succ₁ n)
    ≡⟨ gcd-S≯S m n Sm≯Sn ⟩
  gcd (succ₁ m) (succ₁ n ∸ succ₁ m)
    ≡⟨ ih ⟩
  gcd (succ₁ n ∸ succ₁ m) (succ₁ m)
    ≡⟨ sym (gcd-S>S n m (x≯Sy→Sy>x (nsucc Nm) Nn Sm≯Sn)) ⟩
  gcd (succ₁ n) (succ₁ m) ∎

------------------------------------------------------------------------------
-- gcd m n when m > n is commutative.
gcd-x>y-comm :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → Comm o p) →
  m > n →
  Comm m n
gcd-x>y-comm nzero          Nn             _  0>n   = ⊥-elim (0>x→⊥ Nn 0>n)
gcd-x>y-comm (nsucc {n} _)  nzero          _  _     = gcd-S0-comm n
gcd-x>y-comm (nsucc {m} Nm) (nsucc {n} Nn) ah Sm>Sn = gcd-S>S-comm Nm Nn ih Sm>Sn
  where
  -- Inductive hypothesis.
  ih : Comm (succ₁ m ∸ succ₁ n) (succ₁ n)
  ih = ah {succ₁ m ∸ succ₁ n}
          {succ₁ n}
          (∸-N (nsucc Nm) (nsucc Nn))
          (nsucc Nn)
          ([Sx∸Sy,Sy]<[Sx,Sy] Nm Nn)

------------------------------------------------------------------------------
-- gcd m n when m ≯ n is commutative.
gcd-x≯y-comm :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → Comm o p) →
  m ≯ n →
  Comm m n
gcd-x≯y-comm nzero          nzero          _  _     = gcd-00-comm
gcd-x≯y-comm nzero          (nsucc {n} _)  _  _     = sym (gcd-S0-comm n)
gcd-x≯y-comm (nsucc _)      nzero          _  Sm≯0  = ⊥-elim (S≯0→⊥ Sm≯0)
gcd-x≯y-comm (nsucc {m} Nm) (nsucc {n} Nn) ah Sm≯Sn = gcd-S≯S-comm Nm Nn ih Sm≯Sn
  where
  -- Inductive hypothesis.
  ih : Comm (succ₁ m) (succ₁ n ∸ succ₁ m)
  ih = ah {succ₁ m}
          {succ₁ n ∸ succ₁ m}
          (nsucc Nm)
          (∸-N (nsucc Nn) (nsucc Nm))
          ([Sx,Sy∸Sx]<[Sx,Sy] Nm Nn)

------------------------------------------------------------------------------
-- gcd is commutative.
gcd-comm : ∀ {m n} → N m → N n → Comm m n
gcd-comm = Lexi-wfind A h
  where
  A : D → D → Set
  A i j = Comm i j

  h : ∀ {i j} → N i → N j → (∀ {k l} → N k → N l → Lexi k l i j → A k l) →
      A i j
  h Ni Nj ah = case (gcd-x>y-comm Ni Nj ah)
                    (gcd-x≯y-comm Ni Nj ah)
                    (x>y∨x≯y Ni Nj)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-#  OPTIONS --type-in-type #-}
module TooFewArgsWrongType where

open import AgdaPrelude

myFun : Vec Nat Zero -> Nat -> Nat
myFun x y = y

myApp : Nat
myApp = (myFun Zero)

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module HoleFilling where

data Bool : Set where
  false : Bool
  true  : Bool

_∧_ : Bool → Bool → Bool
false ∧ b = false
true ∧ b  = b

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
open import Agda.Builtin.Nat

record R : Set where
  field
    x : Nat

open R {{...}}

f₁ f₂ : R

-- This is fine.
x ⦃ f₁ ⦄ = 0

-- WAS: THIS WORKS BUT MAKES NO SENSE!!!
f₂ ⦃ .x ⦄ = 0

-- Error:

-- Cannot eliminate type R with pattern ⦃ .x ⦄ (suggestion: write .(x)
-- for a dot pattern, or remove the braces for a postfix projection)
-- when checking the clause left hand side
-- f₂ ⦃ .x ⦄

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module _ where

postulate
  F : Set → Set
  A : Set

module A (X : Set) where
  postulate T : Set

module B where
  private module M = A A
  open M
  postulate t : F T

postulate
  op : {A : Set} → A → A → A

open A A

foo : F T
foo = op B.t {!!}   -- ?0 : F .ReduceNotInScope.B.M.T

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Formalization.ClassicalPropositionalLogic.Syntax where

import      Lvl
open import Functional
open import Sets.PredicateSet using (PredSet)
open import Type

private variable ℓₚ ℓ : Lvl.Level

module _ (P : Type{ℓₚ}) where
  -- Formulas.
  -- Inductive definition of the grammatical elements of the language of propositional logic.
  -- Note: It is possible to reduce the number of formula variants to for example {•,¬,∨} or {•,¬,∧} (This is called propositional adequacy/functional completeness).
  data Formula : Type{ℓₚ} where
    •_ : P → Formula -- Propositional constants

    ⊤ : Formula -- Tautology (Top / True)
    ⊥ : Formula -- Contradiction (Bottom / False)

    ¬_ : Formula → Formula -- Negation (Not)

    _∧_ : Formula → Formula → Formula -- Conjunction (And)
    _∨_ : Formula → Formula → Formula -- Disjunction (Or)
    _⟶_ : Formula → Formula → Formula -- Implication
    _⟷_ : Formula → Formula → Formula -- Equivalence

  Formulas : Type{ℓₚ Lvl.⊔ Lvl.𝐒(ℓ)}
  Formulas{ℓ} = PredSet{ℓ}(Formula)

  infix 1011 •_
  infix 1010 ¬_ ¬¬_
  infixr 1005 _∧_
  infixr 1004 _∨_
  infixr 1000 _⟷_ _⟶_

module _ {P : Type{ℓₚ}} where
  -- Double negation
  -- ¬¬_ : Formula(P) → Formula(P)
  -- ¬¬_ : (¬_) ∘ (¬_)

  -- Reverse implication
  _⟵_ : Formula(P) → Formula(P) → Formula(P)
  _⟵_ = swap(_⟶_)

  -- (Nor)
  _⊽_ : Formula(P) → Formula(P) → Formula(P)
  _⊽_ = (¬_) ∘₂ (_∨_)

  -- (Nand)
  _⊼_ : Formula(P) → Formula(P) → Formula(P)
  _⊼_ = (¬_) ∘₂ (_∧_)

  -- (Exclusive or / Xor)
  _⊻_ : Formula(P) → Formula(P) → Formula(P)
  _⊻_ = (¬_) ∘₂ (_⟷_)

  infixl 1000 _⟵_


text:
-- 2010-10-15

module Issue331 where

record ⊤ : Set where
  constructor tt

data Wrap (I : Set) : Set where
  wrap : I → Wrap I

data B (I : Set) : Wrap I → Set₁ where
  b₁ : ∀ i → B I (wrap i)
  b₂ : {w : Wrap I} → B I w → B I w
  b₃ : (X : Set){w : Wrap I}(f : X → B I w) → B I w

ok : B ⊤ (wrap tt)
ok = b₂ (b₁ _)

-- Issue 331 was: Unsolved meta: _45 : ⊤
bad : Set → B ⊤ (wrap tt)
bad X = b₃ X λ x → b₁ _


text:
open import guarded-recursion.prelude

module guarded-recursion.model where

-- ℂʷᵒᵖ (ℂ^{ω}^{op})
-- Notation:
--   For the category ℂ we use superscript 'c' to disambiguate (e.g. _→ᶜ_)
--   We use ᵖ for the presheaf category.
module Presheaf
  {o m}
  (Objᶜ : Type_ o)
  (_→ᶜ_ : Objᶜ → Objᶜ → Type_ m)
  (idᶜ  : {A : Objᶜ} → A →ᶜ A)
  (_∘ᶜ_ : {A B C : Objᶜ} → (B →ᶜ C) → (A →ᶜ B) → (A →ᶜ C))
  (∘-idᶜ : {A B : Objᶜ} {f : A →ᶜ B} → f ∘ᶜ idᶜ ≡ f)
  (id-∘ᶜ : {A B : Objᶜ} {f : A →ᶜ B} → idᶜ ∘ᶜ f ≡ f)
  (∘-assocᶜ : {A B C D : Objᶜ}
              {f : C →ᶜ D} {g : B →ᶜ C} {h : A →ᶜ B}
              → (f ∘ᶜ g) ∘ᶜ h ≡ f ∘ᶜ (g ∘ᶜ h))
  (𝟙ᶜ : Objᶜ)
  (!ᶜ : {A : Objᶜ} → A →ᶜ 𝟙ᶜ)
  (!-uniqᶜ : {A : Objᶜ} {f : A →ᶜ 𝟙ᶜ} → f ≡ !ᶜ)
  where

  -- Index preserving maps
  _→ᶜ°_ : (A B : ℕ → Objᶜ) → Type_ _
  A →ᶜ° B = (n : ℕ) → A n →ᶜ B n

  Endoᶜ° : (ℕ → Objᶜ) → Type_ _
  Endoᶜ° A = A →ᶜ° A

  -- Restriction maps
  Rmap : (ℕ → Objᶜ) → Type_ _
  Rmap A = (A ∘ S) →ᶜ° A

  Objᵖ : Type_ _
  Objᵖ = Σ (ℕ → Objᶜ) Rmap

  _→ᵖ_ : Objᵖ → Objᵖ → Type_ _
  (A , rᴬ) →ᵖ (B , rᴮ) = Σ (A →ᶜ° B) λ f →
                           (n : ℕ) → f n ∘ᶜ rᴬ n ≡ rᴮ n ∘ᶜ f (1 + n)

  [_]ᵖ : Objᶜ → Objᵖ
  [ A ]ᵖ = (λ _ → A) , (λ _ → idᶜ)

  ⟨_⟩ᵖ : {A B : Objᶜ} → A →ᶜ B → [ A ]ᵖ →ᵖ [ B ]ᵖ
  ⟨ f ⟩ᵖ = (λ _ → f) , (λ n → ∘-idᶜ ∙ ! id-∘ᶜ)

  idᵖ : {A : Objᵖ} → A →ᵖ A
  idᵖ = (λ n → idᶜ) , (λ n → id-∘ᶜ ∙ ! ∘-idᶜ)

  {-
      B ---f--> D
      ^         ^
      |         |
      g         h
      |         |
      A ---i--> C
  -}
  module _ {A B C D}
           (f : B →ᶜ D) (g : A →ᶜ B)
           (h : C →ᶜ D) (i : A →ᶜ C) where
    Squareᶜ = f ∘ᶜ g ≡ h ∘ᶜ i

  module _ {A B C} {f f' : B →ᶜ C} {g g'  : A →ᶜ B} where
    ap-∘ᶜ  : f ≡ f' → g ≡ g' → f ∘ᶜ g ≡ f' ∘ᶜ g'
    ap-∘ᶜ p q = ap (λ x → x ∘ᶜ g) p ∙ ap (_∘ᶜ_ f') q

  !-irrᶜ : {A : Objᶜ} {f g : A →ᶜ 𝟙ᶜ} → f ≡ g
  !-irrᶜ = !-uniqᶜ ∙ ! !-uniqᶜ

  ∘-!ᶜ : {A : Objᶜ} {f : 𝟙ᶜ →ᶜ A} { !g : 𝟙ᶜ →ᶜ 𝟙ᶜ} → f ∘ᶜ !g ≡ f
  ∘-!ᶜ = ap-∘ᶜ idp !-irrᶜ ∙ ∘-idᶜ

  with-∘-assocᶜ : {A B C C' D : Objᶜ}
              {f  : C  →ᶜ D} {g  : B →ᶜ C}
              {f' : C' →ᶜ D} {g' : B →ᶜ C'}
              {h : A →ᶜ B}
              → f ∘ᶜ g ≡ f' ∘ᶜ g'
              → f ∘ᶜ (g ∘ᶜ h) ≡ f' ∘ᶜ (g' ∘ᶜ h)
  with-∘-assocᶜ p = ! ∘-assocᶜ ∙ ap-∘ᶜ p idp ∙ ∘-assocᶜ

  with-!∘-assocᶜ : {A B B' C D : Objᶜ}
              {f  : C  →ᶜ D}
              {g  : B  →ᶜ C} {h : A →ᶜ B}
              {g' : B' →ᶜ C} {h' : A →ᶜ B'}
              → g ∘ᶜ h ≡ g' ∘ᶜ h'
              → (f ∘ᶜ g) ∘ᶜ h ≡ (f ∘ᶜ g') ∘ᶜ h'
  with-!∘-assocᶜ p = ∘-assocᶜ ∙ ap-∘ᶜ idp p ∙ ! ∘-assocᶜ

  {-
      B ---f--> D ---e--> F
      ^         ^         ^
      |         |         |
      g    L    h    R    j
      |         |         |
      A ---i--> C ---k--> E
  -}
  module _
           {A B C D E F}
           {f : B →ᶜ D} {g : A →ᶜ B}
           {h : C →ᶜ D} {i : A →ᶜ C}
           {e : D →ᶜ F}
           {j : E →ᶜ F} {k : C →ᶜ E}
           (L : Squareᶜ f g h i)
           (R : Squareᶜ e h j k) where

      private
        efg-ehi : (e ∘ᶜ f) ∘ᶜ g ≡ e ∘ᶜ (h ∘ᶜ i)
        efg-ehi = ∘-assocᶜ ∙ ap-∘ᶜ idp L

        ehi-jki : e ∘ᶜ (h ∘ᶜ i) ≡ j ∘ᶜ (k ∘ᶜ i)
        ehi-jki = ! ∘-assocᶜ ∙ ap-∘ᶜ R idp ∙ ∘-assocᶜ

      LR : Squareᶜ (e ∘ᶜ f) g j (k ∘ᶜ i)
      LR = efg-ehi ∙ ehi-jki

  {-
                    X
                  / . \
                /   .   \
              /     .     \
           f/       .u!     \g
          /         .         \
        v           v           v
      A <---fst--- A×B ---snd---> B
  -}
  module _
     {A B A×B X : Objᶜ}
     {fstᶜ   : A×B →ᶜ A}
     {sndᶜ   : A×B →ᶜ B}
     {f      : X →ᶜ A}
     {g      : X →ᶜ B}
     (u!     : X →ᶜ A×B)
     (fst-u! : fstᶜ ∘ᶜ u! ≡ f)
     (snd-u! : sndᶜ ∘ᶜ u! ≡ g)
     where
     1-ProductDiagram = fst-u! , snd-u!

  module ProductDiagram
     {A B A×B : Objᶜ}
     {fstᶜ : A×B →ᶜ A}
     {sndᶜ : A×B →ᶜ B}
     {<_,_>ᶜ : ∀ {X} → X →ᶜ A → X →ᶜ B → X →ᶜ A×B}
     (fst-<,> : ∀ {X} {f : X →ᶜ A} {g : X →ᶜ B}
                → fstᶜ ∘ᶜ < f , g >ᶜ ≡ f)
     (snd-<,> : ∀ {X} {f : X →ᶜ A} {g : X →ᶜ B}
                → sndᶜ ∘ᶜ < f , g >ᶜ ≡ g)
     (<,>-uniq! : ∀ {A B X : Objᶜ} {f : X →ᶜ A×B}
                  → < fstᶜ ∘ᶜ f , sndᶜ ∘ᶜ f >ᶜ ≡ f)
     where

     module _ {X} {f : X →ᶜ A} {g : X →ᶜ B} where
        1-productDiagram = 1-ProductDiagram < f , g >ᶜ fst-<,> snd-<,>

  infixr 9 _∘ᵖ_
  _∘ᵖ_ : {A B C : Objᵖ} → (B →ᵖ C) → (A →ᵖ B) → (A →ᵖ C)
  (f , ☐f) ∘ᵖ (g , ☐g) = (λ n → f n ∘ᶜ g n)
                       , (λ n → LR (☐g n) (☐f n))

  -- TODO: the real thing™
  _≡ᵖ_ : {A B : Objᵖ} (f g : A →ᵖ B) → Type_ _
  (f , _) ≡ᵖ (g , _) = ∀ n → f n ≡ g n
  infix 2 _≡ᵖ_

  ∘-idᵖ : {A B : Objᵖ} {f : A →ᵖ B} → f ∘ᵖ idᵖ ≡ᵖ f
  ∘-idᵖ _ = ∘-idᶜ

  id-∘ᵖ : {A B : Objᵖ} {f : A →ᵖ B} → idᵖ ∘ᵖ f ≡ᵖ f
  id-∘ᵖ _ = id-∘ᶜ

  ∘-assocᵖ : {A B C D : Objᵖ}
             {f : C →ᵖ D} {g : B →ᵖ C} {h : A →ᵖ B}
             → (f ∘ᵖ g) ∘ᵖ h ≡ᵖ f ∘ᵖ (g ∘ᵖ h)
  ∘-assocᵖ _ = ∘-assocᶜ

  𝟙ᵖ : Objᵖ
  𝟙ᵖ = (λ _ → 𝟙ᶜ) , (λ _ → idᶜ)
  !ᵖ : {A : Objᵖ} → A →ᵖ 𝟙ᵖ
  !ᵖ = (λ _ → !ᶜ) , (λ _ → !-irrᶜ)
  !-uniqᵖ : {A : Objᵖ} {f : A →ᵖ 𝟙ᵖ} → f ≡ᵖ !ᵖ
  !-uniqᵖ _ = !-uniqᶜ

  ▸ : Objᵖ → Objᵖ
  ▸ (A , rᴬ) = ▸A , ▸rᴬ
     module Later where
       ▸A : ℕ → Objᶜ
       ▸A 0     = 𝟙ᶜ
       ▸A (S n) = A n
       ▸rᴬ : (n : ℕ) → ▸A (1 + n) →ᶜ ▸A n
       ▸rᴬ 0     = !ᶜ
       ▸rᴬ (S n) = rᴬ n

  -- ▸ functor action on morphisms
  ▸[_] : {A B : Objᵖ} → (A →ᵖ B) → ▸ A →ᵖ ▸ B
  ▸[_] {A , rᴬ} {B , rᴮ} (f , ☐) = ▸f , ▸☐
     module Later[] where
       open Later A rᴬ
       open Later B rᴮ renaming (▸A to ▸B; ▸rᴬ to ▸rᴮ)
       ▸f : ▸A →ᶜ° ▸B
       ▸f 0     = !ᶜ
       ▸f (S n) = f n
       ▸☐ : (n : ℕ) → ▸f n ∘ᶜ ▸rᴬ n ≡ ▸rᴮ n ∘ᶜ ▸f (1 + n)
       ▸☐ 0     = !-irrᶜ
       ▸☐ (S n) = ☐ n

  ▸-id : {A : Objᵖ}
       → ▸[ idᵖ {A} ] ≡ᵖ idᵖ
  ▸-id 0     = !-irrᶜ
  ▸-id (S n) = idp

  ▸-∘ : {A B C : Objᵖ} {f : B →ᵖ C} {g : A →ᵖ B}
      → ▸[ f ∘ᵖ g ] ≡ᵖ ▸[ f ] ∘ᵖ ▸[ g ]
  ▸-∘ 0     = !-irrᶜ
  ▸-∘ (S n) = idp

  {-
  ▸-[]ᵖ : {A : Objᶜ} → ▸ [ A ]ᵖ →ᵖ [ A ]ᵖ
  ▸-[]ᵖ {A} = ▸f , ▸☐
    where
      open Later (λ _ → A) (λ _ → idᶜ)
      ▸f : ▸A →ᶜ° (λ _ → A)
      ▸f O     = {!!}
      ▸f (S n) = idᶜ
      ▸☐ : (n : ℕ) → ▸f n ∘ᶜ ▸rᴬ n ≡ idᶜ ∘ᶜ ▸f (1 + n)
      ▸☐ O     = {!!}
      ▸☐ (S n) = idp
  -}

  next : {A : Objᵖ} → A →ᵖ ▸ A
  next {A , rᴬ} = f , ☐
     module Next where
       open Later A rᴬ
       f : (n : ℕ) → A n →ᶜ ▸A n
       f 0     = !ᶜ
       f (S n) = rᴬ n

       ☐ : (n : ℕ) → f n ∘ᶜ rᴬ n ≡ ▸rᴬ n ∘ᶜ f (1 + n)
       ☐ 0     = idp
       ☐ (S n) = idp

  next-nat : {A B : Objᵖ} {f : A →ᵖ B} → ▸[ f ] ∘ᵖ next ≡ᵖ next ∘ᵖ f
  next-nat             0     = !-irrᶜ
  next-nat {f = f , ☐} (S n) = ☐ n

  module _ {A : Objᵖ} (f : A →ᵖ A) where
    Contractive = Σ (▸ A →ᵖ A) λ g → f ≡ᵖ g ∘ᵖ next

  module _ {A B : Objᶜ} {i : B →ᶜ B} {f : A →ᶜ B} where
    id-∘ᶜ' : i ≡ idᶜ → i ∘ᶜ f ≡ f
    id-∘ᶜ' p = ap-∘ᶜ p idp ∙ id-∘ᶜ
  module _ {A B : Objᶜ} {i : A →ᶜ A} {f : A →ᶜ B} where
    ∘-idᶜ' : i ≡ idᶜ → f ∘ᶜ i ≡ f
    ∘-idᶜ' p = ap-∘ᶜ idp p ∙ ∘-idᶜ

  fix1 : {A : Objᵖ} (f : ▸ A →ᵖ A) → 𝟙ᵖ →ᵖ A
  fix1 {A , rᴬ} (f , ☐) = fixf , λ n → ∘-idᶜ ∙ fix☐ n
    module Fix1 where
      open Later A rᴬ

      fixf : (n : ℕ) → 𝟙ᶜ →ᶜ A n
      fixf 0     = f 0
      fixf (S n) = f (S n) ∘ᶜ fixf n

      fix☐ : (n : ℕ) → fixf n ≡ rᴬ n ∘ᶜ fixf (1 + n)
      fix☐ 0     = ! ∘-!ᶜ             ∙ with-∘-assocᶜ (☐ 0)
      fix☐ (S n) = ap-∘ᶜ idp (fix☐ n) ∙ with-∘-assocᶜ (☐ (S n))

  module WithProducts
    (_×ᶜ_ : Objᶜ → Objᶜ → Objᶜ)
    -- projections
    (fstᶜ : ∀ {A B} → (A ×ᶜ B) →ᶜ A)
    (sndᶜ : ∀ {A B} → (A ×ᶜ B) →ᶜ B)
    -- injection (pair creation)
    (<_,_>ᶜ : ∀ {A B C} → A →ᶜ B → A →ᶜ C → A →ᶜ (B ×ᶜ C))
    -- computation rules
    (fst-<,> : ∀ {A B C} {f : A →ᶜ B} {g : A →ᶜ C}
               → fstᶜ ∘ᶜ < f , g >ᶜ ≡ f)
    (snd-<,> : ∀ {A B C} {f : A →ᶜ B} {g : A →ᶜ C}
               → sndᶜ ∘ᶜ < f , g >ᶜ ≡ g)
    -- universal property
    (<,>-uniq! : ∀ {A B X : Objᶜ} {f : X →ᶜ (A ×ᶜ B)}
                 → < fstᶜ ∘ᶜ f , sndᶜ ∘ᶜ f >ᶜ ≡ f)
    where

    firstᶜ : ∀ {A B C} → A →ᶜ B → (A ×ᶜ C) →ᶜ (B ×ᶜ C)
    firstᶜ f = < f ∘ᶜ fstᶜ , sndᶜ >ᶜ

    secondᶜ : ∀ {A B C} → B →ᶜ C → (A ×ᶜ B) →ᶜ (A ×ᶜ C)
    secondᶜ f = < fstᶜ , f ∘ᶜ sndᶜ >ᶜ

    <_×_>ᶜ : ∀ {A B C D} (f : A →ᶜ C) (g : B →ᶜ D) → (A ×ᶜ B) →ᶜ (C ×ᶜ D)
    < f × g >ᶜ = < f ∘ᶜ fstᶜ , g ∘ᶜ sndᶜ >ᶜ

    module _ {A B C} {f f' : A →ᶜ B} {g g' : A →ᶜ C} where
        ≡<_,_> : f ≡ f' → g ≡ g' → < f , g >ᶜ ≡ < f' , g' >ᶜ
        ≡< p , q > = ap (λ f → < f , g >ᶜ) p ∙ ap (λ g → < f' , g >ᶜ) q

    module _ {A B C X} {f₀ : A →ᶜ B} {f₁ : A →ᶜ C} {g : X →ᶜ A} where
        <,>-∘ : < f₀ , f₁ >ᶜ ∘ᶜ g ≡ < f₀ ∘ᶜ g , f₁ ∘ᶜ g >ᶜ
        <,>-∘ = ! <,>-uniq! ∙ ≡< ! ∘-assocᶜ ∙ ap-∘ᶜ fst-<,> idp
                               , ! ∘-assocᶜ ∙ ap-∘ᶜ snd-<,> idp >

    module _ {A B} where
        -- η-rule
        <fst,snd> : < fstᶜ , sndᶜ >ᶜ ≡ idᶜ {A ×ᶜ B}
        <fst,snd> = ≡< ! ∘-idᶜ , ! ∘-idᶜ > ∙ <,>-uniq!

        <fst,id∘snd> : < fstᶜ , idᶜ ∘ᶜ sndᶜ >ᶜ ≡ idᶜ {A ×ᶜ B}
        <fst,id∘snd> = ≡< idp , id-∘ᶜ > ∙ <fst,snd>

    _×ᶜ°_ : (A B : ℕ → Objᶜ) → ℕ → Objᶜ
    (A ×ᶜ° B) n = A n ×ᶜ B n

    _×ʳ_ : {A B : ℕ → Objᶜ} → Rmap A → Rmap B → Rmap (A ×ᶜ° B)
    (rᴬ ×ʳ rᴮ) n = < rᴬ n × rᴮ n >ᶜ

    _×ᵖ_ : Objᵖ → Objᵖ → Objᵖ
    (A , rᴬ) ×ᵖ (B , rᴮ) = (A ×ᶜ° B) , (rᴬ ×ʳ rᴮ)

    fstᵖ : ∀ {A B} → (A ×ᵖ B) →ᵖ A
    fstᵖ = (λ _ → fstᶜ) , (λ _ → fst-<,>)

    sndᵖ : ∀ {A B} → (A ×ᵖ B) →ᵖ B
    sndᵖ = (λ _ → sndᶜ) , (λ _ → snd-<,>)

    <_,_>ᵖ : ∀ {A B C} → A →ᵖ B → A →ᵖ C → A →ᵖ (B ×ᵖ C)
    <_,_>ᵖ {A , rᴬ} {B , rᴮ} {C , rᶜ} (f , f☐) (g , g☐) =
      (λ n → < f n , g n >ᶜ) ,
      (λ n → <,>-∘
           ∙ ≡< f☐ n ∙ ap-∘ᶜ idp (! fst-<,>) ∙ ! ∘-assocᶜ
              , g☐ n ∙ ap-∘ᶜ idp (! snd-<,>) ∙ ! ∘-assocᶜ >
           ∙ ! <,>-∘)

    firstᵖ : ∀ {A B C} → A →ᵖ B → (A ×ᵖ C) →ᵖ (B ×ᵖ C)
    firstᵖ f = < f ∘ᵖ fstᵖ , sndᵖ >ᵖ

    ▸-× : {A B : Objᵖ} → ▸(A ×ᵖ B) →ᵖ (▸ A ×ᵖ ▸ B)
    ▸-× {A , rᴬ} {B , rᴮ} = ▸f , ▸☐
      module LaterProduct where
          open Later A rᴬ
          open Later B rᴮ                 renaming (▸A to ▸B; ▸rᴬ to ▸rᴮ)
          open Later (A ×ᶜ° B) (rᴬ ×ʳ rᴮ) renaming (▸A to ▸AB; ▸rᴬ to ▸rᴬᴮ)
          ▸f : ▸AB →ᶜ° (▸A ×ᶜ° ▸B)
          ▸f 0     = < !ᶜ , !ᶜ >ᶜ
          ▸f (S n) = idᶜ
          ▸☐ : (n : ℕ) → ▸f n ∘ᶜ ▸rᴬᴮ n ≡ (▸rᴬ ×ʳ ▸rᴮ) n ∘ᶜ ▸f (1 + n)
          ▸☐ 0     = <,>-∘ ∙ ≡< !-irrᶜ , !-irrᶜ > ∙ ! ∘-idᶜ
          ▸☐ (S n) = id-∘ᶜ ∙ ! ∘-idᶜ

    _^_  : Objᶜ → ℕ → Objᶜ
    A ^ 0    = 𝟙ᶜ
    A ^(S n) = A ×ᶜ (A ^ n)

    fix : {A B : Objᵖ} (f : (B ×ᵖ ▸ A) →ᵖ A) → B →ᵖ A
    fix {A , rᴬ} {B , rᴮ} (f , ☐) = fixf , fix☐
     module Fix where
      open Later A rᴬ
      open Later B rᴮ renaming (▸A to ▸B; ▸rᴬ to ▸rᴮ)

      fixf : (n : ℕ) → B n →ᶜ A n
      fixf 0     = f 0 ∘ᶜ < idᶜ , !ᶜ >ᶜ
      fixf (S n) = f (S n) ∘ᶜ < idᶜ , fixf n ∘ᶜ rᴮ n >ᶜ

      fix☐ : (n : ℕ) → fixf n ∘ᶜ rᴮ n ≡ rᴬ n ∘ᶜ fixf (1 + n)
      fix☐ 0     = ∘-assocᶜ ∙ ap-∘ᶜ idp (<,>-∘ ∙ ≡< id-∘ᶜ ∙ ! (∘-idᶜ' fst-<,>) ∙ ! ∘-assocᶜ , !-irrᶜ > ∙ ! <,>-∘) ∙ with-∘-assocᶜ (☐ 0)
      fix☐ (S n) = ∘-assocᶜ ∙ ap-∘ᶜ idp (<,>-∘ ∙ ≡< id-∘ᶜ ∙ ! (∘-idᶜ' fst-<,>) ∙ ! ∘-assocᶜ , h      > ∙ ! <,>-∘) ∙ with-∘-assocᶜ (☐ (S n))
        where h = ap-∘ᶜ (fix☐ n) idp ∙ with-!∘-assocᶜ (! snd-<,>)

    module _ {A} where
        initᶜ : ∀ n → (A ^(1 + n)) →ᶜ (A ^ n)
        initᶜ 0     = !ᶜ
        initᶜ (S n) = secondᶜ (initᶜ n)

    module Str1
      (A    : Objᶜ)
      where

      Aᵖ = [ A ]ᵖ

      Str : ℕ → Objᶜ
      Str n = A ^(1 + n)

      rStr : (n : ℕ) → Str (1 + n) →ᶜ Str n
      rStr = λ n → initᶜ (1 + n)

      Strᵖ : Objᵖ
      Strᵖ = Str , rStr

      open Later Str (snd Strᵖ) renaming (▸A to ▸Str; ▸rᴬ to ▸rStr)

      roll : (n : ℕ) → (A ^ n) →ᶜ ▸Str n
      roll 0     = !ᶜ -- or idᶜ {𝟙ᶜ}
      roll (S n) = idᶜ
      unroll : (n : ℕ) → ▸Str n →ᶜ (A ^ n)
      unroll 0     = !ᶜ -- or idᶜ {𝟙ᶜ}
      unroll (S n) = idᶜ

      hdᵖ : Strᵖ →ᵖ Aᵖ
      hdᵖ = (λ _ → fstᶜ) , (λ n → fst-<,> ∙ ! id-∘ᶜ)

      tlᵖ : Strᵖ →ᵖ ▸ Strᵖ
      tlᵖ = f , ☐
        where
          f : (n : ℕ) → Str n →ᶜ ▸Str n
          f n = roll n ∘ᶜ sndᶜ
          ☐ : (n : ℕ) → f n ∘ᶜ rStr n ≡ ▸rStr n ∘ᶜ f (1 + n)
          ☐ 0     = !-irrᶜ
          ☐ (S n) = ∘-assocᶜ ∙ id-∘ᶜ ∙ snd-<,> ∙ ap-∘ᶜ idp (! id-∘ᶜ)

      ∷ᵖ : (Aᵖ ×ᵖ ▸ Strᵖ) →ᵖ Strᵖ
      ∷ᵖ = f , ☐
        where
          f : (n : ℕ) → (A ×ᶜ ▸Str n) →ᶜ Str n
          f n = secondᶜ (unroll n)
          ☐ : (n : ℕ) → f n ∘ᶜ snd (Aᵖ ×ᵖ ▸ Strᵖ) n ≡ rStr n ∘ᶜ f (1 + n)
          ☐ 0     = <,>-∘ ∙ ≡< fst-<,> ∙ id-∘ᶜ , !-irrᶜ > ∙ !(∘-idᶜ' <fst,id∘snd>)
          ☐ (S n) = id-∘ᶜ' <fst,id∘snd> ∙ ≡< id-∘ᶜ , idp > ∙ !(∘-idᶜ' <fst,id∘snd>)

      repeatᵖ : (𝟙ᵖ →ᵖ Aᵖ) → 𝟙ᵖ →ᵖ Strᵖ
      repeatᵖ f = fix1 it
        where it : ▸ Strᵖ →ᵖ Strᵖ
              it = ∷ᵖ ∘ᵖ < f ∘ᵖ !ᵖ , idᵖ >ᵖ

      {-
      iterate f x = x ∷ iterate f (f x)
      or
      iterate f = (∷) id (iterate f ∘ f)
      -}
      {-
      iterateᵖ : (Aᵖ →ᵖ Aᵖ) → Aᵖ →ᵖ Strᵖ
      iterateᵖ f = fix it -- sndᵖ ∘ᵖ fix it ∘ᵖ !ᵖ
        where
           it : Aᵖ ×ᵖ ▸ Strᵖ →ᵖ Strᵖ
           it = < fstᵖ , ∷ᵖ >ᵖ ∘ᵖ firstᵖ (f ∘ᵖ {!!}) ∘ᵖ ▸-×
      -}

{-
      mapᵖ : ([ A ]ᵖ →ᵖ [ A ]ᵖ) → Strᵖ →ᵖ Strᵖ
      mapᵖ f = {!fix!}
-}

  Objᶜ↑ : ℕ → Endo (ℕ → Objᶜ)
  Objᶜ↑ k A n = A (n + k)

  ↑ᶜ° : ∀ k {A B} → A →ᶜ° B → Objᶜ↑ k A →ᶜ° Objᶜ↑ k B
  ↑ᶜ° k f n = f (n + k)

  ↑r : ∀ k {A} → Rmap A → Rmap (Objᶜ↑ k A)
  ↑r k rᴬ n = rᴬ (n + k)

  Objᵖ↑ : ℕ → Endo Objᵖ
  Objᵖ↑ k (A , rᴬ) = Objᶜ↑ k A , ↑r k rᴬ

  r* : {A : ℕ → Objᶜ}
       (rᴬ : Rmap A)
       (n : ℕ) → A (1 + n) →ᶜ A 0
  r* rᴬ 0     = rᴬ 0
  r* rᴬ (S n) = r* rᴬ n ∘ᶜ rᴬ (S n)

  module _
    {A B : ℕ → Objᶜ}
    {rᴬ  : (n : ℕ) → A (1 + n) →ᶜ A n}
    {rᴮ  : (n : ℕ) → B (1 + n) →ᶜ B n}
    (f   : (n : ℕ) → A n →ᶜ B n)
    (☐f  : (n : ℕ) → f n ∘ᶜ rᴬ n ≡ rᴮ n ∘ᶜ f (1 + n))
    where

    ☐* : (n : ℕ) → f 0 ∘ᶜ r* rᴬ n ≡ r* rᴮ n ∘ᶜ f (1 + n)
    ☐* 0     = ☐f 0
    ☐* (S n) = ! ∘-assocᶜ
             ∙ ap-∘ᶜ (☐* n) idp
             ∙ ∘-assocᶜ
             ∙ ap-∘ᶜ idp (☐f (S n))
             ∙ ! ∘-assocᶜ

  module _
    {A B : ℕ → Objᶜ}
    {rᴬ  : (n : ℕ) → A (1 + n) →ᶜ A n}
    {rᴮ  : (n : ℕ) → B (1 + n) →ᶜ B n}
    (f   : (n : ℕ) → A n →ᶜ B n)
    (☐f  : (n : ℕ) → f n ∘ᶜ rᴬ n ≡ rᴮ n ∘ᶜ f (1 + n))
    (k : ℕ)
    where

    --☐*' : (n : ℕ) → f k ∘ᶜ r* (↑r k rᴬ) n ≡ r* (↑r k rᴮ) n ∘ᶜ f ((1 + n) + k)
    --☐*' n = ☐* (↑ᶜ° k f) {!!} n

  module WithMore -- TODO upto topos
    -- Initial object
    (𝟘ᶜ : Objᶜ)
    (¡ᶜ : {A : Objᶜ} → 𝟘ᶜ →ᶜ A)
    (¡-uniqᶜ : {A : Objᶜ} {f : 𝟘ᶜ →ᶜ A} → ¡ᶜ ≡ f)

    -- Coproducts
    (_+ᶜ_ : Objᶜ → Objᶜ → Objᶜ)
    -- injections
    (inlᶜ : ∀ {A B} → A →ᶜ (A +ᶜ B))
    (inrᶜ : ∀ {A B} → B →ᶜ (A +ᶜ B))
    -- projection (coproduct elimination)
    ([_,_]ᶜ : ∀ {A B C} → B →ᶜ A → C →ᶜ A → (B +ᶜ C) →ᶜ A)
    -- computation rules
    ([,]-inl : ∀ {A B C} {f : B →ᶜ A} {g : C →ᶜ A}
               → [ f , g ]ᶜ ∘ᶜ inlᶜ ≡ f)
    ([,]-inr : ∀ {A B C} {f : B →ᶜ A} {g : C →ᶜ A}
               → [ f , g ]ᶜ ∘ᶜ inrᶜ ≡ g)
    -- universal property
    ([,]-uniq! : ∀ {A B X : Objᶜ} {f : (A +ᶜ B) →ᶜ X}
                 → [ f ∘ᶜ inlᶜ , f ∘ᶜ inrᶜ ]ᶜ ≡ f)
    where
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
module Nat where

open import Prelude
open import Star

Nat : Set
Nat = Star One _ _

zero : Nat
zero = ε

suc : Nat -> Nat
suc n = _ • n

infixl 50 _+_ _-_
infixl 60 _*_

_+_ : Nat -> Nat -> Nat
_+_ = _++_

_*_ : Nat -> Nat -> Nat
x * y = bind id (\ _ -> y) x

_-_ : Nat -> Nat -> Nat
n       - ε       = n
ε       - m       = ε
(_ • n) - (_ • m) = n - m

test : Nat
test = suc (suc zero) * suc (suc zero)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
data N : Set where
  Z : N
  suc : N -> N

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
open import Prelude

module RW.Data.RTrie.Decl where

  open import RW.Language.RTerm public
  open import RW.Language.RTermIdx public
  open import RW.Data.PMap (RTermᵢ ⊥) as IdxMap

  data Rule : Set where
    Gr : ℕ     → Rule
    Tr : ℕ → ℕ → Rule
    Fr : ℕ → Name → Rule

  mutual
    Cell : Set
    Cell = IdxMap.to RTrie default     -- Map from indexes to tries,
         × List (ℕ × List Rule) -- Binding symbols,

    data RTrie : Set where
        Fork : List Cell → RTrie
        Leaf : List Rule → RTrie

  BTrieEmpty : RTrie
  BTrieEmpty = Fork $ []

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


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

module TypeEquivCat where

-- We will define a rig category whose objects are types and whose
-- morphisms are type equivalences; and where the equivalence of
-- morphisms ≋ is extensional

open import Level renaming (zero to lzero; suc to lsuc)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_; _×_; uncurry)
open import Data.Fin using (Fin; zero; suc) -- needed for distributivity

import Relation.Binary.PropositionalEquality as P
  using (sym)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)

open import Equiv
  using (_≃_; id≃; sym≃; _●_; _⊎≃_; _×≃_)
open import EquivEquiv
  using (_≋_; eq; id≋; sym≋; trans≋; ●-assoc; _◎_;
    linv≋; rinv≋; lid≋; rid≋; flip-sym≋)

-- list all explicitly, but these are all equivalences

open import TypeEquiv
  using (unite₊equiv; uniti₊equiv; unite₊′equiv; uniti₊′equiv;
         assocr₊equiv; assocl₊equiv;
         unite⋆equiv; uniti⋆equiv; unite⋆′equiv; uniti⋆′equiv;
         assocr⋆equiv; assocl⋆equiv; swap₊equiv;
         swap⋆equiv;
         distequiv; factorequiv;
         distlequiv; factorlequiv;
         distzequiv; factorzequiv;
         distzrequiv; factorzrequiv)

open import TypeEquivEquiv -- need them all!

-- convenience
one two : Fin 3
one = suc zero
two = suc (suc zero)

------------------------------------------------------------------------------
-- We show that types with type equivalences are a commutative rig
-- groupoid

-- First it is a category

TypeEquivCat : Category (lsuc lzero) lzero lzero
TypeEquivCat = record
  { Obj = Set
  ; _⇒_ = _≃_
  ; _≡_ = _≋_
  ; id = id≃
  ; _∘_ = _●_
  ; assoc = λ { {f = f} {g} {h} → ●-assoc {f = f} {g} {h} }
  ; identityˡ = lid≋
  ; identityʳ = rid≋
  ; equiv = record { refl = id≋ ; sym = sym≋ ; trans = trans≋ }
  ; ∘-resp-≡ = _◎_
  }

-- The category has inverses and hence a groupoid

TypeEquivGroupoid : Groupoid TypeEquivCat
TypeEquivGroupoid = record
  { _⁻¹ = sym≃
  ; iso = λ { {f = A≃B} → record
    { isoˡ = linv≋ A≃B
    ; isoʳ = rinv≋ A≃B
    } }
  }

-- The additive structure is monoidal

⊎-bifunctor : Bifunctor TypeEquivCat TypeEquivCat TypeEquivCat
⊎-bifunctor = record
  { F₀ = uncurry _⊎_
  ; F₁ = uncurry _⊎≃_
  ; identity = [id,id]≋id
  ; homomorphism = ⊎●≋●⊎
  ; F-resp-≡ = uncurry _⊎≋_
  }

module ⊎h = MonoidalHelperFunctors TypeEquivCat ⊎-bifunctor ⊥

0⊎x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊎x≡x = record
  { F⇒G = record
    { η = λ X → unite₊equiv {X zero}
    ; commute = λ f → unite₊-nat {f = f zero} }
  ; F⇐G = record
    { η = λ X → uniti₊equiv {X zero}
    ; commute = λ f →  uniti₊-nat {f = f zero} }
  ; iso = λ _ → record
    { isoˡ = linv≋ unite₊equiv
    ; isoʳ = rinv≋ unite₊equiv
    }
  }

x⊎0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊎0≡x = record
  { F⇒G = record
    { η = λ X → unite₊′equiv {X zero}
    ; commute = λ f → unite₊′-nat {f = f zero}
    }
  ; F⇐G = record
    { η = λ X → uniti₊′equiv {X zero}
    ; commute = λ f → uniti₊′-nat {f = f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite₊′equiv
    ; isoʳ = rinv≋ unite₊′equiv
    }
  }

[x⊎y]⊎z≡x⊎[y⊎z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊎y]⊎z≡x⊎[y⊎z] = record
  { F⇒G = record
    { η = λ X → assocr₊equiv {X zero} {X one} {X two}
    ; commute = λ f → assocr₊-nat {f₀ = f zero} {f one} {f two}
    }
  ; F⇐G = record
    { η = λ X → assocl₊equiv {X zero} {X one} {X two}
    ; commute = λ f → assocl₊-nat {f₀ = f zero} {f one} {f two}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ assocr₊equiv
    ; isoʳ = rinv≋ assocr₊equiv
    }
  }

CPM⊎ : Monoidal TypeEquivCat
CPM⊎ = record
  { ⊗ = ⊎-bifunctor
   ; id = ⊥
   ; identityˡ = 0⊎x≡x
   ; identityʳ = x⊎0≡x
   ; assoc = [x⊎y]⊎z≡x⊎[y⊎z]
   ; triangle = unite-assocr₊-coh
   ; pentagon = assocr₊-coh
   }

-- The multiplicative structure is also monoidal

×-bifunctor : Bifunctor TypeEquivCat TypeEquivCat TypeEquivCat
×-bifunctor = record
  { F₀ = uncurry _×_
  ; F₁ = uncurry _×≃_
  ; identity = id×id≋id
      -- the following would have unresolved metas without the extra precision
  ; homomorphism = λ { {f = (f , g)} {h , i} → ×●≋●× {f = f} {g} {h} {i}}
  ; F-resp-≡ = uncurry _×≋_
  }

module ×h = MonoidalHelperFunctors TypeEquivCat ×-bifunctor ⊤

1×y≡y : NaturalIsomorphism ×h.id⊗x ×h.x
1×y≡y = record
  { F⇒G = record
    { η = λ X → unite⋆equiv {X zero}
    ; commute = λ f → unite⋆-nat {f = f zero}
    }
  ; F⇐G = record
    { η = λ X → uniti⋆equiv {X zero}
    ; commute = λ f → uniti⋆-nat {f = f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite⋆equiv
    ; isoʳ = rinv≋ unite⋆equiv
    }
  }

y×1≡y : NaturalIsomorphism ×h.x⊗id ×h.x
y×1≡y = record
  { F⇒G = record
    { η = λ X → unite⋆′equiv {X zero}
    ;  commute = λ f → unite⋆′-nat {f = f zero}
    }
  ; F⇐G = record
    { η = λ X → uniti⋆′equiv {X zero}
    ; commute = λ f → uniti⋆′-nat {f = f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite⋆′equiv
    ; isoʳ = rinv≋ unite⋆′equiv
    }
  }

[x×y]×z≡x×[y×z] : NaturalIsomorphism ×h.[x⊗y]⊗z ×h.x⊗[y⊗z]
[x×y]×z≡x×[y×z] = record
  { F⇒G = record
    { η = λ X → assocr⋆equiv {X zero} {X one} {X two}
    ; commute = λ f → assocr⋆-nat {f₀ = f zero} {f one} {f two}}
  ; F⇐G = record
    { η = λ X → assocl⋆equiv {X zero} {X one} {X two}
    ; commute = λ f → assocl⋆-nat {f₀ = f zero} {f one} {f two}}
  ; iso = λ X → record
    { isoˡ = linv≋ assocr⋆equiv
    ; isoʳ = rinv≋ assocr⋆equiv }
  }

CPM× : Monoidal TypeEquivCat
CPM× = record
  { ⊗ = ×-bifunctor
  ; id = ⊤
  ; identityˡ = 1×y≡y
  ; identityʳ = y×1≡y
  ; assoc = [x×y]×z≡x×[y×z]
  ; triangle = unite-assocr⋆-coh
  ; pentagon = assocr⋆-coh
  }

-- The monoidal structures are symmetric

x⊎y≈y⊎x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊎y≈y⊎x = record
  { F⇒G = record
    { η = λ X → swap₊equiv {X zero} {X (suc zero)}
    ; commute = λ f → swap₊-nat {f = f zero} {f (suc zero)}
    }
  ; F⇐G = record
    { η = λ X → sym≃ (swap₊equiv {X zero} {X (suc zero)})
    ; commute = λ f → swap₊-nat {f = f (suc zero)} {f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ swap₊equiv
    ; isoʳ = rinv≋ swap₊equiv
    }
  }

BM⊎ : Braided CPM⊎
BM⊎ = record
  { braid = x⊎y≈y⊎x
  ; unit-coh = unite₊l-coh
  ; hexagon₁ = assocr₊-swap₊-coh
  ; hexagon₂ = assocl₊-swap₊-coh
  }

x×y≈y×x : NaturalIsomorphism ×h.x⊗y ×h.y⊗x
x×y≈y×x = record
  { F⇒G = record
    { η = λ X → swap⋆equiv
    ; commute = λ _ → swap⋆-nat
    }
  ; F⇐G = record
    { η = λ X → sym≃ swap⋆equiv
    ; commute = λ f → swap⋆-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ swap⋆equiv
    ; isoʳ = rinv≋ swap⋆equiv
    }
  }

BM× : Braided CPM×
BM× = record
  { braid = x×y≈y×x
  ; unit-coh = unite⋆l-coh
  ; hexagon₁ = assocr⋆-swap⋆-coh
  ; hexagon₂ = assocl⋆-swap⋆-coh
  }

SBM⊎ : Symmetric BM⊎
SBM⊎ = record { symmetry = linv≋ swap₊equiv }

SBM× : Symmetric BM×
SBM× = record { symmetry = linv≋ swap⋆equiv }

-- And finally the multiplicative structure distributes over the
-- additive one

module r = BimonoidalHelperFunctors BM⊎ BM×

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record
  { F⇒G = record
    { η = λ X → distlequiv {X zero} {X one} {X two}
    ; commute = λ f → distl-nat {f = f zero} {f one} {f two}
    }
  ; F⇐G = record
    { η = λ X → factorlequiv {X zero} {X one} {X two}
    ; commute = λ f → factorl-nat {f = f zero} {f one} {f two}
    }
  ; iso = λ X → record { isoˡ = linv≋ distlequiv
                       ; isoʳ = rinv≋ distlequiv }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record
    { η = λ X → distequiv
    ; commute = λ f → dist-nat
    }
  ; F⇐G = record
    { η = λ X → factorequiv
    ; commute = λ f → factor-nat
    }
  ; iso = λ X → record { isoˡ = linv≋ distequiv
                       ; isoʳ = rinv≋ distequiv }
  }

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record
    { η = λ X → distzrequiv {X zero}
    ; commute = λ f → distzr-nat {f = f zero}
    }
  ; F⇐G = record
    { η = λ X → factorzrequiv {X zero}
    ; commute = λ f → factorzr-nat {f = f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ distzrequiv
    ; isoʳ = rinv≋ distzrequiv
    }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record
    { η = λ X → distzequiv {X zero}
    ; commute = λ f → distz-nat {f = f zero}
    }
  ; F⇐G = record
    { η = λ X → factorzequiv {X zero}
    ; commute = λ f → factorz-nat {f = f zero}
    }
  ; iso = λ X → record
    { isoˡ = linv≋ (distzequiv {X zero})
    ; isoʳ = rinv≋ distzequiv
    }
  }

TERig : RigCategory SBM⊎ SBM×
TERig = record
  -- new combinators
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  -- derived identities which are ``coherent'' in that the
  -- two natural programs, using the new combinators and
  -- the underlying ones of the symmetric bimonoidal groupoid
  -- are in fact to be identified.
  ; laplazaI = λ {X} → A×[B⊎C]≃[A×C]⊎[A×B] {X zero} {X one} {X two}
  ; laplazaII = λ {X} → [A⊎B]×C≃[C×A]⊎[C×B] {X zero} {X one} {X two}
  ; laplazaIV = λ {X} → [A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D {X zero} {X (suc zero)}
                          {X (suc (suc zero))} {X (suc (suc (suc zero)))}
  ; laplazaVI = λ {X} → A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D {X zero} {X (suc zero)}
                          {X (suc (suc zero))} {X (suc (suc (suc zero)))}
  ; laplazaIX = λ {X} → [A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D {X zero} {X (suc zero)}
                          {X (suc (suc zero))} {X (suc (suc (suc zero)))}
  ; laplazaX = 0×0≃0
  ; laplazaXI = λ {X} → 0×[A⊎B]≃0 {X zero} {X (suc zero)}
  ; laplazaXIII = 0×1≃0
  ; laplazaXV = λ {X} → A×0≃0 {X zero}
  ; laplazaXVI = λ {X} → 0×A×B≃0 {X zero} {X (suc zero)}
  ; laplazaXVII = λ {X} → A×0×B≃0 {X zero} {X (suc zero)}
  ; laplazaXIX = λ {X} → A×[0+B]≃A×B {X zero} {X (suc zero)}
  ; laplazaXXIII = λ {X} → 1×[A⊎B]≃A⊎B {X zero} {X (suc zero)}
  }

-- Notes from Laplaza, 72
-- All of 2, 9, 10, 15
-- one of each of {1,3}, {4,5}, {6,7}, {9, 12},{13,,14},
--   {19,20,21,22}, {23,24}
-- two-of-three of {16,17,18}
--
-- for natural isos
-- α : A × (B × C) → (A × B) × C
-- γ : A × B → B × A
-- λ : U × A → A  (so that U is 1)
-- ρ : A × U → A
-- λ* : N × A → N (so that N is 0)
-- ρ* : A × n → N
-- and ' versions for ⊕
-- as well as natural monomorphisms
-- δ : A × (B ⊎ C) → (A × B) ⊎ (A × C)
-- δ# : (A ⊎ B) × C → (A × C) ⊎ (B × C)

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module _ where

data X : Set where
data R (x : X) : Set where

module SUListSepElemTypes where

  module M2 (Elem : Set) where
    data InclWith : Set where

  module M1 where
    module InclZip1 (R : X → Set) where
      open M2 X public
      module InclZipUnion (Y : Set) where

module SepElemTypes = SUListSepElemTypes

module Zip⊆ = SepElemTypes.M1.InclZip1 R
module Zip⊆∪ = Zip⊆.InclZipUnion X


text:
open import Everything

module Test.Test5
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔞} {𝔒₁ : 𝔛 → Ø 𝔞}
  {𝔟} {𝔒₂ : 𝔛 → Ø 𝔟}
  {ℓ}
  {ℓ̇} (_↦_ : ∀ {x} → 𝔒₂ x → 𝔒₂ x → Ø ℓ̇)
  ⦃ _ : [ExtensibleType] _↦_ ⦄
  ⦃ _ : Smap!.class (Arrow 𝔒₁ 𝔒₂) (Extension 𝔒₂) ⦄
  ⦃ _ : Surjextensionality!.class (Arrow 𝔒₁ 𝔒₂) (Pointwise _↦_) (Extension 𝔒₂) (Pointwise _↦_) ⦄
  -- ⦃ _ : [𝓢urjectivity] (Arrow 𝔒₁ 𝔒₂) (Extension $ ArrowExtensionṖroperty ℓ 𝔒₁ 𝔒₂ _↦_) ⦄
  where
  test[∙] : ∀ {x y} → ArrowExtensionṖroperty ℓ 𝔒₁ 𝔒₂ _↦_ x → Arrow 𝔒₁ 𝔒₂ x y → ArrowExtensionṖroperty ℓ 𝔒₁ 𝔒₂ _↦_ y
  test[∙] P f = f ◃ P


text:
module Div2 where

record True : Set where

data False : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

NonZero : Nat -> Set
NonZero  zero   = False
NonZero (suc _) = True

divHelp : Nat -> Nat -> Nat -> Nat
divHelp  zero    zero   c = suc zero
divHelp  zero   (suc y) c = zero
divHelp (suc x)  zero   c = suc (divHelp x c c)
divHelp (suc x) (suc y) c = divHelp x y c

div : (x y : Nat) -> {p : NonZero y} -> Nat
div  x       zero  {}
div  zero   (suc y) = zero
div (suc x) (suc y) = divHelp (suc x) (suc y) y

n1 = suc zero
n2 = suc n1
n3 = suc n2
n4 = suc n3
n5 = suc n4
n6 = suc n5
n7 = suc n6
n8 = suc n7
n9 = suc n8
n10 = suc n9
n11 = suc n10
n12 = suc n11

test1 : Nat
test1 = div n12 n7


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.IO where

postulate IO : ∀ {a} → Set a → Set a
{-# BUILTIN IO IO #-}

{-# FOREIGN GHC type AgdaIO a b = IO b #-}
{-# COMPILE GHC IO = type AgdaIO #-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
open import Oscar.Prelude

module Oscar.Class.Pure where

module _
  {𝔬 𝔣}
  (𝔉 : Ø 𝔬 → Ø 𝔣)
  where
  𝓹ure = ∀ {𝔒 : Ø 𝔬} → 𝔒 → 𝔉 𝔒
  record 𝓟ure : Ø 𝔣 ∙̂ ↑̂ 𝔬 where
    field pure : 𝓹ure
open 𝓟ure ⦃ … ⦄ public


text:
record R₁ : Set₁ where
  field
    A : Set

open R₁ ⦃ … ⦄

record R₂ : Set₁ where
  field
    ⦃ r₁ ⦄ : R₁

  B : Set
  B = A